Theorem: Matroid.flat_iff_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 : α
h : M.cl F = F
⊢ M.Flat F
Tactic:
rw [← h]
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 : α
h : M.cl F = F
⊢ M.Flat (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 : α
h : M.cl F = F
⊢ M.Flat (M.cl F)
Tactic:
exact cl_flat _ _
State after:
no goals