rintro ⟨D₀, ⟨hD₀, hD₀E⟩, rfl⟩
case mpr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D : Set β
⊢ (∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀) → (∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
⊢ (∀ (x : Set α), M.Indep x → ¬f '' D₀ = f '' x) ∧ ∃ u ⊆ M.E, f '' u = f '' D₀