rw [hI.conn_eq hJ, ← hI.encard, ← hJ.encard, ← encard_union_add_encard_inter, ← hB'.encard,
  ← (base_restrict_iff'.2 hB).encard_compl_eq, restrict_ground_eq, ← add_assoc, add_comm B.encard,
  add_assoc, add_comm B.encard, encard_diff_add_encard_of_subset hB.subset, add_comm]
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
hB' : M.Basis' B (X ∪ Y)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
no goals