obtain ⟨IY, hIY, hIY'⟩ :=
  hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_right)
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
case intro.intro.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
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y