internlm/Lean-Github huggingface dataset:
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
⊢ g ((x * x - y * y) * (x * y - y * x)) = 0
Tactic:
have h0 := hg.Eq3 (x * x - y * y) (x * y - y * x)
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
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
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
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
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
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]
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
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
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
h1 : ((x + 1) * (x + 1) - y * y) * ((x + 1) * y - y * (x + 1)) = 0
⊢ (x * 2 + 1) * (x * y - y * x) = 0
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
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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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
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)
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
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
⊢ ∀ (x y : R), g (x * y) = g x * g y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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
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
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
h : ∀ (x y : R), x * y = 0 ∨ g (x * y) = g x * g y
x y : R
⊢ g (x * y) = g x * g y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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
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
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
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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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
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 ↦ ?_)
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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 ↦ ?_)
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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 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)
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 y : R
⊢ g (x * y + y) + g (x * y - y) = 2 * (g (x * y) + g y)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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 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
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 y : R
this : 2 = 0 ∨ g (x * y * y) - g (x * y) * g y = 0
⊢ g (x * y * y) = g (x * y) * g y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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
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)
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
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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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
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
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
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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
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
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)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq7
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq8
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 y : R
⊢ g (x + y) + g (x - y) = 2 • (g x + g y)
Tactic:
rw [two_nsmul, ← two_mul, ← sub_eq_zero, ← hg.Eq4, hg.Eq7, sub_self, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
⊢ ∃ R' x φ ι, ∀ (x_1 : R), g x_1 = ι (RestrictedSq (φ x_1))
Tactic:
refine ⟨R, CommRing.mk hg.Rcomm, RingHom.id R, ?_⟩
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), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let hR := CommRing.mk hg.Rcomm
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
hR : CommRing R := CommRing.mk ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
hR : CommRing R := CommRing.mk ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
have hS (x y : S) (h : 2 • x = 2 • y) : x = y := by
  rwa [two_nsmul, ← two_mul, two_nsmul, ← two_mul, ← sub_eq_zero, ← mul_sub,
    mul_eq_zero, or_iff_right hg.Schar_ne_two, sub_eq_zero] at h
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let φ := BilinMap hS hg.Eq8
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let ρ := φ 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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
have h : ∀ x, φ x x = 2 • g x := BilinMap_eq_two_nsmul _ _
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
have h0 (x y) : φ x y = ρ (x * y) :=
  hS _ _ <| by rw [two_nsmul_BilinMap_eq, two_nsmul_BilinMap_eq,
    ← hg.Eq2, add_comm, ← neg_sub (x * y), hg.toShiftGood23.map_even]
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let R₂ := AddSubgroup.closure (Set.range λ x : R ↦ x ^ 2)
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
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
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
obtain ⟨ι, h1⟩ : ∃ ι : SqSubring R →+ S, ∀ a : SqSubring R, ρ a = 2 • ι a :=
  suffices ∃ ι : SqSubring R → S, ∀ a : SqSubring R, ρ a = 2 • ι a by
    rcases this with ⟨ι, h1⟩
    have h3 (x y) : ι (x + y) = ι x + ι y := hS _ _ <| by
      rw [← h1, Subring.coe_add, ρ.map_add, h1, h1, nsmul_add]
    exact ⟨AddMonoidHom.mk' ι h3, h1⟩
  suffices ∀ r ∈ R₂, ∃ s, ρ r = 2 • s
    from Classical.axiomOfChoice λ a ↦ this a.1 a.2
  λ r h2 ↦ AddSubgroup.closure_induction h2
    (λ y ⟨x, h3⟩ ↦ ⟨g x, by rw [← h, h0 x, ← sq, ← h3]⟩)
    ⟨0, by rw [ρ.map_zero, nsmul_zero]⟩
    (λ x y ⟨s, hs⟩ ⟨t, ht⟩ ↦ ⟨s + t, by rw [ρ.map_add, hs, ht, nsmul_add]⟩)
    (λ x ⟨s, hs⟩ ↦ ⟨-s, by rw [ρ.map_neg, hs, nsmul_eq_mul, ← mul_neg, nsmul_eq_mul]⟩)
Proof state after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))