Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Rchar' (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_1
S : Type ?u.112996
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 2 = -1
Tactic:
rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf h]
State after:
no goals