exact ⟨fun h ↦ (hI h).elim, hIE⟩
case refine_2.inl.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
no goals