rw [← hKE, ← inter_assoc X, inter_right_comm, hKE, ← cl_inter_ground,
  subset_antisymm_iff, and_iff_left (inter_subset_inter_left K (M.subset_cl _)),
  ← inter_eq_self_of_subset_right hK, ← inter_assoc, cl_inter_coloops_eq,
  inter_assoc]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
hKE : K ∩ M.E = K
⊢ M.cl X ∩ K = X ∩ K
no goals