obtain ⟨I, hIu, hIX, hIY, hIi⟩ := h.exists_common_basis
ι : 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
⊢ M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
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)