case h
α : Type ?u.48928
β : Type ?u.48931
A : Type u_2
F : Type u_1
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ∀ (x : ℕ), ↑f x = ↑g x
α : Type ?u.48928
β : Type ?u.48931
A : Type u_2
F : Type u_1
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ f = g
apply FunLike.ext
case h.zero
α : Type ?u.48928
β : Type ?u.48931
A : Type u_2
F : Type u_1
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ↑f Nat.zero = ↑g Nat.zero

case h.succ
α : Type ?u.48928
β : Type ?u.48931
A : Type u_2
F : Type u_1
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
n : ℕ
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
case h
α : Type ?u.48928
β : Type ?u.48931
A : Type u_2
F : Type u_1
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ∀ (x : ℕ), ↑f x = ↑g x
rintro (_ | n)
no goals
case h.zero
α : Type ?u.48928
β : Type ?u.48931
A : Type u_2
F : Type u_1
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ↑f Nat.zero = ↑g Nat.zero
simp [map_zero f, map_zero g]
no goals
case h.succ
α : Type ?u.48928
β : Type ?u.48931
A : Type u_2
F : Type u_1
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
n : ℕ
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
exact h_pos n.succ_pos