Theorem: LRAT.DefaultFormula.performRatCheck_preserves_formula
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
c : DefaultClause n
heq✝ : f.clauses[ratHint.fst]! = some c
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete p).negate).snd =
      true
⊢ (if
          (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).2.2.snd =
              true ∨
            (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).2.2.fst =
              false then
        ({
              clauses :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.clauses,
              rupUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.rupUnits,
              ratUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.ratUnits,
              assignments :=
                restoreAssignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.assignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).2.fst }.clearRatUnits,
          false)
      else
        ({
              clauses :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.clauses,
              rupUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.rupUnits,
              ratUnits :=
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).1.ratUnits,
              assignments :=
                restoreAssignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).1.assignments
                  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                  assignments := f.assignments }.insertRatUnits
                              (c.delete p).negate).fst.performRupCheck
                        ratHint.snd).2.fst }.clearRatUnits,
          true)).fst =
    f
Tactic:
. let fc := (insertRatUnits f (negate (DefaultClause.delete c p))).1
  have fc_assignments_size : fc.assignments.size = n := by rw [insertRatUnits_preserves_assignments_size, hf.2]
  have insertRatUnits_rw : (insertRatUnits f (negate (DefaultClause.delete c p))).1 =
    ⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits,
     (insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl
  simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits]
  rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw,
    clear_insertRat f hf (negate (DefaultClause.delete c p))]
  split <;> rfl
Proof state after:
no goals