rwa [← hf (hI'.indep.subset_ground hx') hx h_eq]
case intro.intro.intro.intro.intro.h.refine_2.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
x : α
hx : x ∈ M.E
h : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hind : M.Indep (insert x I)
x' : α
hx' : x' ∈ I
h_eq : f x' = f x
⊢ x ∈ I
no goals