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

State before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ cast r 0 = 0
Tactic:
change ((0 : ℤ) : R) + 0 • r = 0
State after:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑0 + 0 • r = 0

State before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑0 + 0 • r = 0
Tactic:
rw [Int.cast_zero, zero_add, zero_zsmul]
State after:
no goals