rw [← hI.eq_of_subset_of_encard_le hJ.subset]
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep I
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep J

case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ I.encard ≤ J.encard