internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
hSurj : Function.Surjective ℤ₄.cast
h2 : Function.Bijective ℤ₄.cast
⊢ f ℤ₄.ℤ₄0.cast = ↑(ℤ₄Map ℤ₄.ℤ₄0)
Tactic:
change f 0 = ((-1 : ℤ) : S)
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
hSurj : Function.Surjective ℤ₄.cast
h2 : Function.Bijective ℤ₄.cast
⊢ f 0 = ↑(-1)
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
hSurj : Function.Surjective ℤ₄.cast
h2 : 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.Case2.RGoodSubcase22.Eq1
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 1) + f (x - 1) + f x = -1
Tactic:
rw [hf.toGoodCase2.Eq6, h, zero_sub, mul_neg_one, neg_add_rev, neg_add_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Rchar
Proof state before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 3 = 0
Tactic:
rw [← two_add_one_eq_three, ← eq_neg_iff_add_eq_zero]
Proof state after:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 2 = -1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Rchar
Proof state before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 2 = -1
Tactic:
refine hf.period_imp_eq _ _ λ x ↦ ?_
Proof state after:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 2) = f (x + -1)
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Rchar
Proof state before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 2) = f (x + -1)
Tactic:
have h0 := Eq1 hf h (x + 1)
Proof state after:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) + f (x + 1) = -1
⊢ f (x + 2) = f (x + -1)
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Rchar
Proof state before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) + f (x + 1) = -1
⊢ f (x + 2) = f (x + -1)
Tactic:
rwa [add_sub_cancel_right, add_assoc x, one_add_one_eq_two, ← Eq1 hf h x,
  ← add_rotate, add_left_inj, add_right_inj, sub_eq_add_neg] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Rchar'
Proof state before:
R : Type u_1
S : Type ?u.112996
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 2 = -1
Tactic:
rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 1) * f (x - 1) = (f x + 1) * f x
Tactic:
have h0 : f 2 ≠ 1 := λ h0 ↦ hf.map_two_ne_neg_one <| by rw [h, zero_eq_neg, ← h, ← h0]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f 2 ≠ 1
⊢ f (x + 1) * f (x - 1) = (f x + 1) * f x
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f 2 ≠ 1
⊢ f (x + 1) * f (x - 1) = (f x + 1) * f x
Tactic:
rw [add_one_mul (f x), ← sq, ← hf.toGoodCase2.Eq7 h0, add_one_mul (f _),
  mul_add_one (f _), add_assoc, add_assoc, self_eq_add_right,
  add_right_comm, ← add_assoc, ← add_assoc, Eq1 hf h, neg_add_self]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Eq2
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f 2 = 1
⊢ f 2 = -1
Tactic:
rw [h, zero_eq_neg, ← h, ← h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) = 0 ∧ f (x - 1) = 0
⊢ x = 0
Tactic:
rw [sub_eq_add_neg, ← Rchar' hf h, ← one_add_one_eq_two, ← add_assoc] at h1
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) = 0 ∧ f (x + 1 + 1) = 0
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) = 0 ∧ f (x + 1 + 1) = 0
⊢ x = 0
Tactic:
replace h1 := hf.toReducedGood.period_imp_zero
  (Eq5 hf.toNontrivialGood hf.map_even h1.1 h1.2)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : 2 * (x + 1) + 1 = 0
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : 2 * (x + 1) + 1 = 0
⊢ x = 0
Tactic:
rwa [Rchar' hf h, neg_one_mul, neg_add_rev, neg_add_cancel_comm, neg_eq_zero] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
have h1 : f (x + 1) + f (x - 1) = 0 := by
  rw [eq_sub_of_add_eq (Eq1 hf h x), h0, sub_self]
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) + f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) + f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
obtain h2 | h2 : f (x + 1) = 0 ∨ f (x - 1) = 0 := by
  rw [← mul_eq_zero, Eq2 hf h, h0, neg_add_self, zero_mul]
Proof state after:
case inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0

