no goals
α : Type ?u.345545
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✝ : Monoid M
f g : Multiplicative ℕ →* M
h : ↑f (↑Multiplicative.ofAdd 1) = ↑g (↑Multiplicative.ofAdd 1)
n : Multiplicative ℕ
⊢ ↑f n = ↑g n
rw [f.apply_mnat, g.apply_mnat, h]