Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isTrue.isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ f' = f.insert c
Tactic:
. next performRatCheck_fold_success =>
  simp only [Bool.not_eq_false] at performRatCheck_fold_success
  let fc := (insertRupUnits f (negate c)).1
  have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
    rw [insertRupUnits_preserves_assignments_size f (negate c)]
    exact f_readyForRatAdd.2.2.1
  simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
    restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
  rw [← ratAddSuccess]
  clear f' ratAddSuccess
  let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
  have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
    have hsize : performRupCheck_res.assignments.size = n := by
      rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
    exact And.intro f_readyForRatAdd.1 hsize
  have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
    ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
     (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
  simp only [performRatCheck_fold_preserves_formula performRupCheck_res h_performRupCheck_res (negateLiteral p) ratHints,
    performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
    restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
    clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
Proof state after:
no goals