fix: use + 1 lemma in apply?

leanprover-community · May 28, 2024 · 379ac44 · 379ac44
1 parent 4422016
commit 379ac44
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/LibrarySearch/basic.lean b/test/LibrarySearch/basic.lean
@@ -19,7 +19,7 @@ set_option pp.unicode.fun true
 
 noncomputable section
 
-/-- info: Try this: exact Nat.lt.base x -/
+/-- info: Try this: exact Nat.lt_add_one x -/
 #guard_msgs in
 example (x : Nat) : x ≠ x.succ := ne_of_lt (by apply?)