∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : SMul ℕ M₂] [inst_3 : AddMonoid M₁]
  (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Surjective.addMonoid f hf one mul npow =
    { toAddSemigroup := Function.Surjective.addSemigroup f hf mul,
      toZero := (Function.Surjective.addZeroClass f hf one mul).toZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n x => n • x, nsmul_zero := ⋯, nsmul_succ := ⋯ }