Theorem: Matroid.Basis.cl_eq_cl (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Basis I X
⊢ M.cl I = M.cl X
Tactic:
refine' subset_antisymm (M.cl_subset_cl h.subset) _
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Basis I X
⊢ M.cl X ⊆ M.cl I

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Basis I X
⊢ M.cl X ⊆ M.cl I
Tactic:
rw [← M.cl_cl I, h.indep.cl_eq_setOf_basis_insert]
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Basis I X
⊢ M.cl X ⊆ M.cl {x | M.Basis I (insert x I)}

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : M.Basis I X
⊢ M.cl X ⊆ M.cl {x | M.Basis I (insert x I)}
Tactic:
exact M.cl_subset_cl fun e he ↦ (h.basis_subset (subset_insert _ _) (insert_subset he h.subset))
State after:
no goals