simp_rw [← coe_le_er_iff, le_er_iff,]
α : 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 : ℕ
⊢ n ≤ M.r X ↔ ∃ 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 : ℕ
⊢ (∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n) ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n