-- 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 inr.inr.intro.intro.intro.intro.intro.intro.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
j1 j2 : Fin (List.length acc.snd.fst)
j1_eq_i : (List.get acc.snd.fst j1).fst.val = ↑i
j2_eq_i : (List.get acc.snd.fst j2).fst.val = ↑i
j1_eq_true : (List.get acc.snd.fst j1).snd = true
j2_eq_false : (List.get acc.snd.fst j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j1 → k ≠ j2 → (List.get acc.snd.fst k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
⊢ ((l :: acc.snd.fst).get j1_succ).fst.val = ↑i ∧
    ((l :: acc.snd.fst).get j2_succ).fst.val = ↑i ∧
      ((l :: acc.snd.fst).get j1_succ).snd = true ∧
        ((l :: acc.snd.fst).get j2_succ).snd = false ∧
          (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] = both ∧
            f.assignments[↑i] = unassigned ∧
              ∀ (k : Fin (List.length acc.snd.fst + 1)),
                ¬k = j1_succ → ¬k = j2_succ → ¬((l :: acc.snd.fst).get k).fst.val = ↑i

Tactic:
apply And.intro j1_eq_i ∘ And.intro j2_eq_i ∘ And.intro j1_eq_true ∘ And.intro j2_eq_false

Result:
case inr.inr.intro.intro.intro.intro.intro.intro.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
j1 j2 : Fin (List.length acc.snd.fst)
j1_eq_i : (List.get acc.snd.fst j1).fst.val = ↑i
j2_eq_i : (List.get acc.snd.fst j2).fst.val = ↑i
j1_eq_true : (List.get acc.snd.fst j1).snd = true
j2_eq_false : (List.get acc.snd.fst j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j1 → k ≠ j2 → (List.get acc.snd.fst k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] = both ∧
    f.assignments[↑i] = unassigned ∧
      ∀ (k : Fin (List.length acc.snd.fst + 1)), ¬k = j1_succ → ¬k = j2_succ → ¬((l :: acc.snd.fst).get k).fst.val = ↑i

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
j1 j2 : Fin (List.length acc.snd.fst)
j1_eq_i : (List.get acc.snd.fst j1).fst.val = ↑i
j2_eq_i : (List.get acc.snd.fst j2).fst.val = ↑i
j1_eq_true : (List.get acc.snd.fst j1).snd = true
j2_eq_false : (List.get acc.snd.fst j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j1 → k ≠ j2 → (List.get acc.snd.fst k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
l_ne_i : l.fst.val ≠ ↑i
k : Fin (List.length acc.snd.fst + 1)
k_ne_j1_succ : ¬k = j1_succ
k_ne_j2_succ : ¬k = j2_succ
zero_in_bounds : 0 < (l :: acc.snd.fst).length
k_ne_zero : ¬k = ⟨0, zero_in_bounds⟩
⊢ ↑k ≠ 0

Tactic:
intro k_eq_zero

Result:
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
j1 j2 : Fin (List.length acc.snd.fst)
j1_eq_i : (List.get acc.snd.fst j1).fst.val = ↑i
j2_eq_i : (List.get acc.snd.fst j2).fst.val = ↑i
j1_eq_true : (List.get acc.snd.fst j1).snd = true
j2_eq_false : (List.get acc.snd.fst j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin (List.length acc.snd.fst)), k ≠ j1 → k ≠ j2 → (List.get acc.snd.fst k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
l_ne_i : l.fst.val ≠ ↑i
k : Fin (List.length acc.snd.fst + 1)
k_ne_j1_succ : ¬k = j1_succ
k_ne_j2_succ : ¬k = j2_succ
zero_in_bounds : 0 < (l :: acc.snd.fst).length
k_ne_zero : ¬k = ⟨0, zero_in_bounds⟩
k_eq_zero : ↑k = 0
⊢ False