obtain ⟨M₀, hM₀, ⟨i, -⟩⟩ := e.exists_iso
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
⊢ Nonempty (N ≤i M.simplification)
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ Nonempty (N ≤i M.simplification)