Theorem: IMOSL.IMO2012A5.Case3.CommCase.SCharNeTwo_cases (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
h : 2 ≠ 0
x : R
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
have h0 := pow_four_Eq2 hf (x * (x + 1))
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
h : 2 ≠ 0
x : R
h0 : f (((x * (x + 1)) ^ 2) ^ 2 + 1) = (f (x * (x + 1) + 1) ^ 2 - 1) ^ 2 - 1
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -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
h : 2 ≠ 0
x : R
h0 : f (((x * (x + 1)) ^ 2) ^ 2 + 1) = (f (x * (x + 1) + 1) ^ 2 - 1) ^ 2 - 1
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
rw [Eq1 hf, mul_pow, mul_pow, add_one_sq, add_one_sq, Eq1 hf, pow_four_Eq1 hf,
  pow_four_Eq2 hf, ← sub_eq_zero, mul_pow, SCharNeTwo_main_ring_id, mul_eq_zero,
  or_iff_right h, mul_eq_zero, ← mul_pow, sq_eq_zero_iff] at h0
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
h : 2 ≠ 0
x : R
h0 : f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -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
h : 2 ≠ 0
x : R
h0 : f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
revert h0
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
h : 2 ≠ 0
x : R
⊢ f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0 →
    (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -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
h : 2 ≠ 0
x : R
⊢ f x * f (x + 1) = 0 ∨ 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0 →
    (f x = 0 ∨ f (x + 1) = 0) ∨ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
refine Or.imp mul_eq_zero.mp λ h0 ↦ ?_
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
h : 2 ≠ 0
x : R
h0 : 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -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
h : 2 ≠ 0
x : R
h0 : 2 + 1 - (f x ^ 2 + f (x + 1) ^ 2) = 0
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
rw [sub_eq_zero, eq_comm] at h0
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
⊢ f x + f (x + 1) = 1 ∧ f x * f (x + 1) = -1
Tactic:
refine (Thm1 hf x).elim (λ h1 ↦ Not.elim h ?_) (λ h1 ↦ ⟨h1, ?_⟩)
State after:
case refine_1
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x ^ 2 + f (x + 1) ^ 2 = 1
⊢ 2 = 0

case refine_2
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x + f (x + 1) = 1
⊢ f x * f (x + 1) = -1

State before:
case refine_2
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x + f (x + 1) = 1
⊢ f x * f (x + 1) = -1
Tactic:
apply congrArg (λ y ↦ y ^ 2) at h1
State after:
case refine_2
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : (f x + f (x + 1)) ^ 2 = 1 ^ 2
⊢ f x * f (x + 1) = -1

State before:
case refine_2
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : (f x + f (x + 1)) ^ 2 = 1 ^ 2
⊢ f x * f (x + 1) = -1
Tactic:
rw [one_pow, add_sq', h0, add_right_comm, add_left_eq_self,
   mul_assoc, ← mul_one_add (2 : S), mul_eq_zero] at h1
State after:
case refine_2
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : 2 = 0 ∨ 1 + f x * f (x + 1) = 0
⊢ f x * f (x + 1) = -1

State before:
case refine_2
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : 2 = 0 ∨ 1 + f x * f (x + 1) = 0
⊢ f x * f (x + 1) = -1
Tactic:
exact eq_neg_of_add_eq_zero_right (h1.resolve_left h)
State after:
no goals

State before:
case refine_1
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
h : 2 ≠ 0
x : R
h0 : f x ^ 2 + f (x + 1) ^ 2 = 2 + 1
h1 : f x ^ 2 + f (x + 1) ^ 2 = 1
⊢ 2 = 0
Tactic:
rwa [h0, add_left_eq_self] at h1
State after:
no goals