α : Type ?u.27138
β : Type ?u.27141
A : Type u_1
B : Type ?u.27147
F : Type u_2
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
⊢ ↑f n = ↑g n
α : Type ?u.27138
β : Type ?u.27141
A : Type u_1
B : Type ?u.27147
F : Type u_2
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ∀ (x : ℕ), ↑f x = ↑g x
intro n
no goals
α : Type ?u.27138
β : Type ?u.27141
A : Type u_1
B : Type ?u.27147
F : Type u_2
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
⊢ ↑f n = ↑g n
induction n with
| zero => simp_rw [Nat.zero_eq, map_zero f, map_zero g]
| succ n ihn =>
  simp [Nat.succ_eq_add_one, h, ihn]
no goals
case zero
α : Type ?u.27138
β : Type ?u.27141
A : Type u_1
B : Type ?u.27147
F : Type u_2
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ↑f Nat.zero = ↑g Nat.zero
simp_rw [Nat.zero_eq, map_zero f, map_zero g]
no goals
case succ
α : Type ?u.27138
β : Type ?u.27141
A : Type u_1
B : Type ?u.27147
F : Type u_2
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
ihn : ↑f n = ↑g n
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
simp [Nat.succ_eq_add_one, h, ihn]