∀ {M₁ : Type u_2} {M₂ : Type u_1} [inst : Mul M₂] [inst_1 : One M₂] [inst_2 : Pow M₂ ℕ] [inst_3 : Monoid M₁]
  (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → ∀ (x : M₁), f x ^ 0 = 1