Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case inr.inl.intro.intro.intro.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
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
⊢ 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 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 × 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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).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:
. let l' := acc.2.1.get j
  have zero_in_bounds : 0 < (l :: acc.2.1).length := by
    simp only [List.length_cons]
    exact Nat.zero_lt_succ (List.length acc.snd.fst)
  have j_succ_in_bounds : j.1 + 1 < (l :: acc.2.1).length := by
    simp only [List.length_cons, Nat.succ_eq_add_one]
    exact Nat.succ_lt_succ j.2
  by_cases l.1.1 = i.1
  . next l_eq_i =>
    apply Or.inr ∘ Or.inr
    have l_ne_l' : l.2 ≠ l'.2 := by
      intro l_eq_l'
      rw [l_eq_i] at h
      simp only [l'] at l_eq_l'
      simp [getElem!, i_in_bounds, h1, ← l_eq_l', has_of_add] at h
    by_cases l.2
    . next l_eq_true =>
      rw [l_eq_true] at l_ne_l'
      have l'_eq_false : l'.2 = false := by rw [← Bool.not_eq_true]; exact Ne.symm l_ne_l'
      apply Exists.intro ⟨0, zero_in_bounds⟩
      apply Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩
      constructor
      . simp only [List.get]
        exact l_eq_i
      . constructor
        . simp only [List.get, Nat.add_eq, Nat.add_zero]
          exact j_eq_i
        . simp only [List.get, Nat.add_eq, Nat.add_zero, List.length_cons, ne_eq]
          apply And.intro l_eq_true ∘ And.intro l'_eq_false
          constructor
          . simp only [l'] at l'_eq_false
            simp only [l_eq_i, addAssignment, l_eq_true, ite_true, Array.get_modify_at_idx i_in_bounds, h1,
              l'_eq_false, ite_false]
            apply addPos_of_addNeg_eq_both
          . constructor
            . simp only [l'] at l'_eq_false
              simp only [l'_eq_false, hasAssignment, ite_false] at h2
              simp only [hasAssignment, l_eq_true, getElem!, l_eq_i, i_in_bounds,
                Array.get_eq_getElem, ↓reduceIte, ↓reduceDite, h1, addAssignment, l'_eq_false,
                hasPos_of_addNeg] at h
              exact unassigned_of_has_neither _ h h2
            . intro k k_ne_zero k_ne_j_succ
              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 k'] 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 [k_eq_succ, List.length_cons, 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
    . next l_eq_false =>
      simp only [Bool.not_eq_true] at l_eq_false
      rw [l_eq_false] at l_ne_l'
      have l'_eq_true : l'.2 = true := by
        have l'_ne_false : l'.2 ≠ false := Ne.symm l_ne_l'
        simp only [ne_eq, Bool.not_eq_false] at l'_ne_false
        exact l'_ne_false
      refine ⟨⟨j.1 + 1, j_succ_in_bounds⟩, ⟨0, zero_in_bounds⟩, ?_⟩
      constructor
      . simp only [List.get, Nat.add_eq, Nat.add_zero]
        exact j_eq_i
      . constructor
        . simp only [List.get]
          exact l_eq_i
        . simp only [List.get, Nat.add_eq, Nat.add_zero, List.length_cons, ne_eq]
          apply And.intro l'_eq_true ∘ And.intro l_eq_false
          constructor
          . simp only [l'] at l'_eq_true
            simp only [l_eq_i, addAssignment, l'_eq_true, ite_true, Array.get_modify_at_idx i_in_bounds, h1,
              l_eq_false, ite_false]
            apply addNeg_of_addPos_eq_both
          . constructor
            . simp only [l'] at l'_eq_true
              simp only [hasAssignment, l'_eq_true, ite_true] at h2
              simp only [hasAssignment, l_eq_false, ↓reduceIte, getElem!, l_eq_i, i_in_bounds,
                Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_of_addPos] at h
              exact unassigned_of_has_neither _ h2 h
            . intro k k_ne_j_succ 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 k'] 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 [k_eq_succ, List.length_cons, 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
  . next l_ne_i =>
    apply Or.inr ∘ Or.inl ∘ Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩
    simp only [List.get, Nat.add_eq, Nat.add_zero]
    constructor
    . exact j_eq_i
    . constructor
      . rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
        exact h1
      . apply And.intro h2
        intro k k_ne_j_succ
        by_cases k.1 = 0
        . next k_eq_zero =>
          have k_eq_zero : k = ⟨0, zero_in_bounds⟩ := by
            apply Fin.eq_of_val_eq
            simp only [List.length_cons]
            exact k_eq_zero
          simp only [k_eq_zero, List.length_cons, List.get, ne_eq]
          exact l_ne_i
        . 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
Proof state after:
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 × 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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).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