obtain (hle | hlt) := le_or_lt 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)
case inr.intro.inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hle : E.encard ≤ ↑k
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)

case inr.intro.inr
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)