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

State before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ 2 + 2 = 0
Tactic:
rw [← h, ← Nat.cast_two, ← Nat.cast_add]
State after:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ ↑(2 + 2) = 4

State before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ ↑(2 + 2) = 4
Tactic:
rfl
State after:
no goals