In a monoid, (gh)^n g = g (hg)^n

Stream: Is there code for X?

[Mitchell Lee]

Here's my proof that in a monoid, $(g h)^n g = g (h g)^n$.

import Mathlib

example {M : Type} [Monoid M] (g h : M) (n : ℕ) : (g * h) ^ n * g = g * (h * g) ^ n := by
  refine (SemiconjBy.eq (SemiconjBy.pow_right ?_ n)).symm
  unfold SemiconjBy
  group

Any easier way to do it?

[Kim Morrison]

I would probably have written

import Mathlib

example {M : Type} [Monoid M] (g h : M) (n : ℕ) : (g * h) ^ n * g = g * (h * g) ^ n := by
  induction n <;> simp_all [pow_succ, mul_assoc]