Theorem: Matroid.Flat.cl_eq_iff_basis_of_indep (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 : M.Flat F
hI : M.Indep I
⊢ M.cl I = F → M.Basis I F
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hI : M.Indep I
hF : M.Flat (M.cl I)
⊢ M.Basis I (M.cl I)

State before:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hI : M.Indep I
hF : M.Flat (M.cl I)
⊢ M.Basis I (M.cl I)
Tactic:
exact hI.basis_cl
State after:
no goals

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 : M.Flat F
hI : M.Indep I
h : M.Basis I F
⊢ M.cl I = F
Tactic:
rw [h.cl_eq_cl, hF.cl]
State after:
no goals