chore: robustify FromLRAT proof (#16017)

Just an unsqueezed simp that broke on an adaptation branch.
leanprover-community · Aug 21, 2024 · 2db1a34 · 2db1a34
1 parent ed125a4
commit 2db1a34
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/Mathlib/Tactic/Sat/FromLRAT.lean b/Mathlib/Tactic/Sat/FromLRAT.lean
@@ -161,8 +161,9 @@ theorem Valuation.mk_implies {p} {as ps} (as₁) : as = List.reverseAux as₁ ps
     subst e; clear ih H
     suffices ∀ n n', n' = List.length as₁ + n →
       ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)
-    induction as₁ with simp
-    | cons b as₁ ih => exact fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _
+    induction as₁ with
+    | nil => simp
+    | cons b as₁ ih => simpa using fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _
 
 /-- Asserts that `¬⟦f⟧_v` implies `p`. -/
 structure Fmla.reify (v : Valuation) (f : Fmla) (p : Prop) : Prop where