α : Type ?u.21
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
f : ℕ →+ A :=
  { toZeroHom := { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) },
    map_add' := (_ : ∀ (a a_1 : ℕ), (a + a_1) • 1 = a • 1 + a_1 • 1) }
⊢ ∀ (n : ℕ), n • 1 = ↑n
α : Type ?u.21
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
⊢ ∀ (n : ℕ), n • 1 = ↑n
let f : ℕ →+ A :=
{ toFun := fun n ↦ n • (1 : A),
  map_zero' := by simp [zero_nsmul],
  map_add' := by simp [add_nsmul] }
α : Type ?u.21
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
f : ℕ →+ A :=
  { toZeroHom := { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) },
    map_add' := (_ : ∀ (a a_1 : ℕ), (a + a_1) • 1 = a • 1 + a_1 • 1) }
⊢ ↑f 1 = 1
α : Type ?u.21
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
f : ℕ →+ A :=
  { toZeroHom := { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) },
    map_add' := (_ : ∀ (a a_1 : ℕ), (a + a_1) • 1 = a • 1 + a_1 • 1) }
⊢ ∀ (n : ℕ), n • 1 = ↑n
refine' eq_natCast' f _
no goals
α : Type ?u.21
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
f : ℕ →+ A :=
  { toZeroHom := { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) },
    map_add' := (_ : ∀ (a a_1 : ℕ), (a + a_1) • 1 = a • 1 + a_1 • 1) }
⊢ ↑f 1 = 1
simp
no goals
α : Type ?u.21
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
⊢ (fun n => n • 1) 0 = 0
simp [zero_nsmul]
no goals
α : Type ?u.21
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : AddMonoidWithOne A
⊢ ∀ (x y : ℕ),
    ZeroHom.toFun { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) } (x + y) =
      ZeroHom.toFun { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) } x +
        ZeroHom.toFun { toFun := fun n => n • 1, map_zero' := (_ : 0 • 1 = 0) } y
simp [add_nsmul]