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

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

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