internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_2
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x : R), 2 • ρ (0 * x) = ρ 0 * ρ x
Tactic:
intro x
Proof state after:
case intro.refine_2
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (0 * x) = ρ 0 * ρ x
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_2
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (0 * x) = ρ 0 * ρ x
Tactic:
rw [zero_mul, ρ.map_zero, zero_mul, nsmul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_3
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x : R), 2 • ρ (x * 0) = ρ x * ρ 0
Tactic:
intro x
Proof state after:
case intro.refine_3
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (x * 0) = ρ x * ρ 0
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_3
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (x * 0) = ρ x * ρ 0
Tactic:
rw [mul_zero, ρ.map_zero, mul_zero, nsmul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_4
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x₁ x₂ y : R), 2 • ρ (x₁ * y) = ρ x₁ * ρ y → 2 • ρ (x₂ * y) = ρ x₂ * ρ y → 2 • ρ ((x₁ + x₂) * y) = ρ (x₁ + x₂) * ρ y
Tactic:
intro x₁ x₂ y hx₁ hx₂
Proof state after:
case intro.refine_4
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x₁ x₂ y : R
hx₁ : 2 • ρ (x₁ * y) = ρ x₁ * ρ y
hx₂ : 2 • ρ (x₂ * y) = ρ x₂ * ρ y
⊢ 2 • ρ ((x₁ + x₂) * y) = ρ (x₁ + x₂) * ρ y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_4
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x₁ x₂ y : R
hx₁ : 2 • ρ (x₁ * y) = ρ x₁ * ρ y
hx₂ : 2 • ρ (x₂ * y) = ρ x₂ * ρ y
⊢ 2 • ρ ((x₁ + x₂) * y) = ρ (x₁ + x₂) * ρ y
Tactic:
rw [add_mul, ρ.map_add, nsmul_add, hx₁, hx₂, ρ.map_add, add_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_5
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y₁ y₂ : R), 2 • ρ (x * y₁) = ρ x * ρ y₁ → 2 • ρ (x * y₂) = ρ x * ρ y₂ → 2 • ρ (x * (y₁ + y₂)) = ρ x * ρ (y₁ + y₂)
Tactic:
intro x y₁ y₂ hy₁ hy₂
Proof state after:
case intro.refine_5
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y₁ y₂ : R
hy₁ : 2 • ρ (x * y₁) = ρ x * ρ y₁
hy₂ : 2 • ρ (x * y₂) = ρ x * ρ y₂
⊢ 2 • ρ (x * (y₁ + y₂)) = ρ x * ρ (y₁ + y₂)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_5
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y₁ y₂ : R
hy₁ : 2 • ρ (x * y₁) = ρ x * ρ y₁
hy₂ : 2 • ρ (x * y₂) = ρ x * ρ y₂
⊢ 2 • ρ (x * (y₁ + y₂)) = ρ x * ρ (y₁ + y₂)
Tactic:
rw [mul_add, ρ.map_add, nsmul_add, hy₁, hy₂, ρ.map_add, mul_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_6
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y : R), 2 • ρ (x * y) = ρ x * ρ y → 2 • ρ (-x * y) = ρ (-x) * ρ y
Tactic:
intro x y h2
Proof state after:
case intro.refine_6
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (-x * y) = ρ (-x) * ρ y
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_6
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (-x * y) = ρ (-x) * ρ y
Tactic:
rw [neg_mul, ρ.map_neg, ρ.map_neg, neg_mul, smul_neg, h2]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_7
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y : R), 2 • ρ (x * y) = ρ x * ρ y → 2 • ρ (x * -y) = ρ x * ρ (-y)
Tactic:
intro x y h2
Proof state after:
case intro.refine_7
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (x * -y) = ρ x * ρ (-y)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof state before:
case intro.refine_7
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
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 : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (x * -y) = ρ x * ρ (-y)
Tactic:
rw [mul_neg, ρ.map_neg, ρ.map_neg, mul_neg, smul_neg, h2]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase23.solution
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
⊢ ∃ R' x φ ι, ∀ (x_1 : R), f x_1 = ι (RestrictedSq (φ x_1) - 1)
Tactic:
rcases (RShiftGood23.shift_mk_iff.mpr ⟨hf, h⟩).solution with ⟨R', _, φ, ι, h0⟩
Proof state after:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
⊢ ∃ R' x φ ι, ∀ (x_1 : R), f x_1 = ι (RestrictedSq (φ x_1) - 1)
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase23.solution
Proof state before:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
⊢ ∃ R' x φ ι, ∀ (x_1 : R), f x_1 = ι (RestrictedSq (φ x_1) - 1)
Tactic:
refine ⟨R', _, φ, ι, λ x ↦ ?_⟩
Proof state after:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = ι (RestrictedSq (φ x) - 1)
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase23.solution
Proof state before:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = ι (RestrictedSq (φ x) - 1)
Tactic:
rw [ι.map_sub, ← h0, ι.map_one]
Proof state after:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = (f + 1) x - 1
Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase23.solution
Proof state before:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = (f + 1) x - 1
Tactic:
exact (add_sub_cancel_right _ _).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
⊢ 2 = 0
Tactic:
refine hf.period_imp_zero λ x ↦ ?_
Proof state after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
x : R
⊢ f (x + 2) = f x
Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two
Proof state before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
x : R
⊢ f (x + 2) = f x
Tactic:
rcases CommSubring.oneVarCommLiftDomain_exists hf.toNontrivialGood x with
  ⟨R', R'comm, φ, -, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f', h1, hf'⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f (φ x + 2) = f (φ x)
Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f (φ x + 2) = f (φ x)
Tactic:
rw [← map_ofNat φ 2, ← φ.map_add, h1, h1, CommCase.two_periodic_of_map_two hf']
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 = -1
Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x
Tactic:
refine map_even_of_map_one hf'.is_good (hρ ?_)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' (-1)) = ρ 0
Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' (-1)) = ρ 0
Tactic:
rw [← h1, φ.map_neg, φ.map_one, h, ρ.map_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 = -1
Tactic:
apply hρ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0.a
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' 2) = ρ (-1)
Theorem: IMOSL.IMO2012A5.Case2.CharTwo'_of_map_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h0.a
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
h : f (-1) = 0
h0 : f 2 = -1
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
x : R'
S' : Type u_1
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h1 : ∀ (a : R'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ρ (f' 2) = ρ (-1)
Tactic:
rw [← h1, map_ofNat, h0, ρ.map_neg, ρ.map_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sq_sub_one_is_good
Proof state before:
R : Type u_1
inst✝ : CommRing R
x✝¹ x✝ : R
⊢ (fun x => x ^ 2 - 1) (x✝¹ * x✝ + 1) =
    (fun x => x ^ 2 - 1) x✝¹ * (fun x => x ^ 2 - 1) x✝ + (fun x => x ^ 2 - 1) (x✝¹ + x✝)
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_left
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |r * ε| < 1
Tactic:
apply (hε (k * ⌈|r|⌉.natAbs)).trans_le'
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |r * ε| ≤ (k * ⌈|r|⌉.natAbs) • |ε|
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_left
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |r * ε| ≤ (k * ⌈|r|⌉.natAbs) • |ε|
Tactic:
rw [abs_mul, mul_nsmul', nsmul_eq_mul ⌈|r|⌉.natAbs]
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|r| * |ε|) ≤ k • (↑⌈|r|⌉.natAbs * |ε|)
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_left
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|r| * |ε|) ≤ k • (↑⌈|r|⌉.natAbs * |ε|)
Tactic:
refine nsmul_le_nsmul_right (mul_le_mul_of_nonneg_right ?_ (abs_nonneg ε)) k
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_left
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs
Tactic:
rw [← Int.cast_natCast ⌈|r|⌉.natAbs, ← Int.ceil_le]
Proof state after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs
Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_left
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs
Tactic:
exact Int.le_natAbs
Proof state after:
no goals