Theorem: Matroid.cl_disjoint_of_disjoint_of_subset_coloops (Matroid/Loop.lean)

State before:
α : 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
Tactic:
rwa [disjoint_iff_inter_eq_empty, cl_inter_eq_of_subset_coloops X hK,
  ← disjoint_iff_inter_eq_empty]
State after:
no goals