Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.reduced_𝔽₂ε_iff (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ r * r = 0 ↔ f (r + 1) = 0
Tactic:
rw [reduced_eq_zero_iff hS hf, Eq2_v2 hf.toNontrivialGood,
  sub_eq_neg_self, sq_eq_zero_iff]
State after:
no goals