rw [← dual_dual (M ／ C' ＼ D'), delete_dual_eq_dual_contract, hb.contract_eq_contract_delete,
  hI.contract_eq_contract_delete, delete_dual_eq_dual_contract, contract_dual_eq_dual_delete,
  dual_dual, delete_delete, contract_delete_contract]
case h.refine'_4
α : 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
hb : (M ／ C')✶.Basis K D'
⊢ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
case h.refine'_4.h
α : 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
hb : (M ／ C')✶.Basis K D'
⊢ Disjoint (D' \ K) (C' \ I ∪ K)