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' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ (unif a b).Base B ↔ B.encard = ↑a
Tactic:
rw [unif, unifOn, truncateTo_base_iff, freeOn_indep_iff, and_iff_right (subset_univ _)]
State after:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ ↑a ≤ (freeOn univ).erk

State before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ ↑a ≤ (freeOn univ).erk
Tactic:
rwa [freeOn_erk_eq, encard_univ, PartENat.card_eq_coe_fintype_card, Fintype.card_fin,
  PartENat.withTopEquiv_natCast, Nat.cast_le]
State after:
no goals