Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case h_2
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c.isUnit = some (l✝, true)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addPosAssignment }.readyForRupAdd

case h_3
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c.isUnit = some (l✝, false)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addNegAssignment }.readyForRupAdd
Tactic:
. next l hc =>
  have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by
    rw [Array.modify_preserves_size, f_readyForRupAdd.2.1]
  refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
  intro i b hb
  have hf := f_readyForRupAdd.2.2 i b
  have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
  have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
  simp only at hb
  by_cases (i, b) = (l, true)
  . next ib_eq_c =>
    simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
      List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
    apply Or.inl ∘ Or.inr
    rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
    apply DefaultClause.ext
    simp only [unit, hc]
  . next ib_ne_c =>
    have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
      by_cases l.1 = i.1
      . next l_eq_i =>
        have b_eq_false : b = false := by
          by_cases b = true
          . next b_eq_true =>
            simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
          . next b_eq_false =>
            simp only [Bool.not_eq_true] at b_eq_false
            exact b_eq_false
        simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_false, hasNeg_of_addPos] at hb
        simp only [hasAssignment, b_eq_false, ite_false, hb]
      . next l_ne_i =>
        simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
        exact hb
    specialize hf hb'
    simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
      exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
    simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
      List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
    rcases hf with hf | hf
    . exact Or.inl $ Or.inl hf
    . exact Or.inr hf
Proof state after:
case h_3
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c.isUnit = some (l✝, false)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addNegAssignment }.readyForRupAdd