rwa [freeOn_erk_eq, encard_univ, PartENat.card_eq_coe_fintype_card, Fintype.card_fin,
  PartENat.withTopEquiv_natCast, Nat.cast_le]
α : 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
no goals