Theorem: IMOSL.IMO2012A5.Case3.CommCase.Thm1 (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
x : R
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
have h := Thm1_ring_id1 (f x) (f (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
x : R
h :
  f x * ((f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x) -
      f (x + 1) * ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) =
    (f x ^ 2 + f (x + 1) ^ 2 - 1) * (f x + f (x + 1) - 1) * (f x - f (x + 1))
⊢ f x ^ 2 + f (x + 1) ^ 2 = 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
x : R
h :
  f x * ((f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x) -
      f (x + 1) * ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) =
    (f x ^ 2 + f (x + 1) ^ 2 - 1) * (f x + f (x + 1) - 1) * (f x - f (x + 1))
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
rw [← Eq3 hf, ← Eq3_v2 hf, mul_left_comm, sub_self, zero_eq_mul,
  mul_eq_zero, sub_eq_zero, sub_eq_zero, sub_eq_zero] at h
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
x : R
h : (f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1) ∨ f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 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
x : R
h : (f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1) ∨ f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
cases h with | inl h => exact h | inr h => ?_
State after:
case inr
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
x : R
h : f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1

State before:
case inr
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
x : R
h : f x = f (x + 1)
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
right
State after:
case inr.h
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
x : R
h : f x = f (x + 1)
⊢ f x + f (x + 1) = 1

State before:
case inr.h
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
x : R
h : f x = f (x + 1)
⊢ f x + f (x + 1) = 1
Tactic:
rw [← h, ← two_mul]
State after:
case inr.h
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
x : R
h : f x = f (x + 1)
⊢ 2 * f x = 1

State before:
case inr.h
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
x : R
h : f x = f (x + 1)
⊢ 2 * f x = 1
Tactic:
have h0 : _ ^ 2 = _ ^ 2 := congrArg (λ x ↦ x ^ 2) (Eq3 hf x)
State after:
case inr.h
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
x : R
h : f x = f (x + 1)
h0 : (f x * f (x * x + x)) ^ 2 = ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) ^ 2
⊢ 2 * f x = 1

State before:
case inr.h
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
x : R
h : f x = f (x + 1)
h0 : (f x * f (x * x + x)) ^ 2 = ((f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)) ^ 2
⊢ 2 * f x = 1
Tactic:
rw [mul_pow, ← add_eq_of_eq_sub (Eq2 hf (x * x + x)), ← h, add_mul_self,
  ← mul_add_one (x * x), Eq1 hf, Eq2 hf, Eq2_v2 hf, ← h,
  ← sub_eq_zero, ← sq, Thm1_ring_id2, mul_eq_zero] at h0
State after:
case inr.h
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
x : R
h : f x = f (x + 1)
h0 : 1 - 2 * f x = 0 ∨ f x ^ 2 - 1 = 0
⊢ 2 * f x = 1

State before:
case inr.h
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
x : R
h : f x = f (x + 1)
h0 : 1 - 2 * f x = 0 ∨ f x ^ 2 - 1 = 0
⊢ 2 * f x = 1
Tactic:
cases h0 with | inl h0 => exact (eq_of_sub_eq_zero h0).symm | inr h0 => ?_
State after:
case inr.h.inr
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
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
⊢ 2 * f x = 1

State before:
case inr.h.inr
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
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
⊢ 2 * f x = 1
Tactic:
have h1 : f (x * x) = 0 := by rw [Eq2_v2 hf, ← h, h0]
State after:
case inr.h.inr
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
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
⊢ 2 * f x = 1

State before:
case inr.h.inr
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
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
⊢ 2 * f x = 1
Tactic:
replace h := Eq3_v2 hf (x * x)
State after:
case inr.h.inr
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
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : f (x * x + 1) * f (x * x * (x * x) + x * x) = (f (x * x) ^ 2 - 1) * (f (x * x) - 1) + f (x * x + 1) * f (x * x)
⊢ 2 * f x = 1

State before:
case inr.h.inr
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
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : f (x * x + 1) * f (x * x * (x * x) + x * x) = (f (x * x) ^ 2 - 1) * (f (x * x) - 1) + f (x * x + 1) * f (x * x)
⊢ 2 * f x = 1
Tactic:
rw [h1, mul_zero, add_zero, sq, zero_mul, zero_sub,
  neg_mul_neg, one_mul, Eq2 hf, h0, zero_mul] at h
State after:
case inr.h.inr
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
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : 0 = 1
⊢ 2 * f x = 1

State before:
case inr.h.inr
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
x : R
h0 : f x ^ 2 - 1 = 0
h1 : f (x * x) = 0
h : 0 = 1
⊢ 2 * f x = 1
Tactic:
rw [← mul_one (2 * f x), ← h, mul_zero]
State after:
no goals

State before:
case inl
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
x : R
h : f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
⊢ f x ^ 2 + f (x + 1) ^ 2 = 1 ∨ f x + f (x + 1) = 1
Tactic:
exact h
State after:
no goals

State before:
case inr.h.inl
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
x : R
h : f x = f (x + 1)
h0 : 1 - 2 * f x = 0
⊢ 2 * f x = 1
Tactic:
exact (eq_of_sub_eq_zero h0).symm
State after:
no goals

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
x : R
h : f x = f (x + 1)
h0 : f x ^ 2 - 1 = 0
⊢ f (x * x) = 0
Tactic:
rw [Eq2_v2 hf, ← h, h0]
State after:
no goals