S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')
unfold SemiconjBy
no goals
S : Type u_1
inst✝ : Semigroup S
a b x y z x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a
rw [←mul_assoc, h.eq, mul_assoc, h'.eq, ←mul_assoc]