rfl
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ ↑(toNat I.encard) = ↑I.ncard
no goals