lift k to ℕ using hk
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)
case inr.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)