rw [flat_iff_cl_self]
α : 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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.Flat F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ 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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F = F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F