feat: exact? finds eliminator-style theorems like iteInduction

src/Lean/Meta/LazyDiscrTree.lean

@@ -368,7 +368,13 @@ def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) :
       let nargs := e.getAppNumArgs
       push (.proj s i nargs) nargs (todo.push a)
     | .fvar _fvarId   =>
-      return (.star, todo)
+      let nargs := e.getAppNumArgs
+      if nargs == 0 then
+        return (.star, todo)
+      else
+        let info ← getFunInfoNArgs fn nargs
+        let todo ← MatchClone.pushArgsAux info.paramInfo (nargs-1) e todo
+        return (.star, todo)
     | .mvar mvarId   =>
       if mvarId == MatchClone.tmpMVarId then
         -- We use `tmp to mark implicit arguments and proofs
@@ -675,16 +681,21 @@ def getMatchCore (root : Std.HashMap Key TrieIndex) (e : Expr) :
     MatchM α (MatchResult α) := do
   let result ← getStarResult root
   let (k, args) ← MatchClone.getMatchKeyArgs e (root := true) (← read)
-  let cases :=
-    match k with
+  let cases ← match k with
     | .star  =>
-      #[]
+      pure #[]
+    /- When goal has fvar head like `p (ite c t e)`, follow the star edge with the fvar's arguments.
+       This finds "eliminator-style" theorems indexed by argument structure. -/
+    | .fvar _ _ =>
+      match root[Key.star]? with
+      | some c => pure #[{ todo := args, score := 0, c }]
+      | none => pure #[]
     /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
     | .arrow =>
-      #[] |> pushRootCase root .other #[]
-          |> pushRootCase root k args
+      pure (#[] |> pushRootCase root .other #[]
+                |> pushRootCase root k args)
     | _ =>
-      #[] |> pushRootCase root k args
+      pure (#[] |> pushRootCase root k args)
   getMatchLoop cases result
 
 /--

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -143,13 +143,10 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
   if name.isMetaprogramming then return #[] else
   forallTelescope constInfo.type fun _ type => do
     let e ← InitEntry.fromExpr type (name, DeclMod.none)
-    let a := #[e]
     if e.key == .const ``Iff 2 then
-      let a := a.push (← e.mkSubEntry 0 (name, DeclMod.mp))
-      let a := a.push (← e.mkSubEntry 1 (name, DeclMod.mpr))
-      pure a
+      return #[e, ← e.mkSubEntry 0 (name, DeclMod.mp), ← e.mkSubEntry 1 (name, DeclMod.mpr)]
     else
-      pure a
+      return #[e]
 
 /-- Stores import discrimination tree. -/
 private def LibSearchState := IO.Ref (Option (LazyDiscrTree (Name × DeclMod)))

tests/lean/run/librarySearch_eliminators.lean

@@ -0,0 +1,18 @@
+/-
+Test that exact? finds "eliminator-style" theorems like iteInduction
+where the conclusion has an fvar head: `motive (C args...)`.
+-/
+
+-- Test that exact? finds iteInduction for fvar-headed goals
+example {α : Sort u} (h : Prop) [Decidable h] {x y : α} {p : α → Prop}
+    (hx : h → p x) (hy : ¬h → p y) : p (if h then x else y) := by
+  exact iteInduction hx hy
+
+/--
+info: Try this:
+  [apply] exact iteInduction hx hy
+-/
+#guard_msgs in
+example {α : Sort u} (h : Prop) [Decidable h] {x y : α} {p : α → Prop}
+    (hx : h → p x) (hy : ¬h → p y) : p (if h then x else y) := by
+  exact?