rw [contract_cl_eq, subset_diff, disjoint_union_left, and_iff_left disjoint_sdiff_left,
  and_iff_left (hdj.mono_left hB.subset), ← cl_union_cl_left_eq, hB.cl_eq_cl, cl_cl,
  cl_union_cl_left_eq, union_diff_self, union_eq_self_of_subset_left hIK, hK.cl_eq_cl]
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ (M ／ (K \ I)).cl B
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ M.cl (I ∪ J)