rw [← cl_inter_ground] at hXI
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
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X
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
hXI : X ⊆ M.cl (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X