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

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