Update grind_try_trace.lean

leanprover · Feb 22, 2025 · 9b72395 · 9b72395
1 parent 1777673
commit 9b72395
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/tests/lean/run/grind_try_trace.lean b/tests/lean/run/grind_try_trace.lean
@@ -132,10 +132,9 @@ example (as : List α) (a : α) : concat as a = as ++ [a] := by
 /--
 info: Try these:
 • (fun_induction concat) <;> simp_all
-• ·
-  fun_induction concat
-  · simp
-  · simp [*]
+• · fun_induction concat
+    · simp
+    · simp [*]
 -/
 #guard_msgs (info) in
 example (as : List α) (a : α) : concat as a = as ++ [a] := by