no goals
α : Type ?u.36144
β : Type ?u.36147
A : Type u_2
B : Type ?u.36153
F : Type u_1
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : ↑f 1 = 1
⊢ ↑f 0 = ↑0
simp [map_zero f]
no goals
α : Type ?u.36144
β : Type ?u.36147
A : Type u_2
B : Type ?u.36153
F : Type u_1
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : ↑f 1 = 1
n : ℕ
⊢ ↑f (n + 1) = ↑(n + 1)
rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]