refine ⟨fun ⟨I, hIX, hI, hc⟩ ↦ ⟨I, hIX, hI, by rw [ncard_def, hc, toNat_coe]⟩,
  fun ⟨I, hIX, hI, hc⟩ ↦ ⟨I, hIX, hI, ?_⟩⟩
α : 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 : ℕ
⊢ (∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n) ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
α : 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
⊢ I.encard = ↑n