rw [indep_iff_er_eq_encard_of_finite _]
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin I
h : I.encard ≤ M.er I
⊢ M.Indep I
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin I
h : I.encard ≤ M.er I
⊢ M.er I = I.encard

α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin I
h : I.encard ≤ M.er I
⊢ I.Finite