rw [erk_eq_er_ground, unif_er_eq]
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ (unif a b).erk = ↑(min a b)
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min (unif a b).E.encard ↑a = ↑(min a b)