Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6 (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 : ∀ (x : R), f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)
⊢ ∀ (x : R), f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
intro x
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 : ∀ (x : R), f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)
x : R
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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 : ∀ (x : R), f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)
x : R
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
refine (h1 x).elim id λ 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 : ∀ (x : R), f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)
x : R
h2 : f (x + 1) = f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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 : ∀ (x : R), f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)
x : R
h2 : f (x + 1) = f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
specialize h1 (x + 1)
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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 1 + 1) + f (x + 1 - 1) = (f (x + 1) + 1) * (f 2 - 1) ∨ f (x + 1 + 1) = f (x + 1 - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 1 + 1) + f (x + 1 - 1) = (f (x + 1) + 1) * (f 2 - 1) ∨ f (x + 1 + 1) = f (x + 1 - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [add_sub_cancel_right, add_assoc, one_add_one_eq_two] at h1
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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1) ∨ f (x + 2) = f x
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1) ∨ f (x + 2) = f x
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rcases h1 with h1 | h1
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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h1 : f x * f (x * 2 - 1) - f x * f (x * 2 + 1) = (f (x - 1) + 1) * f (x * 2 + 1) - (f (x + 1) + 1) * f (x * 2 - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)
Tactic:
rw [Eq2 hf, Eq3 hf h, ← sub_eq_zero, Eq6_ring_id, mul_eq_zero] at h1
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
x : R
h1 : f (x + 1) + f (x - 1) - (f x + 1) * (f 2 - 1) = 0 ∨ f (x + 1) - f (x - 1) = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)

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
x : R
h1 : f (x + 1) + f (x - 1) - (f x + 1) * (f 2 - 1) = 0 ∨ f (x + 1) - f (x - 1) = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1) ∨ f (x + 1) = f (x - 1)
Tactic:
exact h1.imp eq_of_sub_eq_zero eq_of_sub_eq_zero
State after:
no goals

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
have h2 := Eq3 hf h x
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
x : R
h2✝ : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1)
h2 : f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2✝ : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1)
h2 : f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [hf.is_good, eq_sub_of_add_eq h1, add_sub_left_comm, ← mul_sub_one,
  add_one_mul (f _), add_assoc, ← one_add_mul (f x), mul_sub_one,
  ← add_sub_right_comm, add_sub_assoc, add_right_inj, add_comm] at 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
x : R
h2✝ : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1)
h2 : (f x + 1) * (f 2 - 1) - f (x + 1) = f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2✝ : f (x + 1) = f (x - 1)
h1 : f (x + 2) + f x = (f (x + 1) + 1) * (f 2 - 1)
h2 : (f x + 1) * (f 2 - 1) - f (x + 1) = f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
exact (eq_add_of_sub_eq' h2).symm
State after:
no goals

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
have h0 : f 2 + 1 ≠ 0 := λ X ↦ h0 (eq_neg_of_add_eq_zero_left X)
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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
have h3 := Eq3 hf h x
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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [← h2, hf.is_good, h1, ← mul_add_one (f x), ← mul_add_one (f _),
  ← sub_eq_zero, ← sub_mul, mul_eq_zero, or_iff_left h0, sub_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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f x = f (x + 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f x = f (x + 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
have h4 := Eq4 hf h x
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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f x = f (x + 1)
h4 : f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f x = f (x + 1)
h4 : f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [Eq3 hf h, Eq2 hf, ← h2, ← h3, ← sub_eq_zero, ← sub_mul, sub_add_cancel_left,
  neg_one_mul, neg_eq_zero, ← mul_add_one (f x), mul_eq_zero, or_iff_left h0] at h4
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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f x = f (x + 1)
h4 : f x = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f x = f (x + 1)
h4 : f x = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [eq_comm, h4] 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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x + 1) = f (x - 1)
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [eq_comm, h3] at h2
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
x : R
h2 : f (x - 1) = 0
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x - 1) = 0
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
have h5 := Eq5 hf h h4 h3 0
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
x : R
h2 : f (x - 1) = 0
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
h5 : f (0 + (2 * x + 1)) = f 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x - 1) = 0
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
h5 : f (0 + (2 * x + 1)) = f 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [zero_add, hf.is_good, add_comm 2 x, h1, h4, mul_zero,
  add_zero, hf.map_zero, eq_comm, neg_eq_zero] at h5
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
x : R
h2 : f (x - 1) = 0
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
h5 : 1 = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)

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
x : R
h2 : f (x - 1) = 0
h1 : f (x + 2) = f x
h0 : f 2 + 1 ≠ 0
h3 : f (x + 1) = 0
h4 : f x = 0
h5 : 1 = 0
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rw [← sub_eq_zero, ← one_mul (_ - _), h5, zero_mul]
State after:
no goals