simp_rw [Spanning, contract_cl_eq, contract_ground, subset_diff, union_subset_iff,
  and_iff_left inter_subset_right, ← and_assoc, and_congr_left_iff,
  subset_antisymm_iff, subset_diff, diff_subset_iff, and_iff_left disjoint_sdiff_left,
  and_iff_right (M.cl_subset_ground _ ),
  and_iff_right (subset_union_of_subset_right (M.cl_subset_ground _) 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 ／ C).Spanning X ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint 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 α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ C ∪ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C ∩ M.E))