Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant 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.modify_preserves_size)) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get 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
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] = addAssignment (acc.snd.fst.get ⟨↑j, ⋯⟩).snd f.assignments[↑i] ∧
    ¬hasAssignment (acc.snd.fst.get ⟨↑j, ⋯⟩).snd f.assignments[↑i] = true ∧
      ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨↑j + 1, j_succ_in_bounds⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case right.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant 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.modify_preserves_size)) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get 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
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] = addAssignment (acc.snd.fst.get ⟨↑j, ⋯⟩).snd f.assignments[↑i]

case right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant 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.modify_preserves_size)) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get 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
⊢ ¬hasAssignment (acc.snd.fst.get ⟨↑j, ⋯⟩).snd f.assignments[↑i] = true ∧
    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨↑j + 1, j_succ_in_bounds⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i