Theorem: IMOSL.IMO2012A5.ℤφ.mul_assoc (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/Zphi.lean)

State before:
a b a' b' a'' b'' : ℤ
⊢ { re := a, im := b } * { re := a', im := b' } * { re := a'', im := b'' } =
    { re := a, im := b } * ({ re := a', im := b' } * { re := a'', im := b'' })
Tactic:
rw [mul_def, mul_def, mul_def, mul_def, ℤφ.mk.injEq]
State after:
a b a' b' a'' b'' : ℤ
⊢ { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * a'' +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im ∧
    { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * b'' +
          a'' * { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im +
          { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re * b +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im

State before:
a b a' b' a'' b'' : ℤ
⊢ { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * a'' +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im ∧
    { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * b'' +
          a'' * { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im +
          { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re * b +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im
Tactic:
dsimp only
State after:
a b a' b' a'' b'' : ℤ
⊢ (a * a' + b * b') * a'' + (a * b' + a' * b + b * b') * b'' =
      a * (a' * a'' + b' * b'') + b * (a' * b'' + a'' * b' + b' * b'') ∧
    (a * a' + b * b') * b'' + a'' * (a * b' + a' * b + b * b') + (a * b' + a' * b + b * b') * b'' =
      a * (a' * b'' + a'' * b' + b' * b'') + (a' * a'' + b' * b'') * b + b * (a' * b'' + a'' * b' + b' * b'')

State before:
a b a' b' a'' b'' : ℤ
⊢ (a * a' + b * b') * a'' + (a * b' + a' * b + b * b') * b'' =
      a * (a' * a'' + b' * b'') + b * (a' * b'' + a'' * b' + b' * b'') ∧
    (a * a' + b * b') * b'' + a'' * (a * b' + a' * b + b * b') + (a * b' + a' * b + b * b') * b'' =
      a * (a' * b'' + a'' * b' + b' * b'') + (a' * a'' + b' * b'') * b + b * (a' * b'' + a'' * b' + b' * b'')
Tactic:
constructor <;> ring
State after:
no goals