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

State before:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
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' : ℤ) : R) + (b + b') • r = _
State after:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑(a + a') + (b + b') • r = cast r { re := a, im := b } + cast r { re := a', im := b' }

State before:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑(a + a') + (b + b') • r = cast r { re := a, im := b } + cast r { re := a', im := b' }
Tactic:
rw [Int.cast_add, add_zsmul, add_add_add_comm]
State after:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑a + b • r + (↑a' + b' • r) = cast r { re := a, im := b } + cast r { re := a', im := b' }

State before:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑a + b • r + (↑a' + b' • r) = cast r { re := a, im := b } + cast r { re := a', im := b' }
Tactic:
rfl
State after:
no goals