obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans subset_union_left)
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
case intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1