Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case inl.intro
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
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (l_1 : Literal (PosFin n)), l_1 ∈ l :: acc.snd.fst → l_1.fst.val ≠ ↑i) ∨
    (∃ j,
        ((l :: acc.snd.fst).get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((l :: acc.snd.fst).get j).snd fassignments_i ∧
            ¬hasAssignment ((l :: acc.snd.fst).get j).snd fassignments_i = true ∧
              ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((l :: acc.snd.fst).get j1).fst.val = ↑i ∧
          ((l :: acc.snd.fst).get j2).fst.val = ↑i ∧
            ((l :: acc.snd.fst).get j1).snd = true ∧
              ((l :: acc.snd.fst).get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j1 → k ≠ j2 → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Tactic:
by_cases l.1.1 = i.1
Proof state after:
case pos
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
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
h✝ : l.fst.val = ↑i
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (l_1 : Literal (PosFin n)), l_1 ∈ l :: acc.snd.fst → l_1.fst.val ≠ ↑i) ∨
    (∃ j,
        ((l :: acc.snd.fst).get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((l :: acc.snd.fst).get j).snd fassignments_i ∧
            ¬hasAssignment ((l :: acc.snd.fst).get j).snd fassignments_i = true ∧
              ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((l :: acc.snd.fst).get j1).fst.val = ↑i ∧
          ((l :: acc.snd.fst).get j2).fst.val = ↑i ∧
            ((l :: acc.snd.fst).get j1).snd = true ∧
              ((l :: acc.snd.fst).get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j1 → k ≠ j2 → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i

case neg
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
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
h✝ : ¬l.fst.val = ↑i
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (l_1 : Literal (PosFin n)), l_1 ∈ l :: acc.snd.fst → l_1.fst.val ≠ ↑i) ∨
    (∃ j,
        ((l :: acc.snd.fst).get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((l :: acc.snd.fst).get j).snd fassignments_i ∧
            ¬hasAssignment ((l :: acc.snd.fst).get j).snd fassignments_i = true ∧
              ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((l :: acc.snd.fst).get j1).fst.val = ↑i ∧
          ((l :: acc.snd.fst).get j2).fst.val = ↑i ∧
            ((l :: acc.snd.fst).get j1).snd = true ∧
              ((l :: acc.snd.fst).get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j1 → k ≠ j2 → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i