exact M.cl_subset_cl (insert_subset (Or.inl he₀) subset_union_right)
case intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
h₀ : F₀ ⋖[M] M.cl (insert e F₁)
h₁ : F₁ ⋖[M] M.cl (insert e F₁)
⊢ M.cl (insert e F₁) ⊆ M.cl (F₀ ∪ F₁)
no goals