feat: use expose_names at try?

src/Lean/Elab/Tactic/Try.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Try
 import Init.Grind.Tactics
+import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Try
 import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Tactic.Config
@@ -382,15 +383,21 @@ private def allAccessible (majors : Array FVarId) : MetaM Bool :=
 open Try.Collector in
 private def mkFunIndStx (c : FunIndCandidate) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
   if (← allAccessible c.majors) then
+    go
+  else withNewMCtxDepth do
+    -- Create a helper goal to apply
+    let mvarId := (← mkFreshExprMVar (mkConst ``True)).mvarId!
+    let mvarId ← mvarId.exposeNames
+    mvarId.withContext do
+      `(tactic| (expose_names; $(← go):tactic))
+where
+  go : MetaM (TSyntax `tactic) := do
     let mut terms := #[]
     for major in c.majors do
       let localDecl ← major.getDecl
       terms := terms.push (← `($(mkIdent localDecl.userName):term))
     let indFn ← toIdent c.funIndDeclName
     `(tactic| induction $terms,* using $indFn <;> $cont)
-  else
-    -- TODO: use `expose_names`
-    throwError "`induction` failed, majors contain inaccessible vars"
 
 private def mkAllFunIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
   let tacs ← info.funIndCandidates.toArray.mapM (mkFunIndStx · cont)

tests/lean/run/try_trace1.lean

@@ -75,3 +75,25 @@ info: Try these:
 #guard_msgs (info) in
 example : app (app as bs) cs = app as (app bs cs) := by
   try?
+
+/--
+info: Try these:
+• · expose_names; induction as, bs_1 using app.induct <;> grind [= app]
+• · expose_names; induction as, bs_1 using app.induct <;> grind only [app]
+-/
+#guard_msgs (info) in
+example : app (app as bs) cs = app as (app bs cs) := by
+  have bs := 20 -- shadow variable in the goal
+  try?
+
+/--
+info: Try these:
+• · expose_names; induction as, bs using app.induct <;> grind [= app]
+• · expose_names; induction as, bs using app.induct <;> grind only [app]
+-/
+#guard_msgs (info) in
+example : app (app as bs) cs = app as (app bs cs) := by
+  revert as bs cs
+  intro _ _ _
+  -- `as`, `bs`, and `cs` now have inaccessible names.
+  try?