Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f x * (f x * f (x * 2 + 1)) = f x * ((f (x + 1) + 1) * f (x * 2 - 1))
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [← mul_assoc, ← sq, mul_left_comm, Eq4 hf h,
  ← mul_assoc, ← sub_eq_zero, ← sub_mul, mul_eq_zero] at h2
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f x ^ 2 - (f (x + 1) + 1) * (f (x - 1) + 1) = 0 ∨ f (x * 2 + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f x ^ 2 - (f (x + 1) + 1) * (f (x - 1) + 1) = 0 ∨ f (x * 2 + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rcases h2 with h2 | h2
State after:
case inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f x ^ 2 - (f (x + 1) + 1) * (f (x - 1) + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f x ^ 2 - (f (x + 1) + 1) * (f (x - 1) + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
exact (eq_of_sub_eq_zero h2).symm
State after:
case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f x * (f x * f (x * 2 - 1)) = f x * ((f (x - 1) + 1) * f (x * 2 + 1))
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [← mul_assoc, ← sq, mul_left_comm, Eq4_alt hf h,
  ← mul_assoc, ← sub_eq_zero, ← sub_mul, mul_eq_zero] at h3
State after:
case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f x ^ 2 - (f (x - 1) + 1) * (f (x + 1) + 1) = 0 ∨ f (x * 2 - 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f x ^ 2 - (f (x - 1) + 1) * (f (x + 1) + 1) = 0 ∨ f (x * 2 - 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rcases h3 with h3 | h3
State after:
case inr.inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f x ^ 2 - (f (x - 1) + 1) * (f (x + 1) + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f (x * 2 - 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f x ^ 2 - (f (x - 1) + 1) * (f (x + 1) + 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f (x * 2 - 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rwa [sub_eq_zero, eq_comm, mul_comm] at h3
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f (x * 2 - 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x * 2 + 1) = 0
h3 : f (x * 2 - 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [Eq3 hf h] at h2
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) * f 2 + f (x - 1) = 0
h3 : f (x * 2 - 1) = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) * f 2 + f (x - 1) = 0
h3 : f (x + 1) * f 2 + f (x - 1) + f (x * 2 - 1) = 0 + 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [Eq2 hf, add_add_add_comm, add_zero, ← add_mul,
  add_comm (f _), ← mul_add_one (α := S), mul_eq_zero,
  or_iff_left (h0 ∘ eq_neg_of_add_eq_zero_left), ← eq_neg_iff_add_eq_zero] at h3
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) * f 2 + f (x - 1) = 0
h3 : f (x - 1) = -f (x + 1)
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) * f 2 + f (x - 1) = 0
h3 : f (x - 1) = -f (x + 1)
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
have X : f 2 - 1 ≠ 0 := h1 ∘ eq_of_sub_eq_zero
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) * f 2 + f (x - 1) = 0
h3 : f (x - 1) = -f (x + 1)
X : f 2 - 1 ≠ 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) * f 2 + f (x - 1) = 0
h3 : f (x - 1) = -f (x + 1)
X : f 2 - 1 ≠ 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [h3, ← sub_eq_add_neg, ← mul_sub_one, mul_eq_zero, or_iff_left X] at h2
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = -f (x + 1)
X : f 2 - 1 ≠ 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = -f (x + 1)
X : f 2 - 1 ≠ 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [h2, neg_zero] at h3
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = 0
X : f 2 - 1 ≠ 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = 0
X : f 2 - 1 ≠ 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
have h4 := Eq6 hf h h0 x
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = 0
X : f 2 - 1 ≠ 0
h4 : f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = 0
X : f 2 - 1 ≠ 0
h4 : f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [h2, h3, add_zero, zero_eq_mul, or_iff_left X] at h4
State after:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = 0
X : f 2 - 1 ≠ 0
h4 : f x + 1 = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2

State before:
case inr.inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 ≠ -1
h1 : f 2 ≠ 1
x : R
h2 : f (x + 1) = 0
h3 : f (x - 1) = 0
X : f 2 - 1 ≠ 0
h4 : f x + 1 = 0
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rw [h2, h3, zero_add, one_mul, eq_neg_of_add_eq_zero_left h4, neg_one_sq]
State after:
no goals