obtain ⟨B₀, hB, rfl⟩ := h
case refine_2
α : 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 β
h : ∃ B₀, M.Base B₀ ∧ B = f '' B₀
⊢ (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
case refine_2.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.Base B₀
⊢ (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I