internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case2.map_even_of_map_one
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : good f
h : f (-1) = 0
x : R
⊢ f (-x) = f x
Tactic:
specialize hf (x + 1) (-1)
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
h : f (-1) = 0
x : R
hf : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f x
Theorem: IMOSL.IMO2012A5.Case2.map_even_of_map_one
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
h : f (-1) = 0
x : R
hf : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f x
Tactic:
rwa [h, mul_zero, zero_add, add_neg_cancel_right,
  mul_neg_one, neg_add, neg_add_cancel_right] at hf
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.Eq1
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x y : R
⊢ f (x * y - 1) = f x * f y + f (x - y)
Tactic:
rw [← h y, sub_eq_add_neg x, ← hf.is_good, mul_neg, neg_add_eq_sub, ← neg_sub, h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
⊢ f (x * 2 - 1) = f (x - 1) * f 2 + f (x + 1)
Tactic:
have h0 := hf.is_good (x - 1) (1 + 1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f ((x - 1) * (1 + 1) + 1) = f (x - 1) * f (1 + 1) + f (x - 1 + (1 + 1))
⊢ f (x * 2 - 1) = f (x - 1) * f 2 + f (x + 1)
Theorem: IMOSL.IMO2012A5.Case2.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f ((x - 1) * (1 + 1) + 1) = f (x - 1) * f (1 + 1) + f (x - 1 + (1 + 1))
⊢ f (x * 2 - 1) = f (x - 1) * f 2 + f (x + 1)
Tactic:
rwa [sub_add_add_cancel, one_add_one_eq_two, mul_two, add_assoc,
  sub_add_cancel, ← add_sub_right_comm, ← mul_two] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.Eq3
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
⊢ f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
Tactic:
have h0 := Eq2 hf (-x)
Proof state after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f (-x * 2 - 1) = f (-x - 1) * f 2 + f (-x + 1)
⊢ f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
Theorem: IMOSL.IMO2012A5.Case2.Eq3
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f (-x * 2 - 1) = f (-x - 1) * f 2 + f (-x + 1)
⊢ f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
Tactic:
rwa [neg_mul, ← neg_add', h, ← neg_add', h, neg_add_eq_sub, ← neg_sub, h] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
this : ∀ (y : R), f (x + y + 1) = f (x - y)
y : R
⊢ f (y + (2 * x + 1)) = f y
Tactic:
rw [two_mul, ← add_assoc, add_left_comm, this, sub_add_cancel_right, h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
⊢ f (x + y + 1) = f (x - y)
Tactic:
have h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1) := by
  rw [add_one_mul x, mul_add, add_one_mul x]
Proof state after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
⊢ f (x + y + 1) = f (x - y)
Theorem: IMOSL.IMO2012A5.Case2.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
⊢ f (x + y + 1) = f (x - y)
Tactic:
have h3 : x + (x + 1) * y = (x + 1) * (y + 1) - 1 := by
  rw [mul_add_one _ y, add_sub_assoc, add_sub_cancel_right, add_comm]
Proof state after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
h3 : x + (x + 1) * y = (x + 1) * (y + 1) - 1
⊢ f (x + y + 1) = f (x - y)
Theorem: IMOSL.IMO2012A5.Case2.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
h3 : x + (x + 1) * y = (x + 1) * (y + 1) - 1
⊢ f (x + y + 1) = f (x - y)
Tactic:
rwa [hf.is_good, h3, Eq1 hf h, hf.is_good, ← add_rotate, ← mul_add_one x,
  hf.is_good, h0, h1, zero_mul, zero_add, zero_mul, zero_add, zero_add,
  zero_mul, zero_add, add_sub_add_right_eq_sub, ← add_assoc, eq_comm] at h2
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
⊢ f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
Tactic:
rw [add_one_mul x, mul_add, add_one_mul x]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
⊢ x + (x + 1) * y = (x + 1) * (y + 1) - 1
Tactic:
rw [mul_add_one _ y, add_sub_assoc, add_sub_cancel_right, add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4
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
x : R
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
have h0 : x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1 := by
  rw [mul_add_one (x - 1), add_assoc, sub_add_cancel, sub_one_mul,
    ← add_sub_right_comm, add_comm, add_sub_add_right_eq_sub]
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
x : R
h0 : x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4
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
x : R
h0 : x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
apply congrArg f at h0
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
x : R
h0 : f (x * (x + 1) - 1) = f ((x - 1) * (x + 1 + 1) + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4
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
x : R
h0 : f (x * (x + 1) - 1) = f ((x - 1) * (x + 1 + 1) + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
rw [Eq1 hf h, hf.is_good, sub_add_cancel_left, h, hf.map_one, sub_add_add_cancel,
  add_zero, add_assoc, one_add_one_eq_two, ← add_assoc, ← mul_two] at h0
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
x : R
h0 : f x * f (x + 1) = f (x - 1) * f (x + 2) + f (x * 2 + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4
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
x : R
h0 : f x * f (x + 1) = f (x - 1) * f (x + 2) + f (x * 2 + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
rw [Eq2 hf, mul_add, h0, ← add_assoc, add_one_mul (f _),
  add_left_inj, mul_left_comm, ← mul_add, ← hf.is_good]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4
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
x : R
⊢ x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1
Tactic:
rw [mul_add_one (x - 1), add_assoc, sub_add_cancel, sub_one_mul,
  ← add_sub_right_comm, add_comm, add_sub_add_right_eq_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4_alt
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
x : R
⊢ f x * f (x * 2 + 1) = (f (x + 1) + 1) * f (x * 2 - 1)
Tactic:
have h0 := Eq4 hf h (-x)
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
x : R
h0 : f (-x) * f (-x * 2 - 1) = (f (-x - 1) + 1) * f (-x * 2 + 1)
⊢ f x * f (x * 2 + 1) = (f (x + 1) + 1) * f (x * 2 - 1)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4_alt
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
x : R
h0 : f (-x) * f (-x * 2 - 1) = (f (-x - 1) + 1) * f (-x * 2 + 1)
⊢ f x * f (x * 2 + 1) = (f (x + 1) + 1) * f (x * 2 - 1)
Tactic:
rwa [h, neg_mul, ← neg_add', h, ← neg_add', h, neg_add_eq_sub, ← neg_sub, h] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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
x : R
⊢ f (x * 2 + 1) = f (x + 2) - f x
Tactic:
rw [hf.is_good, h0, mul_neg_one, neg_add_eq_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
x : R
⊢ f (x * 2 + 1) = -f (x * 2 - 1)
Tactic:
rw [Eq2 hf, Eq3 hf h, h0, mul_neg_one, mul_neg_one, neg_add_rev, neg_neg]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Tactic:
have h3 := Eq4_alt hf h x
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x * f (x * 2 + 1) = (f (x + 1) + 1) * f (x * 2 - 1)
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x * f (x * 2 + 1) = (f (x + 1) + 1) * f (x * 2 - 1)
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Tactic:
rw [h2, mul_neg, neg_eq_iff_add_eq_zero, ← add_mul, mul_eq_zero, ← add_assoc] at h3
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x + f (x + 1) + 1 = 0 ∨ f (x * 2 - 1) = 0
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x + f (x + 1) + 1 = 0 ∨ f (x * 2 - 1) = 0
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Tactic:
exact h3.imp_left eq_neg_of_add_eq_zero_left
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
h3 : ∀ (x : R), f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
x : R
h4 : f ((x + 1) * 2 - 1) = 0
⊢ f (x + 2) = f x
Tactic:
rwa [mul_two, add_sub_assoc, add_sub_cancel_right,
add_right_comm, ← mul_two, h1, sub_eq_zero] at h4
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
h3 : ∀ (x : R), f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
x : R
h4 : f (x + 1) + f (x + 1 + 1) = -1
h5 : f (x * 2 - 1) = 0
⊢ f (x + 2) = f x
Tactic:
rwa [← neg_eq_zero, ← h2, h1, sub_eq_zero] at h5
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two
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 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
h3 : ∀ (x : R), f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
x : R
h4 : f (x + 1) + f (x + 1 + 1) = -1
h5 : f x + f (x + 1) = -1
⊢ f (x + 2) = f x
Tactic:
rwa [← h5, add_comm, add_left_inj, add_assoc, one_add_one_eq_two] at h4
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6_ring_id
Proof state before:
R : Type ?u.45782
S✝ : Type ?u.45785
inst✝³ : Ring R
inst✝² : CommRing S✝
inst✝¹ : NoZeroDivisors S✝
f : R → S✝
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
S : Type u_1
inst✝ : CommRing S
a b c d : S
⊢ a * (c * d + b) - a * (b * d + c) - ((c + 1) * (b * d + c) - (b + 1) * (c * d + b)) =
    (b + c - (a + 1) * (d - 1)) * (b - c)
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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 : ∀ (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
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 : ∀ (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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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 : ∀ (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 ↦ ?_
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 : ∀ (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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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 : ∀ (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)
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
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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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
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
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
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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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
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
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
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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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
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
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
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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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
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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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
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
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
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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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
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
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
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)
Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6
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
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
Proof state after:
no goals
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
⊢ 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)
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
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)