rw [← subset_compl_iff_disjoint_left, diff_eq, compl_inter, compl_compl]
case refine'_1
α : 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 : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ Disjoint (M.E \ X) H
case refine'_1
α : 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 : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H ⊆ M.Eᶜ ∪ X