Let's say you frequently need to solve equalities on monoids, and you find yourself proving lots of goals like the following:
example [Monoid α]: ∀ (a b c d : α),
a * b * c * d * 1 = a * (b * c) * (1 * 1 * d) := by
intros a b c d
rw [mul_one]
rw [mul_one …