Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof state before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
have hl (acc : Array Assignment) (ih : modified_assignments_invariant acc) (cOpt : Option (DefaultClause n))
  (cOpt_in_arr : cOpt ∈ arr.data) : modified_assignments_invariant (ofArray_fold_fn acc cOpt) := by
  have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size, ih.1]
  apply Exists.intro hsize
  intro i b h
  simp only [ofArray_fold_fn] at h
  split at h
  . exact ih.2 i b h
  . next cOpt c =>
    match heq : isUnit c with
    | none =>
      simp only [heq] at h
      exact ih.2 i b h
    | some (l, true) =>
      simp only [heq] at h
      have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
      have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
      rcases ih with ⟨hsize, ih⟩
      by_cases i = l.1
      . next i_eq_l =>
        simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
        by_cases b
        . next b_eq_true =>
          rw [isUnit_iff, DefaultClause.toList] at heq
          simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
          have i_eq_l : i = l := Subtype.ext i_eq_l
          simp only [unit, b_eq_true, i_eq_l]
          have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
          simp only [heq] at c_def
          rw [c_def] at cOpt_in_arr
          exact cOpt_in_arr
        . next b_eq_false =>
          simp only [Bool.not_eq_true] at b_eq_false
          simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
          specialize ih l false
          simp only [hasAssignment, ite_false] at ih
          rw [b_eq_false, Subtype.ext i_eq_l]
          exact ih h
      . next i_ne_l =>
        simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
        exact ih i b h
    | some (l, false) =>
      simp only [heq] at h
      have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
      have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
      rcases ih with ⟨hsize, ih⟩
      by_cases i = l.1
      . next i_eq_l =>
        simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
        by_cases b
        . next b_eq_true =>
          simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
          specialize ih l true
          simp only [hasAssignment, ite_false] at ih
          rw [b_eq_true, Subtype.ext i_eq_l]
          exact ih h
        . next b_eq_false =>
          rw [isUnit_iff, DefaultClause.toList] at heq
          simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
          have i_eq_l : i = l := Subtype.ext i_eq_l
          simp only [unit, b_eq_false, i_eq_l]
          have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
          simp only [heq] at c_def
          rw [c_def] at cOpt_in_arr
          exact cOpt_in_arr
      . next i_ne_l =>
        simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
        exact ih i b h
Proof state after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList