simpa using contract_minor _ _
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ (M ↾ (N.E ∪ I)) ／ I ≤m M ↾ (((M ↾ (N.E ∪ I)) ／ I).E ∪ I)
no goals