internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.value_bash
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 0 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1
Tactic:
exact absurd rfl h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.solution
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0 : 3 ≠ 0
h : 1 = 0
⊢ 3 = 0
Tactic:
have h0 := hf.map_one
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : f 1 = 0
⊢ 3 = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.solution
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : f 1 = 0
⊢ 3 = 0
Tactic:
rw [h, hf.map_zero, neg_eq_zero] at h0
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : 1 = 0
⊢ 3 = 0
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.solution
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h✝ : f 2 = 0
h0✝ : 3 ≠ 0
h : 1 = 0
h0 : 1 = 0
⊢ 3 = 0
Tactic:
rw [← mul_one 3, h0, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.solution
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
h1 : Function.Bijective 𝔽₃.cast
⊢ f 𝔽₃.𝔽₃0.cast = ↑(𝔽₃Map2 𝔽₃.𝔽₃0)
Tactic:
change f 0 = ((-1 : ℤ) : S)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
h1 : Function.Bijective 𝔽₃.cast
⊢ f 0 = ↑(-1)
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.solution
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
h0 : 3 ≠ 0
h1 : Function.Bijective 𝔽₃.cast
⊢ f 0 = ↑(-1)
Tactic:
rw [hf.map_zero, Int.cast_neg, Int.cast_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
c : R
⊢ ∃ R' x φ,
    ∃ (_ : Function.Injective ⇑φ) (_ : c ∈ Set.range ⇑φ),
      ∃ S' x_3,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ g', ∃ (_ : ∀ (a : R'), g (φ a) = ρ (g' a)), ShiftGood23 g'
Tactic:
rcases hg.shift_good.oneVarLift_exists c with
  ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f', h0, hf'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ g', ∃ (_ : ∀ (a : R'_1), g (φ_1 a) = ρ (g' a)), ShiftGood23 g'
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ g', ∃ (_ : ∀ (a : R'_1), g (φ_1 a) = ρ (g' a)), ShiftGood23 g'
Tactic:
refine ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f' + 1, ?_, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∀ (a : R'), g (φ a) = ρ ((f' + 1) a)

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ShiftGood23 (f' + 1)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∀ (a : R'), g (φ a) = ρ ((f' + 1) a)
Tactic:
intro x
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = ρ ((f' + 1) x)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = ρ ((f' + 1) x)
Tactic:
rw [Pi.add_apply, Pi.one_apply, ρ.map_add, ← h0, ρ.map_one]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = (g - 1) (φ x) + 1
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = (g - 1) (φ x) + 1
Tactic:
exact (sub_add_cancel _ _).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ShiftGood23 (f' + 1)
Tactic:
refine ⟨by rwa [add_sub_cancel_right], hρ ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ρ ((f' + 1) 2) = ρ 4
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ρ ((f' + 1) 2) = ρ 4
Tactic:
rw [Pi.add_apply, Pi.one_apply, ρ.map_add, ρ.map_one, ← h0, map_ofNat,
  map_ofNat, Pi.sub_apply, Pi.one_apply, hg.map_two, sub_add_cancel]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists
Proof state before:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ GoodCase2 (f' + 1 - 1)
Tactic:
rwa [add_sub_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.shift_mk_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ ShiftGood23 (f + 1) ↔ GoodCase2 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
⊢ GoodCase2 f ∧ (f + 1) 2 = 3 + 1 ↔ GoodCase2 f ∧ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.shift_mk_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ GoodCase2 f ∧ (f + 1) 2 = 3 + 1 ↔ GoodCase2 f ∧ f 2 = 3
Tactic:
exact and_congr_right' (add_left_inj _)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Schar_ne_two
Proof state before:
R : Type ?u.155749
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
h : 2 = 0
⊢ (g - 1) 2 = -1
Tactic:
rw [Pi.sub_apply, Pi.one_apply, sub_eq_neg_self, hg.map_two, ← three_add_one_eq_four,
  ← two_add_one_eq_three, h, zero_add, one_add_one_eq_two, h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.is_good
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
⊢ g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)
Tactic:
have h := hg.shift_good.is_good x y
Proof state after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : (g - 1) (x * y + 1) = (g - 1) x * (g - 1) y + (g - 1) (x + y)
⊢ g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.is_good
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : (g - 1) (x * y + 1) = (g - 1) x * (g - 1) y + (g - 1) (x + y)
⊢ g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)
Tactic:
simp only [Pi.sub_apply, Pi.one_apply] at h
Proof state after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : g (x * y + 1) - 1 = (g x - 1) * (g y - 1) + (g (x + y) - 1)
⊢ g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.is_good
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : g (x * y + 1) - 1 = (g x - 1) * (g y - 1) + (g (x + y) - 1)
⊢ g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)
Tactic:
rwa [← add_sub_assoc, sub_left_inj] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.alt_good
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
⊢ g (x * y - 1) = (g x - 1) * (g y - 1) + g (x - y)
Tactic:
have h := hg.is_good x (-y)
Proof state after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : g (x * -y + 1) = (g x - 1) * (g (-y) - 1) + g (x + -y)
⊢ g (x * y - 1) = (g x - 1) * (g y - 1) + g (x - y)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.alt_good
Proof state before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : g (x * -y + 1) = (g x - 1) * (g (-y) - 1) + g (x + -y)
⊢ g (x * y - 1) = (g x - 1) * (g y - 1) + g (x - y)
Tactic:
rwa [hg.map_even, mul_neg, neg_add_eq_sub, ← neg_sub, hg.map_even, ← sub_eq_add_neg] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq1
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
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Tactic:
have h := hg.shift_good.Eq6 x
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 : (g - 1) (x + 1) + (g - 1) (x - 1) = ((g - 1) x + 1) * ((g - 1) 2 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq1
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 - 1) (x + 1) + (g - 1) (x - 1) = ((g - 1) x + 1) * ((g - 1) 2 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Tactic:
simp only [Pi.sub_apply, Pi.one_apply] 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 : g (x + 1) - 1 + (g (x - 1) - 1) = (g x - 1 + 1) * (g 2 - 1 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq1
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 + 1) - 1 + (g (x - 1) - 1) = (g x - 1 + 1) * (g 2 - 1 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Tactic:
rwa [sub_add_cancel, hg.map_two, sub_eq_of_eq_add three_add_one_eq_four.symm,
  sub_eq_of_eq_add two_add_one_eq_three.symm, sub_add_sub_comm, mul_two,
  sub_eq_iff_eq_add, one_add_one_eq_two, ← two_mul, ← mul_add_one (α := S)] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq2
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 y : R
⊢ g (x * y + 1) - g (x * y - 1) = g (x + y) - g (x - y)
Tactic:
rw [hg.is_good, hg.alt_good, add_sub_add_left_eq_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_1
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
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
have h : (g - 1) 2 ≠ 1 := λ h0 ↦ by
  rw [Pi.sub_apply, hg.map_two, sub_eq_of_eq_add three_add_one_eq_four.symm,
    ← two_add_one_eq_three, add_left_eq_self] at h0
  exact hg.Schar_ne_two h0
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 : (g - 1) 2 ≠ 1
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_1
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 - 1) 2 ≠ 1
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
replace h := hg.shift_good.Eq7 h x
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 : ((g - 1) (x + 1) + 1) * ((g - 1) (x - 1) + 1) = (g - 1) x ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_1
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 - 1) (x + 1) + 1) * ((g - 1) (x - 1) + 1) = (g - 1) x ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
simp only [Pi.sub_apply, Pi.one_apply, sub_add_cancel] 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 : g (x + 1) * g (x - 1) = (g x - 1) ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_1
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 + 1) * g (x - 1) = (g x - 1) ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
exact h
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_1
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
h0 : (g - 1) 2 = 1
⊢ False
Tactic:
rw [Pi.sub_apply, hg.map_two, sub_eq_of_eq_add three_add_one_eq_four.symm,
  ← two_add_one_eq_three, add_left_eq_self] at h0
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
h0 : 2 = 0
⊢ False
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_1
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
h0 : 2 = 0
⊢ False
Tactic:
exact hg.Schar_ne_two h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.CommCase.Eq3_2
Proof state before:
R : Type u_2
S✝ : Type ?u.184718
inst✝⁴ : Ring R
inst✝³ : Ring S✝
inst✝² : NoZeroDivisors S✝
g✝ : R → S✝
hg✝ : ShiftGood23 g✝
S : Type u_1
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
⊢ (g (x + 1) - g (x - 1)) ^ 2 = 2 ^ 4 * g x
Tactic:
rw [sub_sq', ← sub_eq_of_eq_add (add_sq' (g _) _),
  Eq1 hg, mul_assoc, Eq3_1 hg]
Proof state after:
R : Type u_2
S✝ : Type ?u.184718
inst✝⁴ : Ring R
inst✝³ : Ring S✝
inst✝² : NoZeroDivisors S✝
g✝ : R → S✝
hg✝ : ShiftGood23 g✝
S : Type u_1
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
⊢ (2 * (g x + 1)) ^ 2 - 2 * (g x - 1) ^ 2 - 2 * (g x - 1) ^ 2 = 2 ^ 4 * g x
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.CommCase.Eq3_2
Proof state before:
R : Type u_2
S✝ : Type ?u.184718
inst✝⁴ : Ring R
inst✝³ : Ring S✝
inst✝² : NoZeroDivisors S✝
g✝ : R → S✝
hg✝ : ShiftGood23 g✝
S : Type u_1
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
⊢ (2 * (g x + 1)) ^ 2 - 2 * (g x - 1) ^ 2 - 2 * (g x - 1) ^ 2 = 2 ^ 4 * g x
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_2
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
⊢ (g (x + 1) - g (x - 1)) ^ 2 = 2 ^ 4 * g x
Tactic:
rcases oneVarLift_exists hg x with
  ⟨R', R'comm, φ, -, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, -, g', h0, hg'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
g' : R' → S'
h0 : ∀ (a : R'), g (φ a) = ρ (g' a)
hg' : ShiftGood23 g'
⊢ (g (φ x + 1) - g (φ x - 1)) ^ 2 = 2 ^ 4 * g (φ x)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u_2
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
g' : R' → S'
h0 : ∀ (a : R'), g (φ a) = ρ (g' a)
hg' : ShiftGood23 g'
⊢ (g (φ x + 1) - g (φ x - 1)) ^ 2 = 2 ^ 4 * g (φ x)
Tactic:
rw [← φ.map_one, ← φ.map_add, ← φ.map_sub, h0, h0, ← ρ.map_sub, ← ρ.map_pow,
  CommCase.Eq3_2 hg', h0, ρ.map_mul, ρ.map_pow, map_ofNat]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq4
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 y : R
h : g (x * y + 1) + g (x * y - 1) = (g x - 1) * (g y - 1) + g (x + y) + ((g x - 1) * (g y - 1) + g (x - y))
⊢ 2 * (g (x * y) - g x * g y) = g (x + y) + g (x - y) - 2 * (g x + g y)
Tactic:
rw [Eq1 hg, add_add_add_comm, ← two_mul, ← sub_eq_iff_eq_add', ← mul_sub] 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 y : R
h : 2 * (g (x * y) + 1 - (g x - 1) * (g y - 1)) = g (x + y) + g (x - y)
⊢ 2 * (g (x * y) - g x * g y) = g (x + y) + g (x - y) - 2 * (g x + g y)
Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq4
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 y : R
h : 2 * (g (x * y) + 1 - (g x - 1) * (g y - 1)) = g (x + y) + g (x - y)
⊢ 2 * (g (x * y) - g x * g y) = g (x + y) + g (x - y) - 2 * (g x + g y)
Tactic:
rw [← h, ← mul_sub, sub_sub, sub_one_mul, mul_sub_one, sub_sub, sub_add,
  ← add_sub_assoc, sub_sub_cancel_left, sub_neg_eq_add, add_sub_add_right_eq_sub]
Proof state after:
no goals
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 - 1) (x * 2 + 1) + (g - 1) (x * 2 - 1) =
    (g - 1) (x + 1) * (g - 1) 2 + (g - 1) (x - 1) + ((g - 1) (x - 1) * (g - 1) 2 + (g - 1) (x + 1))
⊢ g (x * 2) = g x * 4
Tactic:
simp only [Pi.sub_apply, Pi.one_apply] 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 :
  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