rw [hIi.er_eq_encard, hIu.er_eq_encard, hIX.er_eq_encard, hIY.er_eq_encard,
  ← encard_union_add_encard_inter, ← inter_union_distrib_left, ← inter_inter_distrib_left,
  ← inter_assoc, inter_eq_self_of_subset_left hIu.subset, add_comm]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.ModularPair X Y
I : Set α
hIu : M.Basis I (X ∪ Y)
hIX : M.Basis (I ∩ X) X
hIY : M.Basis (I ∩ Y) Y
hIi : M.Basis (I ∩ X ∩ Y) (X ∩ Y)
⊢ M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
no goals