rw [delete_elem_r_eq _ hXd.2, delete_elem_r_eq _ (by simp), deleteElem, delete_ground,
  diff_diff_comm, diff_diff, union_singleton] at hId
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑((M₁ ＼ e).r Xd) + ↑((M₂ ＼ e).r ((M₂ ＼ e).E \ Xd))
hIc : ↑Ic.ncard = ↑(M₁.r (insert e Xc)) - 1 + (↑(M₂.r (M₂.E \ Xc)) - 1)
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑(M₁.r Xd) + ↑(M₂.r (M₂.E \ insert e Xd))
hIc : ↑Ic.ncard = ↑(M₁.r (insert e Xc)) - 1 + (↑(M₂.r (M₂.E \ Xc)) - 1)
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False