no goals
α : Type ?u.239358
G : Type ?u.239361
M✝ : Type ?u.239364
R : Type u_1
A : Type ?u.239370
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
m n : R
hm : m ∈ M
hn : n ∈ N
⊢ ↑(↑AddMonoidHom.mul ↑{ val := m, property := hm }) n = m * n
rfl