Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq6 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

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
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

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
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

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
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

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
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

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
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

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]
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

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 ↦ ?_
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

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)
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

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
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

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
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

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
State after:
no goals

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]
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)

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))
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)

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
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)

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)
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)

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
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)

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]
State after:
no goals

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]
State after:
no goals