rw [← cl_inter_ground, hf.preimage_image_inter, hF]
case intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ f '' M.cl (f ⁻¹' (f '' F)) = f '' F
case intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f✝ : α
β : Type u_2
f : α → β
hf : InjOn f M.E
F : Set α
hF : M.cl F = F
⊢ F ⊆ M.E