Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7 (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
h : ∀ (x y : R), g (x * y * y) = g (x * y) * g y
⊢ ∀ (x y : R), g (x * y) = g x * g y
Tactic:
replace h (x y) : x * y = 0 ∨ g (x * y) = g x * g y := by
  have h0 := h 1 (x * y)
  rw [one_mul, ← mul_assoc, hg.Rcomm _ x, ← mul_assoc, h, mul_assoc, hg.Rcomm x,
    hg.Rcomm x, h, mul_assoc, hg.Rcomm y, ← sub_eq_zero, ← mul_sub, mul_eq_zero] at h0
  exact h0.imp hg.Eq6 (λ h0 ↦ (eq_of_sub_eq_zero h0).symm)
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
⊢ ∀ (x y : R), g (x * y) = g 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
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
⊢ ∀ (x y : R), g (x * y) = g x * g y
Tactic:
intro x 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
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
⊢ g (x * y) = g 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
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
⊢ g (x * y) = g x * g y
Tactic:
refine (h x y).elim (λ h0 ↦ ?_) id
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
⊢ g (x * y) = g 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
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
⊢ g (x * y) = g x * g y
Tactic:
refine (h (x + 1) y).elim (λ h1 ↦ ?_) (λ h1 ↦ ?_)
State after:
case refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : (x + 1) * y = 0
⊢ g (x * y) = g x * g y

case refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
⊢ g (x * y) = g x * g y

State before:
case refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
⊢ g (x * y) = g x * g y
Tactic:
refine (h (x - 1) y).elim (λ h2 ↦ ?_) (λ h2 ↦ ?_)
State after:
case refine_2.refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
h2 : (x - 1) * y = 0
⊢ g (x * y) = g x * g y

case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
h2 : g ((x - 1) * y) = g (x - 1) * g y
⊢ g (x * y) = g x * g y

State before:
case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
h2 : g ((x - 1) * y) = g (x - 1) * g y
⊢ g (x * y) = g x * g y
Tactic:
rw [add_one_mul x, h0, zero_add] at h1
State after:
case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g y = g (x + 1) * g y
h2 : g ((x - 1) * y) = g (x - 1) * g y
⊢ g (x * y) = g x * g y

State before:
case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g y = g (x + 1) * g y
h2 : g ((x - 1) * y) = g (x - 1) * g y
⊢ g (x * y) = g x * g y
Tactic:
rw [sub_one_mul, h0, zero_sub, hg.toShiftGood23.map_even] at h2
State after:
case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g y = g (x + 1) * g y
h2 : g y = g (x - 1) * g y
⊢ g (x * y) = g x * g y

State before:
case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g y = g (x + 1) * g y
h2 : g y = g (x - 1) * g y
h3 : g y + g y = g (x + 1) * g y + g (x - 1) * g y
⊢ g (x * y) = g x * g y
Tactic:
rw [← two_mul, ← add_mul, hg.Eq1, mul_add_one (α := S), add_mul, self_eq_add_left,
  mul_assoc, mul_eq_zero, or_iff_right hg.Schar_ne_two] at h3
State after:
case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g y = g (x + 1) * g y
h2 : g y = g (x - 1) * g y
h3 : g x * g y = 0
⊢ g (x * y) = g x * g y

State before:
case refine_2.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g y = g (x + 1) * g y
h2 : g y = g (x - 1) * g y
h3 : g x * g y = 0
⊢ g (x * y) = g x * g y
Tactic:
rw [h0, hg.toShiftGood23.map_zero, 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 y : R
⊢ g (x * y * y) = g (x * y) * g y
Tactic:
suffices g (x * y + y) + g (x * y - y) = 2 * (g (x * y) + g y) by
  rw [← sub_eq_zero, ← hg.Eq4, mul_eq_zero] at this
  exact eq_of_sub_eq_zero (this.resolve_left hg.Schar_ne_two)
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 y : R
⊢ g (x * y + y) + g (x * y - y) = 2 * (g (x * y) + 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 y : R
h :
  2 * (g ((x + 1) * y) - g (x + 1) * g y) + 2 * (g ((x - 1) * y) - g (x - 1) * g y) =
    g (x + 1 + y) + g (x + 1 - y) - 2 * (g (x + 1) + g y) + (g (x - 1 + y) + g (x - 1 - y) - 2 * (g (x - 1) + g y))
⊢ g (x * y + y) + g (x * y - y) = 2 * (g (x * y) + g y)
Tactic:
rwa [← mul_add, sub_add_sub_comm, ← add_mul, sub_add_sub_comm, add_add_add_comm,
  hg.Eq1, add_right_comm x, ← add_sub_right_comm x y, hg.Eq1, add_sub_right_comm x,
  sub_right_comm, hg.Eq1, ← mul_add, ← mul_add, ← mul_sub, add_add_add_comm,
  add_add_add_comm (g _) (g y), hg.Eq1, ← sub_eq_zero, ← mul_sub, mul_eq_zero,
  or_iff_right hg.Schar_ne_two, sub_eq_zero, sub_eq_iff_eq_add, one_add_one_eq_two,
  mul_add_one (α := S), ← two_mul, add_right_comm (2 * g x), add_sub_add_right_eq_sub,
  ← mul_add, ← hg.Eq4, ← mul_add_one (α := S), mul_assoc, ← mul_add, add_one_mul (g x),
  add_comm _ (g y), sub_add_add_cancel, add_one_mul x, sub_one_mul] at h
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 y : R
this : g (x * y + y) + g (x * y - y) = 2 * (g (x * y) + g y)
⊢ g (x * y * y) = g (x * y) * g y
Tactic:
rw [← sub_eq_zero, ← hg.Eq4, mul_eq_zero] at this
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 y : R
this : 2 = 0 ∨ g (x * y * y) - g (x * y) * g y = 0
⊢ g (x * y * y) = g (x * y) * 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 y : R
this : 2 = 0 ∨ g (x * y * y) - g (x * y) * g y = 0
⊢ g (x * y * y) = g (x * y) * g y
Tactic:
exact eq_of_sub_eq_zero (this.resolve_left hg.Schar_ne_two)
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
h : ∀ (x y : R), g (x * y * y) = g (x * y) * g y
x y : R
⊢ x * y = 0 ∨ g (x * y) = g x * g y
Tactic:
have h0 := h 1 (x * 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
h : ∀ (x y : R), g (x * y * y) = g (x * y) * g y
x y : R
h0 : g (1 * (x * y) * (x * y)) = g (1 * (x * y)) * g (x * y)
⊢ x * y = 0 ∨ g (x * y) = g 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
h : ∀ (x y : R), g (x * y * y) = g (x * y) * g y
x y : R
h0 : g (1 * (x * y) * (x * y)) = g (1 * (x * y)) * g (x * y)
⊢ x * y = 0 ∨ g (x * y) = g x * g y
Tactic:
rw [one_mul, ← mul_assoc, hg.Rcomm _ x, ← mul_assoc, h, mul_assoc, hg.Rcomm x,
  hg.Rcomm x, h, mul_assoc, hg.Rcomm y, ← sub_eq_zero, ← mul_sub, mul_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
h : ∀ (x y : R), g (x * y * y) = g (x * y) * g y
x y : R
h0 : g (x * y) = 0 ∨ g x * g y - g (x * y) = 0
⊢ x * y = 0 ∨ g (x * y) = g 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
h : ∀ (x y : R), g (x * y * y) = g (x * y) * g y
x y : R
h0 : g (x * y) = 0 ∨ g x * g y - g (x * y) = 0
⊢ x * y = 0 ∨ g (x * y) = g x * g y
Tactic:
exact h0.imp hg.Eq6 (λ h0 ↦ (eq_of_sub_eq_zero h0).symm)
State after:
no goals

State before:
case refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : (x + 1) * y = 0
⊢ g (x * y) = g x * g y
Tactic:
rw [add_one_mul x, h0, zero_add] at h1
State after:
case refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : y = 0
⊢ g (x * y) = g x * g y

State before:
case refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : y = 0
⊢ g (x * y) = g x * g y
Tactic:
rw [h1, mul_zero, hg.toShiftGood23.map_zero, mul_zero]
State after:
no goals

State before:
case refine_2.refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
h2 : (x - 1) * y = 0
⊢ g (x * y) = g x * g y
Tactic:
rw [sub_one_mul x, h0, zero_sub, neg_eq_zero] at h2
State after:
case refine_2.refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
h2 : y = 0
⊢ g (x * y) = g x * g y

State before:
case refine_2.refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
h0 : x * y = 0
h1 : g ((x + 1) * y) = g (x + 1) * g y
h2 : y = 0
⊢ g (x * y) = g x * g y
Tactic:
rw [h2, mul_zero, hg.toShiftGood23.map_zero, mul_zero]
State after:
no goals