Theorem: Matroid.flat_iff_subset_cl_self (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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.Flat F ↔ M.cl F ⊆ F
Tactic:
rw [flat_iff_cl_self, subset_antisymm_iff, and_iff_left_iff_imp]
State after:
α : 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 → F ⊆ M.cl F

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 : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F ⊆ F → F ⊆ M.cl F
Tactic:
exact fun _ ↦ M.subset_cl F
State after:
no goals