specialize hB (f '' J) ((map_image_indep_iff hJ.subset_ground).2 hJ) (image_subset _ hB₀J)
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
hB : f '' B₀ = f '' J
⊢ B₀ = J