rwa [disjoint_iff_inter_eq_empty, cl_inter_eq_of_subset_coloops X hK,
  ← disjoint_iff_inter_eq_empty]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hXK : Disjoint X K
hK : K ⊆ M✶.cl ∅
⊢ Disjoint (M.cl X) K
no goals