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

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.rupUnits = f.rupUnits
Tactic:
simp only [performRupCheck, Misc.Prod.mk.eta]
State after:
no goals