have hnss : ¬ (F₀ ⊆ F₁) :=
  fun hss ↦ hne.symm <| h₀.eq_of_subset_of_ssubset h₁.flat_left hss h₁.ssubset
α : 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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
α : 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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)