Theorem: Matroid.simplification_factorsThrough_removeLoops (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝¹ x✝ : Matroid α
h : x✝¹.removeLoops = x✝.removeLoops
⊢ x✝¹.simplification = x✝.simplification
Tactic:
rw [simplification, h, simplification]
State after:
no goals