obtain (h | h) := isEmpty_or_nonempty β
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
⊢ N.Simple
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ N.Simple

case inr
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : Nonempty β
⊢ N.Simple