Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_size (LeanSAT/LRAT/Formula/RatAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRatUnits units).fst.assignments.size = f.assignments.size
Tactic:
simp only [insertRatUnits, Prod.mk.eta]
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst.size = f.assignments.size
Tactic:
exact insertUnit_fold_preserves_size f.ratUnits f.assignments false
State after:
no goals