feat: run try? +harder at an empty by

src/Init/Try.lean

@@ -50,6 +50,9 @@ namespace Lean.Parser.Tactic
 
 syntax (name := tryTrace) "try?" optConfig : tactic
 
+/-- Helper tactic for empty `by` blocks: runs `try?` and then reports unsolved goals. -/
+syntax (name := tryAndFail) "tryAndFail!" : tactic
+
 /-- Helper internal tactic for implementing the tactic `try?`. -/
 syntax (name := attemptAll) "attempt_all " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 

src/Lean/Elab/Tactic/Try.lean

@@ -685,4 +685,50 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
     evalAndSuggest tk stx config
   | _ => throwUnsupportedSyntax
 
+/-- Helper tactic for empty `by` blocks: runs `try? +harder` for suggestions,
+    then restores the goal without failing. -/
+@[builtin_tactic tryAndFail] def evalTryAndFail : Tactic := fun stx => do
+  match stx with
+  | `(tactic| tryAndFail!) => do withMainContext do
+    -- Prepare to run `try? +harder`.
+    let config : Try.Config := { harder := true }
+    let mainGoal ← getMainGoal
+    let info ← Try.collect mainGoal config
+    let tacStx ← mkTryEvalSuggestStx info
+
+    -- Evaluate the tactics and collect suggestions (this will consume goals)
+    let savedState ← saveState
+    let suggestions? ← try
+      let tac' ← evalSuggest tacStx |>.run { terminal := true, root := tacStx, config }
+      pure (some ((getSuggestions tac')[*...config.max].toArray))
+    catch _ =>
+      -- If try? fails to find a proof, just continue without suggestions
+      pure none
+    -- Restore state before adding suggestions
+    restoreState savedState
+
+    -- Now add the suggestions if we found any
+    if let some suggestions := suggestions? then
+      unless suggestions.isEmpty do
+        -- Wrap each tactic suggestion in `by` to make it a term suggestion
+        -- Use string format since constructing proper syntax is complex
+        let wrappedSuggestions ← suggestions.mapM fun sugg => do
+          let suggStr ← sugg.pretty
+          return { sugg with suggestion := .string s!"by {suggStr}" }
+        -- Use the reference to the enclosing term (the `by` block) instead of tk
+        let ref ← getRef
+        Tactic.TryThis.addSuggestions ref wrappedSuggestions (origSpan? := ref)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Try
+
+open Lean.Parser.Term in
+-- Macro to expand empty `by` blocks to `by tryAndFail!; done`
+-- This ensures we get both the try? suggestions AND the unsolved goals error
+@[builtin_macro Lean.Parser.Term.byTactic] def expandEmptyBy : Lean.Macro
+  | `(by%$tk $seq:tacticSeq) =>
+    if seq.raw.getArgs.all (·.isNone) then
+      `(by%$tk tryAndFail!; done)
+    else
+      Lean.Macro.throwUnsupported
+  | _ => Lean.Macro.throwUnsupported

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -35,7 +35,7 @@ def OrdSet.isEmpty {_ : Hashable α} {_ : BEq α} (s : OrdSet α) : Bool :=
   s.elems.isEmpty
 
 structure Result where
-  /-- All constant symbols occurring in the gal. -/
+  /-- All constant symbols occurring in the goal. -/
   allConsts : OrdSet Name  := {}
   /-- Unfolding candidates. -/
   unfoldCandidates : OrdSet Name  := {}

src/Lean/Parser/Term/Basic.lean

@@ -88,7 +88,7 @@ The strict indentation requirement only apply to *nested* `by`s, as top-level `b
 position set. -/
 @[builtin_doc, run_builtin_parser_attribute_hooks]
 def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
-  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
+  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented) <|> sepByIndentSemicolon tacticParser
 
 /- Raw sequence for quotation and grouping -/
 @[run_builtin_parser_attribute_hooks]

tests/lean/run/empty_by.lean

@@ -0,0 +1,84 @@
+import Std
+
+/--
+info: Try these:
+  [apply] simp
+  [apply] simp only
+  [apply] grind
+  [apply] grind only
+  [apply] simp_all
+-/
+#guard_msgs in
+example : True := by try?
+
+/--
+info: Try these:
+  [apply] by simp
+  [apply] by simp only
+  [apply] by grind
+  [apply] by grind only
+  [apply] by simp_all
+---
+error: unsolved goals
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+
+/--
+info: Try these:
+  [apply] by simp
+  [apply] by simp only [List.append_assoc]
+  [apply] by grind
+  [apply] by grind only
+  [apply] by simp_all
+---
+error: unsolved goals
+x y z : List Nat
+⊢ x ++ (y ++ z) = x ++ y ++ z
+-/
+#guard_msgs in
+example {x y z : List Nat} : x ++ (y ++ z) = (x ++ y) ++ z := by
+
+/--
+info: Try these:
+  [apply] by exact Int.emod_add_mul_ediv a b
+---
+error: unsolved goals
+a b : Int
+⊢ a % b + b * (a / b) = a
+-/
+#guard_msgs in
+example {a b : Int} : a % b + b * (a / b) = a := by
+
+/--
+info: Try these:
+  [apply] by grind
+  [apply] by grind only [= Std.ExtHashMap.getKey_erase, = Std.ExtHashMap.contains_erase,
+    = Std.ExtHashMap.mem_erase, = Std.ExtHashMap.contains_insert, = Std.ExtHashMap.getElem?_insert,
+    = getElem?_pos, = Std.ExtHashMap.getElem?_erase, = Std.ExtHashMap.getKey_eq, = getElem?_neg,
+    =_ Std.ExtHashMap.contains_iff_mem, = Std.ExtHashMap.mem_insert]
+---
+error: unsolved goals
+m : Std.ExtHashMap Nat Int
+⊢ (m.insert 37 5).erase 37 = m.erase 37
+-/
+#guard_msgs in
+example {m : Std.ExtHashMap Nat Int} : (m.insert 37 5).erase 37 = m.erase 37 := by
+
+def fib : Nat → Nat
+  | 0 => 0
+  | 1 => 1
+  | n + 2 => fib n + fib (n + 1)
+
+/--
+info: Try these:
+  [apply] by grind [= fib]
+  [apply] by grind only [fib]
+---
+error: unsolved goals
+n : Nat
+⊢ fib (n + 8) % 3 = fib n % 3
+-/
+#guard_msgs in
+example : fib (n + 8) % 3 = fib n % 3 := by