diff --git a/Mathlib/Tactic/Sat/FromLRAT.lean b/Mathlib/Tactic/Sat/FromLRAT.lean
index 3bbdaa9c67d0c..6104d507b0039 100644
--- 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