no goals
F : Type u_1
M : Type u_2
N : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
a x y : M
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy (↑f a) (↑f x) (↑f y)
simpa only [SemiconjBy, map_mul] using congr_arg f h