obtain ⟨IX, hIX, hIX'⟩ :=
  hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_left)
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
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 : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y