exact M.cl_subset_cl subset_union_right
α : 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ M.cl (P ∪ C)
no goals