rw [← relRank_inter_ground_left, ← relRank_inter_ground_right,
  hJ.basis'.relRank_eq_encard_diff hIC.basis', ← er_inter_ground_eq,
  ← hIC.encard, encard_diff_add_encard_inter, hJ.encard, ← union_inter_distrib_right,
  er_inter_ground_eq]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J✝ C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X D J : Set α
hJ : M.Basis J (X ∩ M.E ∪ C ∩ M.E)
hIC : M.Basis (J ∩ (C ∩ M.E)) (C ∩ M.E)
hD : D ⊆ (M ／ (J ∩ (C ∩ M.E))).E
hM : M ／ C = M ／ (J ∩ (C ∩ M.E)) ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
no goals