refine ⟨fun ⟨e⟩ ↦ ?_, fun ⟨e⟩ ↦ ⟨e.trans M.simplification_restriction.minor.isoMinor⟩⟩
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
⊢ Nonempty (N ≤i M) ↔ Nonempty (N ≤i M.simplification)
α : 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)