[GOAL]
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)
[PROOFSTEP]
simpa only [SemiconjBy, map_mul] using congr_arg f h
[GOAL]
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
f : F
hf : Function.Injective ↑f
h : SemiconjBy (↑f a) (↑f x) (↑f y)
⊢ ↑f (a * x) = ↑f (y * a)
[PROOFSTEP]
simpa only [SemiconjBy, map_mul] using h
[GOAL]
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
f : F
hf : Function.Injective ↑f
h : Commute (↑f x) (↑f y)
⊢ ↑f (x * y) = ↑f (y * x)
[PROOFSTEP]
simpa only [map_mul] using h.eq
