Theorem: IMOSL.IMO2012A5.Case1.map_two (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 : NontrivialGood f
h : f (-1) ≠ 0
⊢ f 2 = 1
Tactic:
rw [← zero_add 2, ← neg_inj, ← Eq2 hf h, neg_zero, hf.map_zero]
State after:
no goals