simp only [ge_iff_le, contract_ground, unifOn_ground_eq, diff_self_inter, subset_diff] at hS
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 ⊆ (unifOn E ↑k ／ C).E
⊢ (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
⊢ (unifOn E ↑k ／ C).Spanning S ↔ (unifOn (E \ C) (↑k - (E ∩ C).encard)).Spanning S