More_than_one_Left_Identity_then_no_Right_Identity

import Mathlib.Algebra.Group.Defs

theorem More_than_one_Left_Identity_then_no_Right_Identity {α : Type _} [Mul α] (e₁ e₂ : α) (hne : e₁ ≠ e₂) (h₁ : ∀ x : α, e₁ * x = x) (h₂ : ∀ x : α, e₂ * x = x) : ¬∃ eR : α, ∀ x : α, x * eR = x := by sorry