rw [unifOn_eq_of_le hle, freeOn_dual_eq, tsub_eq_zero_of_le hle, unifOn_zero]
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)
no goals