obtain ⟨I, D, hIC, hD, -, hM⟩ := M.exists_eq_contract_indep_delete C
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X : Set α
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
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)