Theorem: Matroid.Flat.map (Matroid/Flat.lean)

State before:
α : 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 : M.Flat F
hf : InjOn f M.E
⊢ (M.map f hf).Flat (f '' F)
Tactic:
rw [flat_iff_cl_self, map_cl_eq, ← cl_inter_ground, hf.preimage_image_inter hF.subset_ground,
  hF.cl]
State after:
no goals