no goals
α : Type ?u.42893
β : Type ?u.42896
M : Type u_2
N : Type u_3
P : Type ?u.42905
G : Type ?u.42908
H : Type ?u.42911
F : Type u_1
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ ↑f a * ↑f b = 1
rw [← map_mul, h, map_one]