rwa [← Finite.eq_of_subset_of_encard_le' (hX.finite_of_basis hJX) hIJ hI]
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X
no goals