Theorem: IMOSL.IMO2012A5.Case3.Eq1 (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x * (x + 1) + 1) = f x * f (x + 1)
Tactic:
rw [hf.is_good, add_add_cancel_left, hf.map_one, add_zero]
State after:
no goals