Theorem: IMOSL.IMO2012A5.ℤφ.mul_add (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 } * { re := a'', im := b'' }
Tactic:
rw [mul_def, mul_def, mul_def, add_def, add_def, ℤφ.mk.injEq]
State after:
a b a' b' a'' b'' : ℤ
⊢ a * { re := a' + a'', im := b' + b'' }.re + b * { re := a' + a'', im := b' + b'' }.im =
      a * a' + b * b' + (a * a'' + b * b'') ∧
    a * { re := a' + a'', im := b' + b'' }.im + { re := a' + a'', im := b' + b'' }.re * b +
        b * { re := a' + a'', im := b' + b'' }.im =
      a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')

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

State before:
a b a' b' a'' b'' : ℤ
⊢ a * (a' + a'') + b * (b' + b'') = a * a' + b * b' + (a * a'' + b * b'') ∧
    a * (b' + b'') + (a' + a'') * b + b * (b' + b'') = a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Tactic:
constructor
State after:
case left
a b a' b' a'' b'' : ℤ
⊢ a * (a' + a'') + b * (b' + b'') = a * a' + b * b' + (a * a'' + b * b'')

case right
a b a' b' a'' b'' : ℤ
⊢ a * (b' + b'') + (a' + a'') * b + b * (b' + b'') = a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')

State before:
case left
a b a' b' a'' b'' : ℤ
⊢ a * (a' + a'') + b * (b' + b'') = a * a' + b * b' + (a * a'' + b * b'')
Tactic:
rw [add_add_add_comm, ← mul_add, ← mul_add]
State after:
no goals

State before:
case right
a b a' b' a'' b'' : ℤ
⊢ a * (b' + b'') + (a' + a'') * b + b * (b' + b'') = a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Tactic:
rw [add_add_add_comm, ← mul_add, add_add_add_comm, ← mul_add, ← add_mul]
State after:
no goals