Theorem: Matroid.ModularPair.er_add_er (Matroid/Modular.lean)

State before:
ι : 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)
Tactic:
obtain ⟨I, hIu, hIX, hIY, hIi⟩ := h.exists_common_basis
State after:
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)

State before:
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)
Tactic:
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]
State after:
no goals