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

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) ≠ 0
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : ¬f (-1) = -2
h1 : f (-1) = 1
⊢ 3 ≠ 0
Tactic:
rwa [← two_add_one_eq_three, Ne,
← neg_eq_iff_add_eq_zero, ← h1, eq_comm]
State after:
no goals