Theorem: LRAT.DefaultFormula.insert_preserves_ratUnits (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).ratUnits = f.ratUnits
Tactic:
simp only [insert]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).ratUnits =
    f.ratUnits

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).ratUnits =
    f.ratUnits
Tactic:
split <;> simp only
State after:
no goals