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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ (unif a b).rk = min a b
Tactic:
rw [rk, unif_erk_eq, ENat.toNat_coe]
State after:
no goals