For example, for a coq file that looks like:
Theorem mini : forall a:nat, a + 0 = a. Proof. auto. Qed. Theorem main : forall a:nat, a + 0 = a /\ a + 1 > a. Proof. split. ...
Then is there some tactic that can search through the current context to see that this first subgoal has already been solved previously in “Theorem mini” and then runs “apply mini”?
I know I can do an explicit search with “Search (forall a:nat, a+0 = a)”!