exact ⟨hdj.mono_left hB.subset,
  hsk.union_indep_of_indep_subsets hB.indep hB.subset (hK.indep.diff _) Subset.rfl⟩
case refine_1
α : 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)
⊢ Disjoint B (K \ I) ∧ M.Indep (B ∪ K \ I)
no goals