internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ f' (-x) = f' x
Tactic:
apply hρ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.a
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ ρ (f' (-x)) = ρ (f' x)
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.a
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ ρ (f' (-x)) = ρ (f' x)
Tactic:
rw [← h0, ← h0, φ.map_neg, hf.map_even]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 ≠ -1
Tactic:
intro h1
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ False
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ False
Tactic:
apply hf.map_two_ne_neg_one
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ f 2 = -1
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.oneVarLift_exists
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ f 2 = -1
Tactic:
rw [← map_ofNat φ 2, h0, h1, ρ.map_neg, ρ.map_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq6
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
x : R
⊢ f (x + 1) + f (x - 1) = (f x + 1) * (f 2 - 1)
Tactic:
rcases oneVarLift_exists hf x with
  ⟨R', R'comm, φ, -, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, -, f', h0, hf'⟩
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
f : R → S
hf : GoodCase2 f
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ f (φ x + 1) + f (φ x - 1) = (f (φ x) + 1) * (f 2 - 1)
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq6
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
f : R → S
hf : GoodCase2 f
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ f (φ x + 1) + f (φ x - 1) = (f (φ x) + 1) * (f 2 - 1)
Tactic:
rw [h0, ← φ.map_one, ← φ.map_sub, ← φ.map_add, h0, h0, ← map_ofNat φ 2, h0,
  ← ρ.map_one, ← ρ.map_add, ← ρ.map_add, ← ρ.map_sub, ← ρ.map_mul]
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
f : R → S
hf : GoodCase2 f
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ρ (f' (x + 1) + f' (x - 1)) = ρ ((f' x + 1) * (f' (OfNat.ofNat 2) - 1))
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq6
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
f : R → S
hf : GoodCase2 f
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ρ (f' (x + 1) + f' (x - 1)) = ρ ((f' x + 1) * (f' (OfNat.ofNat 2) - 1))
Tactic:
exact congrArg ρ
  (CommCase.Eq6 hf'.toNontrivialGood hf'.map_even hf'.map_two_ne_neg_one x)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq7
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
x : R
⊢ (f (x + 1) + 1) * (f (x - 1) + 1) = f x ^ 2
Tactic:
rcases oneVarLift_exists hf x with
  ⟨R', R'comm, φ, -, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, -, f', h0, hf'⟩
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
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq7
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
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2
Tactic:
have h2 : f' 2 ≠ 1 := λ h2 ↦ h1 <| by rw [← map_ofNat φ 2, h0, h2, ρ.map_one]
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
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq7
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
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ (f (φ x + 1) + 1) * (f (φ x - 1) + 1) = f (φ x) ^ 2
Tactic:
rw [h0, ← φ.map_one, ← φ.map_sub, ← φ.map_add, h0, h0, ← ρ.map_one,
  ← ρ.map_add, ← ρ.map_add, ← ρ.map_mul, ← ρ.map_pow]
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
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ ρ ((f' (x + 1) + 1) * (f' (x - 1) + 1)) = ρ (f' x ^ 2)
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq7
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
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 ≠ 1
⊢ ρ ((f' (x + 1) + 1) * (f' (x - 1) + 1)) = ρ (f' x ^ 2)
Tactic:
exact congrArg ρ
  (CommCase.Eq7 hf'.toNontrivialGood hf'.map_even hf'.map_two_ne_neg_one h2 x)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.Eq7
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h1 : f 2 ≠ 1
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
f' : R' → S'
h0 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : GoodCase2 f'
h2 : f' 2 = 1
⊢ f 2 = 1
Tactic:
rw [← map_ofNat φ 2, h0, h2, ρ.map_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
have h := Eq1 hf (2 + 1) 2
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f ((2 + 1) * 2 - 1) = f (2 + 1) * f 2 + f (2 + 1 - 2)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f ((2 + 1) * 2 - 1) = f (2 + 1) * f 2 + f (2 + 1 - 2)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [add_sub_cancel_left, hf.map_one, add_zero,
  mul_two, add_sub_assoc, add_sub_cancel_right] at h
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
have h0 := Eq6 hf (2 + 1 + 1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1 + 1 + 1) + f (2 + 1 + 1 - 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1 + 1 + 1) + f (2 + 1 + 1 - 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [add_sub_cancel_right, add_assoc, one_add_one_eq_two, h, ← mul_add_one (f _)] 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 : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1 + 2) = f (2 + 1) * f 2
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
replace h := Eq6 hf (2 + 1)
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + f (2 + 1 - 1) = (f (2 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + f (2 + 1 - 1) = (f (2 + 1) + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [add_sub_cancel_right, add_one_mul (α := S), add_sub_left_comm,
  add_comm, add_right_inj, eq_sub_iff_add_eq] at h
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) * (f 2 + 1) = (f (2 + 1 + 1) + 1) * (f 2 - 1)
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [h, mul_assoc, eq_comm, ← sub_eq_zero, ← mul_sub, mul_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 : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
h : f (2 + 1 + 1) + 1 = f (2 + 1) * (f 2 - 1)
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
clear h
Proof state after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h0 : f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
revert 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 : GoodCase2 f
⊢ f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0 → f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
⊢ f (2 + 1) = 0 ∨ (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0 → f 2 = 1 ∨ f 2 = 0 ∨ f 2 = 3
Tactic:
refine Or.imp (λ h ↦ ?_) (λ h ↦ ?_)
Proof state after:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
⊢ f 2 = 1

case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
⊢ f 2 = 1
Tactic:
have h0 := Eq1 hf 2 (1 + 1)
Proof state after:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f (2 * (1 + 1) - 1) = f 2 * f (1 + 1) + f (2 - (1 + 1))
⊢ f 2 = 1
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f (2 * (1 + 1) - 1) = f 2 * f (1 + 1) + f (2 - (1 + 1))
⊢ f 2 = 1
Tactic:
rw [two_mul, ← add_assoc, add_sub_cancel_right, one_add_one_eq_two, sub_self,
  hf.map_zero, h, eq_comm, add_neg_eq_zero, mul_self_eq_one_iff] at h0
Proof state after:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f 2 = 1 ∨ f 2 = -1
⊢ f 2 = 1
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f (2 + 1) = 0
h0 : f 2 = 1 ∨ f 2 = -1
⊢ f 2 = 1
Tactic:
exact h0.resolve_right hf.map_two_ne_neg_one
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : (f 2 - 1) * (f 2 - 1) - (f 2 + 1) = 0
⊢ f 2 = 0 ∨ f 2 = 3
Tactic:
rw [mul_sub_one, sub_one_mul, sub_sub, sub_add_add_cancel, ← two_mul,
  sub_sub, ← one_add_mul 2 (f 2), ← sub_mul, mul_eq_zero, add_comm] at h
Proof state after:
case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f 2 - (2 + 1) = 0 ∨ f 2 = 0
⊢ f 2 = 0 ∨ f 2 = 3
Theorem: IMOSL.IMO2012A5.Case2.GoodCase2.map_two_cases
Proof state before:
case refine_2
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
h : f 2 - (2 + 1) = 0 ∨ f 2 = 0
⊢ f 2 = 0 ∨ f 2 = 3
Tactic:
exact h.symm.imp_right λ h ↦ (eq_of_sub_eq_zero h).trans two_add_one_eq_three
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
⊢ f (x + 2) = -f x
Tactic:
have h0 := hf.toGoodCase2.Eq6 (x + 1)
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) = (f (x + 1) + 1) * (f 2 - 1)
⊢ f (x + 2) = -f x
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) = (f (x + 1) + 1) * (f 2 - 1)
⊢ f (x + 2) = -f x
Tactic:
rw [h, sub_self, mul_zero, add_sub_cancel_right, add_assoc, one_add_one_eq_two] at h0
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 2) + f x = 0
⊢ f (x + 2) = -f x
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 2) + f x = 0
⊢ f (x + 2) = -f x
Tactic:
exact eq_neg_iff_add_eq_zero.mpr h0
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
⊢ f (x + 4) = f x
Tactic:
have h1 : (2 : R) + 2 = 4 := by norm_num
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
h1 : 2 + 2 = 4
⊢ f (x + 4) = f x
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
h1 : 2 + 2 = 4
⊢ f (x + 4) = f x
Tactic:
rw [← h1, ← add_assoc, h0, h0, neg_neg]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
⊢ 2 + 2 = 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
x : R
⊢ f (x + 2) = f x * -f 2
Tactic:
rw [h0, h, mul_neg_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
h2 : QuasiPeriodic f 2
⊢ 2 + 1 = -1
Tactic:
rwa [two_add_one_eq_three, eq_neg_iff_add_eq_zero, three_add_one_eq_four]
Proof state after:
no goals