internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
h :
  g (x * 2 + 1) - 1 + (g (x * 2 - 1) - 1) =
    (g (x + 1) - 1) * (g 2 - 1) + (g (x - 1) - 1) + ((g (x - 1) - 1) * (g 2 - 1) + (g (x + 1) - 1))
⊢ g (x * 2) = g x * 4
Tactic:
rw [← add_sub_add_comm, Eq1 hg, add_add_add_comm, ← add_mul,
  add_comm (g (x - 1) - 1), mul_sub_one, sub_add_cancel, ← add_sub_add_comm,
  Eq1 hg, one_add_one_eq_two, mul_add_one (α := S), add_sub_cancel_right,
  mul_add_one (α := S), add_sub_cancel_right, hg.map_two, mul_assoc,
  ← sub_eq_zero, ← mul_sub, mul_eq_zero] at h
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
h : 2 = 0 ∨ g (x * 2) - g x * 4 = 0
⊢ g (x * 2) = g x * 4
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq5
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
h : 2 = 0 ∨ g (x * 2) - g x * 4 = 0
⊢ g (x * 2) = g x * 4
Tactic:
exact eq_of_sub_eq_zero (h.resolve_left hg.Schar_ne_two)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.shift_mk_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ RShiftGood23 (f + 1) ↔ RGoodCase2 f ∧ f 2 = 3
Tactic:
rw [mk_iff, add_sub_cancel_right, ← three_add_one_eq_four]
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ RGoodCase2 f ∧ (f + 1) 2 = 3 + 1 ↔ RGoodCase2 f ∧ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.shift_mk_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ RGoodCase2 f ∧ (f + 1) 2 = 3 + 1 ↔ RGoodCase2 f ∧ f 2 = 3
Tactic:
exact and_congr_right' (add_left_inj _)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.period_imp_zero₀
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : RShiftGood23 g
c : R
h : ∀ (x : R), g (x + c) = g x
x : R
⊢ g (x + c) = g (x + 0)
Tactic:
rw [h, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
⊢ x = 0
Tactic:
have h0 := hg.Eq3 x 1
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : (g (x + 1) - g (x - 1)) ^ 2 = 2 ^ 4 * g (x * 1)
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : (g (x + 1) - g (x - 1)) ^ 2 = 2 ^ 4 * g (x * 1)
⊢ x = 0
Tactic:
rw [mul_one, h, mul_zero, sq_eq_zero_iff, sub_eq_zero] at h0
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = g (x - 1)
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = g (x - 1)
⊢ x = 0
Tactic:
have h1 := hg.Eq1 x
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = g (x - 1)
h1 : g (x + 1) + g (x - 1) = 2 * (g x + 1)
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = g (x - 1)
h1 : g (x + 1) + g (x - 1) = 2 * (g x + 1)
⊢ x = 0
Tactic:
rw [h, zero_add, h0, ← two_mul, ← sub_eq_zero, ← mul_sub,
  mul_eq_zero, or_iff_right hg.Schar_ne_two, sub_eq_zero] at h1
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = g (x - 1)
h1 : g (x - 1) = 1
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = g (x - 1)
h1 : g (x - 1) = 1
⊢ x = 0
Tactic:
rw [h1] at h0
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
⊢ x = 0
Tactic:
have h2 (y) : g (y - x) + 2 * g y = (2 + 1) * g (y + x) := by
  have h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y) := by
    rw [mul_sub_one, add_sub_left_comm, sub_add_cancel_left, ← sub_eq_add_neg,
      hg.toShiftGood23.alt_good, h0, sub_self, zero_mul, zero_add]
  have h3 := hg.toShiftGood23.is_good (x + 1) (x * (y - 1))
  rw [h0, sub_self, zero_mul, zero_add, ← add_rotate, ← mul_add_one x, sub_add_cancel,
    ← mul_assoc, add_one_mul x, ← mul_add_one x, mul_assoc, hg.toShiftGood23.is_good,
    h2, hg.toShiftGood23.is_good, h, zero_sub, neg_one_mul, neg_one_mul, neg_sub,
    neg_sub, sub_add, sub_add, sub_right_inj, sub_eq_iff_eq_add] at h3
  replace h2 := hg.Eq4 (x + 1) (y - 1)
  rw [h0, one_mul, mul_sub, mul_one_add (α := S), ← sub_sub, sub_left_inj,
    eq_sub_iff_add_eq, h3, mul_add, add_assoc, ← mul_add_one (α := S),
    add_add_sub_cancel, ← hg.Eq1, ← sub_add, ← add_assoc, ← add_rotate,
    add_left_inj, sub_sub, add_sub_add_right_eq_sub, ← neg_sub, mul_sub,
    hg.toShiftGood23.map_even, ← add_sub_assoc, sub_eq_iff_eq_add'] at h2
  rw [h2, add_one_mul (α := S), add_comm x]
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
h2 : ∀ (y : R), g (y - x) + 2 * g y = (2 + 1) * g (y + x)
⊢ x = 0
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
h2 : ∀ (y : R), g (y - x) + 2 * g y = (2 + 1) * g (y + x)
⊢ x = 0
Tactic:
refine hg.period_imp_zero₀ λ y ↦ ?_
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
h2 : ∀ (y : R), g (y - x) + 2 * g y = (2 + 1) * g (y + x)
y : R
⊢ g (y + x) = g y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
h2 : ∀ (y : R), g (y - x) + 2 * g y = (2 + 1) * g (y + x)
y : R
⊢ g (y + x) = g y
Tactic:
have h3 := h2 (-y)
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
h2 : ∀ (y : R), g (y - x) + 2 * g y = (2 + 1) * g (y + x)
y : R
h3 : g (-y - x) + 2 * g (-y) = (2 + 1) * g (-y + x)
⊢ g (y + x) = g y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
h2 : ∀ (y : R), g (y - x) + 2 * g y = (2 + 1) * g (y + x)
y : R
h3 : g (-y - x) + 2 * g (-y) = (2 + 1) * g (-y + x)
⊢ g (y + x) = g y
Tactic:
rw [← neg_add', hg.toShiftGood23.map_even, hg.toShiftGood23.map_even,
  neg_add_eq_sub, ← neg_sub, hg.toShiftGood23.map_even] at h3
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
h2 : ∀ (y : R), g (y - x) + 2 * g y = (2 + 1) * g (y + x)
y : R
h3 : g (y + x) + 2 * g y = (2 + 1) * g (y - x)
⊢ g (y + x) = g y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h3 : g (y + x) + 2 * g y = (2 + 1) * g (y - x)
h2 : g (y + x) + 2 * g y - (g (y - x) + 2 * g y) = (2 + 1) * g (y - x) - (2 + 1) * g (y + x)
⊢ g (y + x) = g y
Tactic:
rw [add_sub_add_right_eq_sub, ← mul_sub, ← neg_sub, neg_eq_iff_add_eq_zero,
  ← one_add_mul (α := S), mul_eq_zero, add_left_comm, one_add_one_eq_two,
  ← two_mul, mul_self_eq_zero, or_iff_right hg.Schar_ne_two, sub_eq_zero] at h2
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h3 : g (y + x) + 2 * g y = (2 + 1) * g (y - x)
h2 : g (y - x) = g (y + x)
⊢ g (y + x) = g y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h3 : g (y + x) + 2 * g y = (2 + 1) * g (y - x)
h2 : g (y - x) = g (y + x)
⊢ g (y + x) = g y
Tactic:
rwa [h2, add_one_mul (α := S), add_comm, add_left_inj, ← sub_eq_zero, ← mul_sub,
  mul_eq_zero, or_iff_right hg.Schar_ne_two, sub_eq_zero, eq_comm] at h3
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Tactic:
have h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y) := by
  rw [mul_sub_one, add_sub_left_comm, sub_add_cancel_left, ← sub_eq_add_neg,
    hg.toShiftGood23.alt_good, h0, sub_self, zero_mul, zero_add]
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y)
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y)
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Tactic:
have h3 := hg.toShiftGood23.is_good (x + 1) (x * (y - 1))
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y)
h3 : g ((x + 1) * (x * (y - 1)) + 1) = (g (x + 1) - 1) * (g (x * (y - 1)) - 1) + g (x + 1 + x * (y - 1))
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y)
h3 : g ((x + 1) * (x * (y - 1)) + 1) = (g (x + 1) - 1) * (g (x * (y - 1)) - 1) + g (x + 1 + x * (y - 1))
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Tactic:
rw [h0, sub_self, zero_mul, zero_add, ← add_rotate, ← mul_add_one x, sub_add_cancel,
  ← mul_assoc, add_one_mul x, ← mul_add_one x, mul_assoc, hg.toShiftGood23.is_good,
  h2, hg.toShiftGood23.is_good, h, zero_sub, neg_one_mul, neg_one_mul, neg_sub,
  neg_sub, sub_add, sub_add, sub_right_inj, sub_eq_iff_eq_add] at h3
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y)
h3 : g ((x + 1) * (y - 1)) = g y - g (x + y) + g (x + 1 - y)
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h2 : g (x + (x + 1) * (y - 1)) = g (x + 1 - y)
h3 : g ((x + 1) * (y - 1)) = g y - g (x + y) + g (x + 1 - y)
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Tactic:
replace h2 := hg.Eq4 (x + 1) (y - 1)
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h3 : g ((x + 1) * (y - 1)) = g y - g (x + y) + g (x + 1 - y)
h2 :
  2 * (g ((x + 1) * (y - 1)) - g (x + 1) * g (y - 1)) =
    g (x + 1 + (y - 1)) + g (x + 1 - (y - 1)) - 2 * (g (x + 1) + g (y - 1))
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h3 : g ((x + 1) * (y - 1)) = g y - g (x + y) + g (x + 1 - y)
h2 :
  2 * (g ((x + 1) * (y - 1)) - g (x + 1) * g (y - 1)) =
    g (x + 1 + (y - 1)) + g (x + 1 - (y - 1)) - 2 * (g (x + 1) + g (y - 1))
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Tactic:
rw [h0, one_mul, mul_sub, mul_one_add (α := S), ← sub_sub, sub_left_inj,
  eq_sub_iff_add_eq, h3, mul_add, add_assoc, ← mul_add_one (α := S),
  add_add_sub_cancel, ← hg.Eq1, ← sub_add, ← add_assoc, ← add_rotate,
  add_left_inj, sub_sub, add_sub_add_right_eq_sub, ← neg_sub, mul_sub,
  hg.toShiftGood23.map_even, ← add_sub_assoc, sub_eq_iff_eq_add'] at h2
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h3 : g ((x + 1) * (y - 1)) = g y - g (x + y) + g (x + 1 - y)
h2 : g (y - x) + 2 * g y = 2 * g (x + y) + g (x + y)
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
h3 : g ((x + 1) * (y - 1)) = g y - g (x + y) + g (x + 1 - y)
h2 : g (y - x) + 2 * g y = 2 * g (x + y) + g (x + y)
⊢ g (y - x) + 2 * g y = (2 + 1) * g (y + x)
Tactic:
rw [h2, add_one_mul (α := S), add_comm x]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x : R
h : g x = 0
h0 : g (x + 1) = 1
h1 : g (x - 1) = 1
y : R
⊢ g (x + (x + 1) * (y - 1)) = g (x + 1 - y)
Tactic:
rw [mul_sub_one, add_sub_left_comm, sub_add_cancel_left, ← sub_eq_add_neg,
  hg.toShiftGood23.alt_good, h0, sub_self, zero_mul, zero_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
⊢ ∀ (x y : R), x * y = y * x
Tactic:
have X : (2 : S) ^ 4 ≠ 0 := pow_ne_zero 4 hg.Schar_ne_two
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
⊢ ∀ (x y : R), x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
⊢ ∀ (x y : R), x * y = y * x
Tactic:
have h (x y) : g (x * y) = g (y * x) := by
  have h := hg.Eq3 x y
  rw [add_comm, ← neg_sub y, hg.toShiftGood23.map_even, hg.Eq3,
    ← sub_eq_zero, ← mul_sub, mul_eq_zero, or_iff_right X] at h
  exact (eq_of_sub_eq_zero h).symm
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h : ∀ (x y : R), g (x * y) = g (y * x)
⊢ ∀ (x y : R), x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h : ∀ (x y : R), g (x * y) = g (y * x)
⊢ ∀ (x y : R), x * y = y * x
Tactic:
replace h (x y) : (x * x - y * y) * (x * y - y * x) = 0 := hg.Eq6 <| by
  have h0 := hg.Eq3 (x * x - y * y) (x * y - y * x)
  rwa [sub_add_sub_comm, ← mul_add, ← mul_add, add_comm y, ← sub_mul, h,
    sub_sub_sub_comm, ← mul_sub, ← mul_sub, ← neg_sub x, mul_neg, sub_neg_eq_add,
    add_mul, sub_self, sq, zero_mul, zero_eq_mul, or_iff_right X] at h0
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h : ∀ (x y : R), (x * x - y * y) * (x * y - y * x) = 0
⊢ ∀ (x y : R), x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h : ∀ (x y : R), (x * x - y * y) * (x * y - y * x) = 0
⊢ ∀ (x y : R), x * y = y * x
Tactic:
have h0 (x y : R) : (x + 1) * y - y * (x + 1) = x * y - y * x := by
  rw [add_one_mul x, mul_add_one y, add_sub_add_right_eq_sub]
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h : ∀ (x y : R), (x * x - y * y) * (x * y - y * x) = 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
⊢ ∀ (x y : R), x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h : ∀ (x y : R), (x * x - y * y) * (x * y - y * x) = 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
⊢ ∀ (x y : R), x * y = y * x
Tactic:
replace h (x y : R) : (x * 2 + 1) * (x * y - y * x) = 0 := by
  have h1 := h (x + 1) y
  rwa [h0, add_one_mul x, mul_add_one x, add_assoc, add_sub_right_comm,
    add_mul, h, zero_add, ← add_assoc, ← mul_two] at h1
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
⊢ ∀ (x y : R), x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
⊢ ∀ (x y : R), x * y = y * x
Tactic:
intro x y
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
x y : R
⊢ x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
x y : R
⊢ x * y = y * x
Tactic:
have h1 := h (x + 1) y
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
x y : R
h1 : ((x + 1) * 2 + 1) * ((x + 1) * y - y * (x + 1)) = 0
⊢ x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
x y : R
h1 : ((x + 1) * 2 + 1) * ((x + 1) * y - y * (x + 1)) = 0
⊢ x * y = y * x
Tactic:
rw [h0, add_one_mul x, add_right_comm, add_mul, h, zero_add] at h1
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
x y : R
h1 : 2 * (x * y - y * x) = 0
⊢ x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
h : ∀ (x y : R), (x * 2 + 1) * (x * y - y * x) = 0
x y : R
h1 : 2 * (x * y - y * x) = 0
⊢ x * y = y * x
Tactic:
specialize h x y
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
x y : R
h1 : 2 * (x * y - y * x) = 0
h : (x * 2 + 1) * (x * y - y * x) = 0
⊢ x * y = y * x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
h0 : ∀ (x y : R), (x + 1) * y - y * (x + 1) = x * y - y * x
x y : R
h1 : 2 * (x * y - y * x) = 0
h : (x * 2 + 1) * (x * y - y * x) = 0
⊢ x * y = y * x
Tactic:
rwa [add_one_mul (α := R), mul_assoc, h1, mul_zero, zero_add, sub_eq_zero] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
x y : R
⊢ g (x * y) = g (y * x)
Tactic:
have h := hg.Eq3 x y
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
x y : R
h : (g (x + y) - g (x - y)) ^ 2 = 2 ^ 4 * g (x * y)
⊢ g (x * y) = g (y * x)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
x y : R
h : (g (x + y) - g (x - y)) ^ 2 = 2 ^ 4 * g (x * y)
⊢ g (x * y) = g (y * x)
Tactic:
rw [add_comm, ← neg_sub y, hg.toShiftGood23.map_even, hg.Eq3,
  ← sub_eq_zero, ← mul_sub, mul_eq_zero, or_iff_right X] at h
Proof state after:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
x y : R
h : g (y * x) - g (x * y) = 0
⊢ g (x * y) = g (y * x)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Rcomm
Proof state before:
S : Type ?u.222622
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
X : 2 ^ 4 ≠ 0
x y : R
h : g (y * x) - g (x * y) = 0
⊢ g (x * y) = g (y * x)
Tactic:
exact (eq_of_sub_eq_zero h).symm
Proof state after:
no goals