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

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