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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
⊢ g ((x * x - y * y) * (x * y - y * x)) = 0
Tactic:
have h0 := hg.Eq3 (x * x - y * y) (x * y - y * x)
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
h0 :
  (g (x * x - y * y + (x * y - y * x)) - g (x * x - y * y - (x * y - y * x))) ^ 2 =
    2 ^ 4 * g ((x * x - y * y) * (x * y - y * x))
⊢ g ((x * x - y * y) * (x * y - y * x)) = 0

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
h0 :
  (g (x * x - y * y + (x * y - y * x)) - g (x * x - y * y - (x * y - y * x))) ^ 2 =
    2 ^ 4 * g ((x * x - y * y) * (x * y - y * x))
⊢ g ((x * x - y * y) * (x * y - y * x)) = 0
Tactic:
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
State after:
no goals

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 + 1) * y - y * (x + 1) = x * y - y * x
Tactic:
rw [add_one_mul x, mul_add_one y, add_sub_add_right_eq_sub]
State after:
no goals

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 * 2 + 1) * (x * y - y * x) = 0
Tactic:
have h1 := h (x + 1) y
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
h1 : ((x + 1) * (x + 1) - y * y) * ((x + 1) * y - y * (x + 1)) = 0
⊢ (x * 2 + 1) * (x * y - y * x) = 0

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
h1 : ((x + 1) * (x + 1) - y * y) * ((x + 1) * y - y * (x + 1)) = 0
⊢ (x * 2 + 1) * (x * y - y * x) = 0
Tactic:
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
State after:
no goals