no goals
M : Type u_2
inst✝² : Monoid M
s✝ : Set M
A : Type ?u.26765
inst✝¹ : AddMonoid A
t : Set A
γ : Type u_1
inst✝ : Monoid γ
f : M → γ
hf : IsMonoidHom f
s : Set M
hs : IsSubmonoid s
a b : γ
x✝¹ : a ∈ f '' s
x✝ : b ∈ f '' s
x : M
hx : x ∈ s ∧ f x = a
y : M
hy : y ∈ s ∧ f y = b
⊢ f (x * y) = a * b
rw [hf.map_mul, hx.2, hy.2]