have hJX := hJ.indep.basis_of_subset_of_subset_cl (hIJ.trans hIX) 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
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
⊢ 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
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X