simp only [flat_iff_cl_self, map_cl_eq]
α : 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 β
⊢ (M.map f hf).Flat F ↔ ∃ F₀, M.Flat F₀ ∧ F = f '' F₀
α : 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 β
⊢ f '' M.cl (f ⁻¹' F) = F ↔ ∃ F₀, M.cl F₀ = F₀ ∧ F = f '' F₀