Update RupAddResult.lean

leanprover · Nov 19, 2024 · 5372af3 · 5372af3
1 parent a5e74f4
commit 5372af3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -815,7 +815,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             have k'_in_bounds : k' < acc.2.1.length := by
               simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
               exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
-            exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst k' k'_in_bounds
+            exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst ⟨k', k'_in_bounds⟩
     · next l_ne_i =>
       apply Or.inl
       constructor