obtain (rfl | hk) := eq_or_ne k ⊤
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
⊢ (unifOn E ⊤)✶ = unifOn E (E.encard - ⊤)

case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)