simp [hE]
α : 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
⊢ (M₁ ＼ e).E = (M₂ ＼ e).E
no goals