Theorem: IMOSL.IMO2012A5.ℤ₄.cast_add (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

State before:
R : Type u_1
inst✝ : NonAssocRing R
h✝ : 4 = 0
x y : ℤ₄
h : 2 + 2 = 0
h0 : 1 + 1 = 2
⊢ -1 = 1 + 2
Tactic:
rwa [neg_eq_iff_add_eq_zero, ← add_assoc, h0]
State after:
no goals