no goals
α : Type ?u.41556
β : Type ?u.41559
A✝ : Type ?u.41562
B : Type u_3
F : Type u_2
inst✝³ : AddMonoidWithOne B
inst✝² : AddMonoidWithOne A✝
A : Type u_1
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F A B
f : F
h : ↑f 1 = 1
⊢ ↑f ↑0 = ↑0
simp [map_zero f]
no goals
α : Type ?u.41556
β : Type ?u.41559
A✝ : Type ?u.41562
B : Type u_3
F : Type u_2
inst✝³ : AddMonoidWithOne B
inst✝² : AddMonoidWithOne A✝
A : Type u_1
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F A B
f : F
h : ↑f 1 = 1
n : ℕ
⊢ ↑f ↑(n + 1) = ↑(n + 1)
rw [Nat.cast_add, map_add, Nat.cast_add, map_natCast' f h n, Nat.cast_one, h, Nat.cast_one]