M : Type ?u.84938
N : Type ?u.84941
G : Type u_1
H : Type ?u.84947
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ a * (b * j) = c * (a * j)
M : Type ?u.84938
N : Type ?u.84941
G : Type u_1
H : Type ?u.84947
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x => a * x) ((fun x => b * x) j) = (fun x => c * x) ((fun x => a * x) j)
dsimp only
no goals
M : Type ?u.84938
N : Type ?u.84941
G : Type u_1
H : Type ?u.84947
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ a * (b * j) = c * (a * j)
rw [← mul_assoc, h.eq, mul_assoc]