rw [ncard_insert_of_not_mem hIc₁.1 (hIc₁.2.subset (subset_insert _ _)).finite,
  ← insert_union] at hcon
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
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : (insert e Ic).ncard + 1 ≤ M₁.r (insert e (Xc ∪ Xd)) + M₂.r (M₂.E \ insert e (Xc ∪ 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
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
⊢ False