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

State before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
h0 : 2 ≠ 0
h1 : 1 = 0
⊢ 2 = 0
Tactic:
rw [← one_mul (2 : R), h1, zero_mul]
State after:
no goals