Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isTrue
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
ratAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          if
              (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 then
            ((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).fst,
              false)
          else
            ({
                      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

case 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
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c
Tactic:
. split at ratAddSuccess
  . simp at ratAddSuccess
  . split at ratAddSuccess
    . simp at ratAddSuccess
    . split at ratAddSuccess
      . simp at ratAddSuccess
      . split at ratAddSuccess
        . simp at ratAddSuccess
        . 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:
case 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
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c