Using mul_assoc on middle values

Stream: new members

[Shadman Sakib]

Hi, how would I manipulate mul_assoc to encapsulate the middle values of an equation in parenthesis?

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric

lemma mid_mul_assoc (a b c d: ℂ) : a * b * c * d  = a * (b * c) * d :=
begin
  sorry,
end

[Adam Topaz]

When rewriting, you can use mul_assoc a b c to specify exactly what three variables to apply the lemma to. I would just use simp [mul_assoc] to associate everything in sight, and that should close the goal

[Shadman Sakib]

Ahh okay, thank you!

[Yakov Pechersky]

There is also the tactic ac_refl, which uses available associativity lemmas to find a rfl proof. Underused in mathlib