rw [← hIX.er_eq_er_union, union_comm, ← hIY.er_eq_er_union, ← hIi.encard, ← hIX.encard,
  ← hIY.encard, union_comm, ← encard_union_add_encard_inter, add_comm]
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
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 (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard