Theorem: Matroid.unif_erk_eq_of_le (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
⊢ (unif a b).erk = ↑a
Tactic:
simpa
State after:
no goals