exact hCD'.symm
α : 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
⊢ Disjoint D' C'
no goals