rw [hcard, ← hJ.er_eq_encard, er_inter_ground_eq ]
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ J.encard ≤ I.encard
no goals