internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case1.map_neg_one_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
⊢ f (-1) = -2 ∨ f (-1) = 1
Tactic:
rw [← sub_eq_zero (b := 1), eq_neg_iff_add_eq_zero, ← mul_eq_zero,
  mul_sub_one, add_mul, two_mul, add_sub_assoc, add_sub_add_left_eq_sub]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Theorem: IMOSL.IMO2012A5.Case1.map_neg_one_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
have h0 := Eq5 hf h (-1 + -1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1 + -1 + 1) = 0 ∨ f (-1 + -1) + f (-(-1 + -1)) = f (-1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Theorem: IMOSL.IMO2012A5.Case1.map_neg_one_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1 + -1 + 1) = 0 ∨ f (-1 + -1) + f (-(-1 + -1)) = f (-1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
rw [neg_add_cancel_right, or_iff_right h, ← eq_sub_iff_add_eq] at h0
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Theorem: IMOSL.IMO2012A5.Case1.map_neg_one_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
have h1 := hf.is_good (-1) (-1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
h1 : f (-1 * -1 + 1) = f (-1) * f (-1) + f (-1 + -1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Theorem: IMOSL.IMO2012A5.Case1.map_neg_one_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
h1 : f (-1 * -1 + 1) = f (-1) * f (-1) + f (-1 + -1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
rwa [h0, neg_mul_neg, one_mul, ← neg_add, neg_neg, one_add_one_eq_two, map_two hf h,
  eq_comm, ← sub_eq_zero, add_sub_assoc, sub_sub, one_add_one_eq_two] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Subcase11_solution
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
⊢ f (x + 1) = f x + 1
Tactic:
rcases Eq5 hf h x with h2 | h2
Proof state after:
case inl
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f (x + 1) = 0
⊢ f (x + 1) = f x + 1

case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f x + f (-x) = f (-1)
⊢ f (x + 1) = f x + 1
Theorem: IMOSL.IMO2012A5.Case1.Subcase11_solution
Proof state before:
case inl
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f (x + 1) = 0
⊢ f (x + 1) = f x + 1
Tactic:
rw [Eq6 hf h h2, h2, neg_add_self]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.Subcase11_solution
Proof state before:
case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f x + f (-x) = f (-1)
⊢ f (x + 1) = f x + 1
Tactic:
rw [Eq1 hf, h0, add_left_comm, ← mul_two, mul_neg, ← neg_mul, ← add_mul,
  eq_neg_iff_add_eq_zero, ← add_one_mul _ (2 : S), mul_eq_zero, add_assoc] at h2
Proof state after:
case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : -f (x + 1) + (f x + 1) = 0 ∨ 2 = 0
⊢ f (x + 1) = f x + 1
Theorem: IMOSL.IMO2012A5.Case1.Subcase11_solution
Proof state before:
case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : -f (x + 1) + (f x + 1) = 0 ∨ 2 = 0
⊢ f (x + 1) = f x + 1
Tactic:
exact neg_add_eq_zero.mp (h2.resolve_right (neg_ne_zero.mp (h0.symm.trans_ne h)))
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.map_neg_one_ne_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : f (-1) = 0
⊢ 3 = 0
Tactic:
rw [← mul_one (3 : S), ← hf.map_neg_one, h, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
⊢ x = 0
Tactic:
have h0 (x) : f (-x) = f (x + 1) + f x := by
  rw [Eq1 hf.toNontrivialGood, hf.map_neg_one, mul_one]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
⊢ x = 0
Tactic:
have h1 : f (-x) = f x := by rw [h0, h, zero_add]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
⊢ x = 0
Tactic:
refine hf.period_imp_zero λ y ↦ ?_
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
⊢ f (y + x) = f y
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
⊢ f (y + x) = f y
Tactic:
have h2 := Eq3 hf.toNontrivialGood x (y - 1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
h2 : f (-x) * f (-(y - 1)) + f (-(x + (y - 1))) = f x * f (y - 1) + f (x + (y - 1))
⊢ f (y + x) = f y
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
h2 : f (-x) * f (-(y - 1)) + f (-(x + (y - 1))) = f x * f (y - 1) + f (x + (y - 1))
⊢ f (y + x) = f y
Tactic:
rwa [h1, Case1.Eq6 hf.toNontrivialGood (map_neg_one_ne_zero hf) h, neg_one_mul,
  neg_one_mul, h0, h0 (x + _), add_assoc, sub_add_cancel, ← add_assoc, add_left_inj,
  neg_add_rev, add_assoc, add_right_eq_self, neg_add_eq_zero, eq_comm, add_comm] at h2
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : f (x✝ + 1) = 0
x : R
⊢ f (-x) = f (x + 1) + f x
Tactic:
rw [Eq1 hf.toNontrivialGood, hf.map_neg_one, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
⊢ f (-x) = f x
Tactic:
rw [h0, h, zero_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.triple_sum_eq_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
⊢ f x + f (x + 1) + f (x + 2) = 0
Tactic:
have h := Eq1 hf.toNontrivialGood x
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x + f (x + 1) + f (x + 2) = 0
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.triple_sum_eq_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x + f (x + 1) + f (x + 2) = 0
Tactic:
rwa [Case1.Eq2 hf.toNontrivialGood (map_neg_one_ne_zero hf), hf.map_neg_one,
  mul_one, neg_eq_iff_add_eq_zero, add_comm, add_comm (f _)] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.Rchar
Proof state before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
⊢ 3 = 0
Tactic:
refine hf.period_imp_zero λ x ↦ ?_
Proof state after:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
⊢ f (x + 3) = f x
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.Rchar
Proof state before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
⊢ f (x + 3) = f x
Tactic:
have h := triple_sum_eq_zero hf
Proof state after:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
⊢ f (x + 3) = f x
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.Rchar
Proof state before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
⊢ f (x + 3) = f x
Tactic:
have h0 := h (x + 1)
Proof state after:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
h0 : f (x + 1) + f (x + 1 + 1) + f (x + 1 + 2) = 0
⊢ f (x + 3) = f x
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.Rchar
Proof state before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
h0 : f (x + 1) + f (x + 1 + 1) + f (x + 1 + 2) = 0
⊢ f (x + 3) = f x
Tactic:
rwa [add_assoc x, one_add_one_eq_two, ← add_rotate, ← h x, add_left_inj,
  add_left_inj, add_assoc, add_comm 1, two_add_one_eq_three] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
have h := eq_zero_or_map_neg_add_self hf
Proof state after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
⊢ x = 0 ∨ x = 1 ∨ x = -1
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
refine (h x).imp_right λ h0 ↦ (h (x - 1)).imp eq_of_sub_eq_zero
  λ h1 ↦ eq_neg_of_add_eq_zero_left <| (h (x + 1)).resolve_right λ h2 ↦ ?_
Proof state after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
⊢ False
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
⊢ False
Tactic:
replace h (x) : f x + f (x + 1) + f (x - 1) = 0 := by
  have h3 : (2 : R) = -1 := by
    rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf]
  rw [sub_eq_add_neg, ← h3, triple_sum_eq_zero hf]
Proof state after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : ∀ (x : R), f x + f (x + 1) + f (x - 1) = 0
⊢ False
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : f x + f (x + 1) + f (x - 1) + (f (-x) + f (-x + 1) + f (-x - 1)) = 0 + 0
⊢ False
Tactic:
rw [add_zero, ← neg_add', add_right_comm (f _), add_add_add_comm,
  add_add_add_comm (f _), h0, h2, neg_add_eq_sub, ← neg_sub x, h1,
  one_add_one_eq_two, two_add_one_eq_three] at h
Proof state after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : 3 = 0
⊢ False
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : 3 = 0
⊢ False
Tactic:
exact hf.Schar h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
⊢ f x + f (x + 1) + f (x - 1) = 0
Tactic:
have h3 : (2 : R) = -1 := by
  rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf]
Proof state after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
h3 : 2 = -1
⊢ f x + f (x + 1) + f (x - 1) = 0
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
h3 : 2 = -1
⊢ f x + f (x + 1) + f (x - 1) = 0
Tactic:
rw [sub_eq_add_neg, ← h3, triple_sum_eq_zero hf]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.value_bash
Proof state before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
⊢ 2 = -1
Tactic:
rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : 1 = 0
⊢ f (-1) = 0
Tactic:
rw [h, neg_zero, ← h, hf.map_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : Function.Bijective 𝔽₃.cast
⊢ f 𝔽₃.𝔽₃0.cast = ↑(𝔽₃Map1 𝔽₃.𝔽₃0)
Tactic:
change f 0 = ((-1 : ℤ) : S)
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : Function.Bijective 𝔽₃.cast
⊢ f 0 = ↑(-1)
Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
h : Function.Bijective 𝔽₃.cast
⊢ f 0 = ↑(-1)
Tactic:
rw [hf.map_zero, Int.cast_neg, Int.cast_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case1.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) ≠ 0
hf' : NontrivialGood f := hf.toNontrivialGood
h0 : ¬f (-1) = -2
h1 : f (-1) = 1
⊢ 3 ≠ 0
Tactic:
rwa [← two_add_one_eq_three, Ne,
← neg_eq_iff_add_eq_zero, ← h1, eq_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.add_one_iterate
Proof state before:
n : ℕ
a : ℤ
⊢ (fun x => x + 1)^[n + 1] a = a + ↑(n + 1)
Tactic:
rw [iterate_succ_apply', add_one_iterate n a, add_assoc]
Proof state after:
n : ℕ
a : ℤ
⊢ a + (↑n + 1) = a + ↑(n + 1)
Theorem: IMOSL.IMO2020A6.add_one_iterate
Proof state before:
n : ℕ
a : ℤ
⊢ a + (↑n + 1) = a + ↑(n + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.good_add_one
Proof state before:
a b : ℤ
⊢ (fun x => x + 1)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => x + 1) a + b * (fun x => x + 1) b
Tactic:
have h (c : ℤ) : c + ((c.natAbs ^ 2 : ℕ) : ℤ) = c * (c + 1) := by
  rw [Int.natCast_pow, Int.natAbs_sq, sq, ← mul_one_add, add_comm]
Proof state after:
a b : ℤ
h : ∀ (c : ℤ), c + ↑(c.natAbs ^ 2) = c * (c + 1)
⊢ (fun x => x + 1)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => x + 1) a + b * (fun x => x + 1) b
Theorem: IMOSL.IMO2020A6.good_add_one
Proof state before:
a b : ℤ
h : ∀ (c : ℤ), c + ↑(c.natAbs ^ 2) = c * (c + 1)
⊢ (fun x => x + 1)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => x + 1) a + b * (fun x => x + 1) b
Tactic:
rw [add_one_iterate, Int.ofNat_add, add_add_add_comm, h, h]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.good_add_one
Proof state before:
a b c : ℤ
⊢ c + ↑(c.natAbs ^ 2) = c * (c + 1)
Tactic:
rw [Int.natCast_pow, Int.natAbs_sq, sq, ← mul_one_add, add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
a b : ℤ
⊢ (fun x => 0)^[a.natAbs ^ 2 + b.natAbs ^ 2] (a + b) = a * (fun x => 0) a + b * (fun x => 0) b
Tactic:
rw [const_iterate, ← Int.add_mul, Int.mul_zero]
Proof state after:
a b : ℤ
⊢ (bif (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 then a + b else 0) = 0
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
a b : ℤ
⊢ (bif (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 then a + b else 0) = 0
Tactic:
cases h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0
Proof state after:
case false
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = false
⊢ (bif false then a + b else 0) = 0

case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
⊢ (bif true then a + b else 0) = 0
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
case false
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = false
⊢ (bif false then a + b else 0) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
⊢ (bif true then a + b else 0) = 0
Tactic:
have h0 : ∀ c : ℤ, c.natAbs ^ 2 = 0 ↔ c = 0 :=
  λ c ↦ by rw [sq_eq_zero_iff, Int.natAbs_eq_zero]
Proof state after:
case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
case true
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0
Tactic:
rw [Nat.beq_eq, add_eq_zero, h0, h0] at h
Proof state after:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then a + b else 0) = 0
Tactic:
rw [h.1, h.2]
Proof state after:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then 0 + 0 else 0) = 0
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
case true
a b : ℤ
h : a = 0 ∧ b = 0
h0 : ∀ (c : ℤ), c.natAbs ^ 2 = 0 ↔ c = 0
⊢ (bif true then 0 + 0 else 0) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.good_zero
Proof state before:
a b : ℤ
h : (a.natAbs ^ 2 + b.natAbs ^ 2).beq 0 = true
c : ℤ
⊢ c.natAbs ^ 2 = 0 ↔ c = 0
Tactic:
rw [sq_eq_zero_iff, Int.natAbs_eq_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.map_iterate_sq
Proof state before:
f : ℤ → ℤ
h : good f
a : ℤ
⊢ f^[a.natAbs ^ 2] a = a * f a
Tactic:
have h := h a 0
Proof state after:
f : ℤ → ℤ
h✝ : good f
a : ℤ
h : f^[a.natAbs ^ 2 + Int.natAbs 0 ^ 2] (a + 0) = a * f a + 0 * f 0
⊢ f^[a.natAbs ^ 2] a = a * f a
Theorem: IMOSL.IMO2020A6.map_iterate_sq
Proof state before:
f : ℤ → ℤ
h✝ : good f
a : ℤ
h : f^[a.natAbs ^ 2 + Int.natAbs 0 ^ 2] (a + 0) = a * f a + 0 * f 0
⊢ f^[a.natAbs ^ 2] a = a * f a
Tactic:
rwa [zero_mul, add_zero, add_zero] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2020A6.map_iterate_sq_add_one
Proof state before:
f : ℤ → ℤ
h : good f
a : ℤ
⊢ f^[(a + 1).natAbs ^ 2 + 1] a = f^[(a + 1).natAbs ^ 2] (a + 1)
Tactic:
have h0 := h (a + 1) (-1)
Proof state after:
f : ℤ → ℤ
h : good f
a : ℤ
h0 : f^[(a + 1).natAbs ^ 2 + (-1).natAbs ^ 2] (a + 1 + -1) = (a + 1) * f (a + 1) + -1 * f (-1)
⊢ f^[(a + 1).natAbs ^ 2 + 1] a = f^[(a + 1).natAbs ^ 2] (a + 1)
Theorem: IMOSL.IMO2020A6.map_iterate_sq_add_one
Proof state before:
f : ℤ → ℤ
h : good f
a : ℤ
h0 : f^[(a + 1).natAbs ^ 2 + (-1).natAbs ^ 2] (a + 1 + -1) = (a + 1) * f (a + 1) + -1 * f (-1)
⊢ f^[(a + 1).natAbs ^ 2 + 1] a = f^[(a + 1).natAbs ^ 2] (a + 1)
Tactic:
rwa [add_neg_cancel_right, map_neg_one h,
  mul_zero, add_zero, ← map_iterate_sq h] at h0
Proof state after:
no goals