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

State before:
R : Type u_2
S : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CharTwo R
inst✝² : CommRing S
inst✝¹ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
inst✝ : CharTwo S
x : R
⊢ f (x + 1) = f x + 1
Tactic:
have h := Thm1 hf x
State after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CharTwo R
inst✝² : CommRing S
inst✝¹ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
inst✝ : CharTwo S
x : R
h : f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
⊢ f (x + 1) = f x + 1

State before:
R : Type u_2
S : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CharTwo R
inst✝² : CommRing S
inst✝¹ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
inst✝ : CharTwo S
x : R
h : f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
⊢ f (x + 1) = f x + 1
Tactic:
rwa [← CharTwo.add_sq, CharTwo.sq_eq_one_iff, or_self, add_eq_iff_eq_add''] at h
State after:
no goals