rw [← contract_inter_ground_eq, unifOn_ground_eq, inter_comm,
  contract_spanning_iff, unifOn_spanning_iff', unifOn_spanning_iff', tsub_le_iff_right,
  iff_true_intro (disjoint_of_subset_right inter_subset_right hS.2), and_true,
   ← encard_union_eq (disjoint_of_subset_right inter_subset_right hS.2), union_subset_iff,
  and_iff_left inter_subset_left, and_iff_left hS.1, subset_diff, union_inter_distrib_left,
  and_iff_left hS, union_eq_self_of_subset_left hS.1, inter_eq_left,
  subset_antisymm_iff, subset_diff, and_iff_right hS, diff_subset_iff, union_comm C]
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ (unifOn E ↑k ／ C).Spanning S ↔ (unifOn (E \ C) (↑k - (E ∩ C).encard)).Spanning S
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ ↑k - (E ∩ C).encard ≠ ⊤

case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ ↑k ≠ ⊤