-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula n)
    (f_assignments_size : f.assignments.size = n)
    (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = n)
    (l : Literal (PosFin n)) (ih : DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1)
    (h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true) :
    have hsize' : (Array.modify acc.1 l.1.1 (addAssignment l.snd)).size = n

Proof state:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) (Array.size_modify acc.fst l.fst.val (addAssignment l.snd)))) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j : Fin (List.length acc.snd.fst)
j_eq_i : (List.get acc.snd.fst j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (List.get acc.snd.fst j).snd f.assignments[↑i]
h2 : ¬hasAssignment (List.get acc.snd.fst j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j → (List.get acc.snd.fst k).fst.val ≠ ↑i
l' : Literal (PosFin n) := List.get acc.snd.fst j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
h✝ : ¬↑k = 0
⊢ ((l :: acc.snd.fst).get k).fst.val ≠ ↑i

Tactic:
next k_ne_zero =>
have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
  have k_val_ne_zero : k.1 ≠ 0 := by
    intro k_eq_zero
    simp only [List.length_cons, ← k_eq_zero, ne_eq, not_true] at k_ne_zero
  rcases Nat.exists_eq_succ_of_ne_zero k_val_ne_zero with ⟨k', k_eq_k'_succ⟩
  rw [Nat.succ_eq_add_one] at k_eq_k'_succ
  have k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length := by rw [← k_eq_k'_succ]; exact k.2
  apply Exists.intro k' ∘ Exists.intro k'_succ_in_bounds
  apply Fin.eq_of_val_eq
  exact k_eq_k'_succ
rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
rw [k_eq_succ]
simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq]
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
have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by
  simp only [List.length_cons] at k_eq_succ
  simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ
  exact Fin.ne_of_val_ne k_ne_j_succ
exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) (Array.size_modify acc.fst l.fst.val (addAssignment l.snd)))) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j : Fin (List.length acc.snd.fst)
j_eq_i : (List.get acc.snd.fst j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (List.get acc.snd.fst j).snd f.assignments[↑i]
h2 : ¬hasAssignment (List.get acc.snd.fst j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j → (List.get acc.snd.fst k).fst.val ≠ ↑i
l' : Literal (PosFin n) := List.get acc.snd.fst j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
⊢ ↑j + 1 < List.length acc.snd.fst + 1

Tactic:
exact Nat.succ_lt_succ j.2

Result:
no goals

Proof state:
case right.right.right.right.intro.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) (Array.size_modify acc.fst l.fst.val (addAssignment l.snd)))) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j : Fin (List.length acc.snd.fst)
j_eq_i : (List.get acc.snd.fst j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (List.get acc.snd.fst j).snd f.assignments[↑i]
h2 : ¬hasAssignment (List.get acc.snd.fst j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j → (List.get acc.snd.fst k).fst.val ≠ ↑i
l' : Literal (PosFin n) := List.get acc.snd.fst j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_eq_i : l.fst.val = ↑i
l_ne_l' : false ≠ l'.snd
l_eq_false : l.snd = false
l'_eq_true : l'.snd = true
k : Fin (List.length acc.snd.fst + 1)
k_ne_j_succ : ¬k = ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬k = ⟨0, zero_in_bounds⟩
k' : Nat
k'_succ_in_bounds : k' + 1 < (l :: acc.snd.fst).length
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
⊢ ¬((l :: acc.snd.fst).get k).fst.val = ↑i

Tactic:
rw [k_eq_succ]

Result:
case right.right.right.right.intro.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) (Array.size_modify acc.fst l.fst.val (addAssignment l.snd)))) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j : Fin (List.length acc.snd.fst)
j_eq_i : (List.get acc.snd.fst j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (List.get acc.snd.fst j).snd f.assignments[↑i]
h2 : ¬hasAssignment (List.get acc.snd.fst j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j → (List.get acc.snd.fst k).fst.val ≠ ↑i
l' : Literal (PosFin n) := List.get acc.snd.fst j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_eq_i : l.fst.val = ↑i
l_ne_l' : false ≠ l'.snd
l_eq_false : l.snd = false
l'_eq_true : l'.snd = true
k : Fin (List.length acc.snd.fst + 1)
k_ne_j_succ : ¬k = ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬k = ⟨0, zero_in_bounds⟩
k' : Nat
k'_succ_in_bounds : k' + 1 < (l :: acc.snd.fst).length
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
⊢ ¬((l :: acc.snd.fst).get ⟨k' + 1, k'_succ_in_bounds⟩).fst.val = ↑i