∀ (M : Type u_4) [inst : AddZero M],
  AddMonoid.End.instMonoid M =
    { mul := AddMonoidHom.comp, mul_assoc := ⋯, one := AddMonoidHom.id M, one_mul := ⋯, mul_one := ⋯,
      npow := fun n f => AddMonoidHom.copy (npowRec n f) (⇑f)^[n] ⋯, npow_zero := ⋯, npow_succ := ⋯ }