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

State before:
R : Type u_1
inst✝ : Ring R
r : R
h : r * r = r + 1
a b a' b' : ℤ
⊢ cast r ({ re := a, im := b } * { re := a', im := b' }) = cast r { re := a, im := b } * cast r { re := a', im := b' }
Tactic:
change ↑(a * a' + b * b') + (a * b' + a' * b + b * b') • r
  = (↑a + b • r) * (↑a' + b' • r)
State after:
R : Type u_1
inst✝ : Ring R
r : R
h : r * r = r + 1
a b a' b' : ℤ
⊢ ↑(a * a' + b * b') + (a * b' + a' * b + b * b') • r = (↑a + b • r) * (↑a' + b' • r)

State before:
R : Type u_1
inst✝ : Ring R
r : R
h : r * r = r + 1
a b a' b' : ℤ
⊢ ↑(a * a' + b * b') + (a * b' + a' * b + b * b') • r = (↑a + b • r) * (↑a' + b' • r)
Tactic:
rw [add_zsmul, Int.cast_add, add_add_add_comm, ← zsmul_one (b * b'),
  ← zsmul_add, add_comm 1 r, ← h, add_zsmul, ← add_assoc, mul_zsmul,
  zsmul_eq_mul, Int.cast_mul, ← mul_add, add_mul, add_assoc, add_right_inj,
  mul_add, ← zsmul_eq_mul', mul_zsmul, add_right_inj, mul_zsmul, zsmul_eq_mul,
  zsmul_eq_mul', zsmul_eq_mul, zsmul_eq_mul', mul_assoc, ← mul_assoc]
State after:
no goals