rw [← inter_eq_left (s := M.E), inter_union_distrib_left,
  inter_eq_self_of_subset_right (M.cl_subset_ground _), subset_antisymm_iff, union_subset_iff,
  and_iff_right inter_subset_left, union_eq_self_of_subset_left (s := M.E ∩ C),
  and_iff_right (M.cl_subset_ground _), Iff.comm, ← cl_union_cl_right_eq,cl_inter_ground,
  cl_union_cl_right_eq]
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ C ∪ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C ∩ M.E))
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C))

α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ M.E ∩ C ⊆ M.cl (X ∪ C)