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

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

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