case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
⊢ f (x + 1) + f (x - 1) = 0
Tactic:
rw [eq_sub_of_add_eq (Eq1 hf h x), h0, sub_self]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) + f (x - 1) = 0
⊢ f (x + 1) = 0 ∨ f (x - 1) = 0
Tactic:
rw [← mul_eq_zero, Eq2 hf h, h0, neg_add_self, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
case inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
rw [h2, zero_add] at h1
Proof state after:
case inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
case inl
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
exact ⟨h2, h1⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
rw [h2, add_zero] at h1
Proof state after:
case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_imp
Proof state before:
case inr
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f x = -1
h1 : f (x + 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
exact ⟨h1, h2⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
⊢ f x = -1 ∨ f x = 0
Tactic:
have Rchar' := Rchar' hf h
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
⊢ f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
⊢ f x = -1 ∨ f x = 0
Tactic:
have h1 : f (x * x + 1) = (f x + 1) * f x := by
  rw [hf.is_good, ← two_mul, Rchar', neg_one_mul, hf.map_even, add_one_mul (f x)]
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
⊢ f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
⊢ f x = -1 ∨ f x = 0
Tactic:
have h2 : f (x * x - 1) = f x * f x - 1 := by
  rw [Case2.Eq1 hf.toNontrivialGood hf.map_even, sub_self, hf.map_zero, sub_eq_add_neg]
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
⊢ f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
⊢ f x = -1 ∨ f x = 0
Tactic:
have h3 : f (x * x) = (f x + 1 + 1) * f x := by
  have h2 := hf.is_good (x + 1) (x - 1)
  rw [Eq2 hf h, add_one_mul x, mul_sub_one, sub_add_sub_cancel, sub_add_cancel,
    add_add_sub_cancel, ← two_mul, Rchar', neg_one_mul, hf.map_even] at h2
  exact h2.trans (add_one_mul _ (f x)).symm
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
⊢ f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
⊢ f x = -1 ∨ f x = 0
Tactic:
have h4 := Eq1 hf h (x * x)
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f (x * x + 1) + f (x * x - 1) + f (x * x) = -1
⊢ f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f (x * x + 1) + f (x * x - 1) + f (x * x) = -1
⊢ f x = -1 ∨ f x = 0
Tactic:
rw [h1, h2, h3, ← add_sub_assoc, ← add_mul, ← add_sub_right_comm,
  sub_eq_neg_self, ← add_mul, mul_eq_zero, add_add_add_comm] at h4
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0
Tactic:
clear h1 h2 h3
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0
Tactic:
revert h4
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
⊢ f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0 → f x = -1 ∨ f x = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
⊢ f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0 → f x = -1 ∨ f x = 0
Tactic:
refine Or.imp_left λ h1 ↦ ?_
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f x + 1 + (f x + 1) + (f x + 1) = 0
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f x + 1 + (f x + 1) + (f x + 1) = 0
⊢ f x = -1
Tactic:
rw [← two_mul, ← add_one_mul 2 (f x + 1), mul_eq_zero, two_add_one_eq_three] at h1
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : 3 = 0 ∨ f x + 1 = 0
⊢ f x = -1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : 3 = 0 ∨ f x + 1 = 0
⊢ f x = -1
Tactic:
exact eq_neg_of_add_eq_zero_left (h1.resolve_left h0)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
⊢ f (x * x + 1) = (f x + 1) * f x
Tactic:
rw [hf.is_good, ← two_mul, Rchar', neg_one_mul, hf.map_even, add_one_mul (f x)]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
⊢ f (x * x - 1) = f x * f x - 1
Tactic:
rw [Case2.Eq1 hf.toNontrivialGood hf.map_even, sub_self, hf.map_zero, sub_eq_add_neg]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
⊢ f (x * x) = (f x + 1 + 1) * f x
Tactic:
have h2 := hf.is_good (x + 1) (x - 1)
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f ((x + 1) * (x - 1) + 1) = f (x + 1) * f (x - 1) + f (x + 1 + (x - 1))
⊢ f (x * x) = (f x + 1 + 1) * f x
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f ((x + 1) * (x - 1) + 1) = f (x + 1) * f (x - 1) + f (x + 1 + (x - 1))
⊢ f (x * x) = (f x + 1 + 1) * f x
Tactic:
rw [Eq2 hf h, add_one_mul x, mul_sub_one, sub_add_sub_cancel, sub_add_cancel,
  add_add_sub_cancel, ← two_mul, Rchar', neg_one_mul, hf.map_even] at h2
Proof state after:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f (x * x) = (f x + 1) * f x + f x
⊢ f (x * x) = (f x + 1 + 1) * f x
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.map_eq_neg_one_or_zero
Proof state before:
R : Type ?u.124008
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f (x * x) = (f x + 1) * f x + f x
⊢ f (x * x) = (f x + 1 + 1) * f x
Tactic:
exact h2.trans (add_one_mul _ (f x)).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.value_bash
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
have h1 (x) : x = 0 ∨ f x = 0 :=
  (map_eq_neg_one_or_zero hf h h0 x).imp_left (map_eq_neg_one_imp hf h)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.value_bash
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
refine (h1 x).imp_right λ h2 ↦ (h1 (x - 1)).imp eq_of_sub_eq_zero λ h3 ↦
  (h1 (x + 1)).elim eq_neg_of_add_eq_zero_left λ h4 ↦ ?_
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
⊢ x = -1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.value_bash
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
⊢ x = -1
Tactic:
have h5 := Eq1 hf h x
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : f (x + 1) + f (x - 1) + f x = -1
⊢ x = -1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.value_bash
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : f (x + 1) + f (x - 1) + f x = -1
⊢ x = -1
Tactic:
rw [h2, h3, h4, add_zero, add_zero, eq_comm, neg_eq_zero] at h5
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.value_bash
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1
Tactic:
rw [← mul_one 3, h5, mul_zero] at h0
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 0 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1