internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq7
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Rtwo_ne_zero
Proof state before:
R : Type u_1
S : Type ?u.70700
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : 2 = 0
⊢ f 2 = -1
Tactic:
rw [h, hf.map_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
c : R
⊢ ∃ R' x φ,
    ∃ (_ : Function.Injective ⇑φ) (_ : c ∈ Set.range ⇑φ),
      ∃ S' x_3,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ f', ∃ (_ : ∀ (a : R'), f (φ a) = ρ (f' a)), GoodCase2 f'
Tactic:
rcases CommSubring.oneVarCommLiftDomain_exists hf.toNontrivialGood c with
  ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f', h0, hf'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ f', ∃ (_ : ∀ (a : R'_1), f (φ_1 a) = ρ (f' a)), GoodCase2 f'
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ f', ∃ (_ : ∀ (a : R'_1), f (φ_1 a) = ρ (f' a)), GoodCase2 f'
Tactic:
refine ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f', h0, hf', ?_, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 ≠ -1
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x
Tactic:
intro x
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ f' (-x) = f' x