rw [preimage_inter, eq_comm, ← cl_inter_ground, inter_assoc, hf.preimage_image_inter Subset.rfl,
  cl_inter_ground]
case h.e'_3
α : 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
X : Set β
h' : ∀ X ⊆ f '' M.E, (M.map f hf).cl X = f '' M.cl (f ⁻¹' X)
⊢ f '' M.cl (f ⁻¹' X) = f '' M.cl (f ⁻¹' (X ∩ f '' M.E))
no goals