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

State before:
R : Type u_1
S : Type ?u.155523
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ ((r + 1) * (r + 1) = 0 ∨ r * r = 0) ∨ r * (r + 1) + 1 = 0
Tactic:
rw [reduced_𝔽₂ε_iff hS hf, reduced_𝔽₂ε_iff hS hf,
  reduced_𝔽₄_iff hS hf, add_add_cancel_right]
State after:
R : Type u_1
S : Type ?u.155523
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ (f r = 0 ∨ f (r + 1) = 0) ∨ f r + f (r + 1) = 1 ∧ f r * f (r + 1) = -1

State before:
R : Type u_1
S : Type ?u.155523
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
⊢ (f r = 0 ∨ f (r + 1) = 0) ∨ f r + f (r + 1) = 1 ∧ f r * f (r + 1) = -1
Tactic:
exact main_cases hS hf.toNontrivialGood r
State after:
no goals