case h
α : Type u_1
β : Type ?u.14
G : Type ?u.17
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) z = x * y * z
α : Type u_1
β : Type ?u.14
G : Type ?u.17
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) = fun x_1 => x * y * x_1
ext z
no goals
case h
α : Type u_1
β : Type ?u.14
G : Type ?u.17
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x * x_1) ∘ fun x => y * x) z = x * y * z
simp [mul_assoc]