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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
⊢ M.simplification = M
Tactic:
rwa [IsSimplification.eq_self_iff M.simplification_isSimplification]
State after:
no goals