obtain ⟨J, hJ, rfl⟩ := hIC.exists_basis_inter_eq_of_superset
  (subset_union_right (s := X ∩ M.E)) (by simp)
case 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 I D : Set α
hIC : M.Basis I (C ∩ M.E)
hD : D ⊆ (M ／ I).E
hM : M ／ C = M ／ I ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
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)