∀ {A : Type u_1} [inst : AddMonoid A] {M : Type u_2} [inst_1 : Monoid M] (toFun toFun_1 : A → M)
  (e_toFun : toFun = toFun_1) (map_zero_eq_one' : toFun 0 = 1)
  (map_add_eq_mul' : ∀ (a b : A), toFun (a + b) = toFun a * toFun b),
  { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } =
    { toFun := toFun_1, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }