rw [← delete_dual_eq_dual_contract, ← contract_dual_eq_dual_delete] at hss
case h.refine'_1
α : Type u_1
M M' : Matroid α
e f : α
I✝ J R B X Y Z K✝ : Set α
M₀ M₁ M₂ : Matroid α
C' D' : Set α
hC' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M✶ ／ K ＼ I).cl ∅
⊢ M.Indep (I ∪ D' \ K)
case h.refine'_1
α : Type u_1
M M' : Matroid α
e f : α
I✝ J R B X Y Z K✝ : Set α
M₀ M₁ M₂ : Matroid α
C' D' : Set α
hC' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M ＼ K ／ I)✶.cl ∅
⊢ M.Indep (I ∪ D' \ K)