Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_assignments_size (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.assignments.size = f.assignments.size
Tactic:
simp only [insertRupUnits, Prod.mk.eta]
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.rupUnits, 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.rupUnits, f.assignments, false) units).2.fst.size = f.assignments.size
Tactic:
exact insertUnit_fold_preserves_size f.rupUnits f.assignments false
State after:
no goals