Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.map_neg_one_ne_zero (IMOSLLean4/IMO2012/A5/A5Cases/Case1.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : f (-1) = 0
⊢ 3 = 0
Tactic:
rw [← mul_one (3 : S), ← hf.map_neg_one, h, mul_zero]
State after:
no goals