Theorem: Matroid.unif_base_iff' (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
⊢ (unif a (a + b)).Base B ↔ B.encard = ↑a
Tactic:
rw [unif_base_iff (Nat.le_add_right _ _)]
State after:
no goals