exact hM.map hf
case inr.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
h : Nonempty β
f : α → β
hf : InjOn f M.E
i : M ≂ M.map f hf
⊢ (M.map f hf).Simple
no goals