internlm/Lean-Github huggingface dataset:
Theorem: SciLean.BasisDuality.toDual.arg_x.IsAffineMap_rule
Proof state before:
R : Type ?u.127261
X✝ : Type ?u.127264
Y✝ : Type ?u.127267
Z✝ : Type ?u.127270
ι : Type ?u.127273
E : ι → Type ?u.127278
inst✝²⁴ : CommRing R
inst✝²³ : AddCommGroup X✝
inst✝²² : Module R X✝
inst✝²¹ : AddCommGroup Y✝
inst✝²⁰ : Module R Y✝
inst✝¹⁹ : AddCommGroup Z✝
inst✝¹⁸ : Module R Z✝
inst✝¹⁷ : IndexType ι
inst✝¹⁶ : LawfulIndexType ι
inst✝¹⁵ : DecidableEq ι
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module R (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.130530
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.130617
inst✝ : FinVec IZ K Z
⊢ IsAffineMap K fun x => toDual x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.fromDual.arg_x.IsAffineMap_rule
Proof state before:
R : Type ?u.131101
X✝ : Type ?u.131104
Y✝ : Type ?u.131107
Z✝ : Type ?u.131110
ι : Type ?u.131113
E : ι → Type ?u.131118
inst✝²⁴ : CommRing R
inst✝²³ : AddCommGroup X✝
inst✝²² : Module R X✝
inst✝²¹ : AddCommGroup Y✝
inst✝²⁰ : Module R Y✝
inst✝¹⁹ : AddCommGroup Z✝
inst✝¹⁸ : Module R Z✝
inst✝¹⁷ : IndexType ι
inst✝¹⁶ : LawfulIndexType ι
inst✝¹⁵ : DecidableEq ι
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module R (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.134370
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.134457
inst✝ : FinVec IZ K Z
⊢ IsAffineMap K fun x => fromDual x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Iran1998P9.compute_norm
Proof state before:
v : EuclideanSpace ℝ (Fin 3)
⊢ ‖v‖ = √(∑ i : Fin 3, v i ^ 2)
Tactic:
rw[EuclideanSpace.norm_eq v]
Proof state after:
v : EuclideanSpace ℝ (Fin 3)
⊢ √(∑ i : Fin 3, ‖v i‖ ^ 2) = √(∑ i : Fin 3, v i ^ 2)
Theorem: Iran1998P9.compute_norm
Proof state before:
v : EuclideanSpace ℝ (Fin 3)
⊢ √(∑ i : Fin 3, ‖v i‖ ^ 2) = √(∑ i : Fin 3, v i ^ 2)
Tactic:
congr
Proof state after:
case e_x.e_f
v : EuclideanSpace ℝ (Fin 3)
⊢ (fun i => ‖v i‖ ^ 2) = fun i => v i ^ 2
Theorem: Iran1998P9.compute_norm
Proof state before:
case e_x.e_f
v : EuclideanSpace ℝ (Fin 3)
⊢ (fun i => ‖v i‖ ^ 2) = fun i => v i ^ 2
Tactic:
ext
Proof state after:
case e_x.e_f.h
v : EuclideanSpace ℝ (Fin 3)
x✝ : Fin 3
⊢ ‖v x✝‖ ^ 2 = v x✝ ^ 2
Theorem: Iran1998P9.compute_norm
Proof state before:
case e_x.e_f.h
v : EuclideanSpace ℝ (Fin 3)
x✝ : Fin 3
⊢ ‖v x✝‖ ^ 2 = v x✝ ^ 2
Tactic:
rw [Real.norm_eq_abs, sq_abs]
Proof state after:
no goals
Theorem: IntegersInACircle.lemma1
Proof state before:
a : ℤ
h1 : a % 100 = 0
h2 : 0 < a
h3 : a < 300
⊢ a = 200 ∨ a = 100
Tactic:
omega
Proof state after:
no goals
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Tactic:
let g := λ (i:ℕ) ↦ y + (i:ZMod 101)
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Tactic:
have hg: ∀ (x : ℕ),
    x ∈ Finset.range 101 → ∀ (y : ℕ), y ∈ Finset.range 101 → g x = g y → x = y := by
  intro a ha b hb hgab
  dsimp [g] at hgab
  have h5 : (a : ZMod 101) = (b : ZMod 101) := by linear_combination hgab
  have h8: a % 101 = b % 101 := Iff.mp (ZMod.natCast_eq_natCast_iff' a b 101) h5
  rw [Finset.mem_range] at ha hb
  rwa [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at h8
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Tactic:
rw[← Finset.sum_image hg]
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ x ∈ Finset.image (fun x => g x) (Finset.range 101), f x
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
h3 : Finset.image g (Finset.range 101) = Finset.univ
⊢ ∑ z : ZMod 101, f z = ∑ x ∈ Finset.image (fun x => g x) (Finset.range 101), f x
Tactic:
rw[h3]
Proof state after:
no goals
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
Tactic:
intro a ha b hb hgab
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : g a = g b
⊢ a = b
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : g a = g b
⊢ a = b
Tactic:
dsimp [g] at hgab
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
⊢ a = b
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
⊢ a = b
Tactic:
have h5 : (a : ZMod 101) = (b : ZMod 101) := by linear_combination hgab
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
⊢ a = b
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
⊢ a = b
Tactic:
have h8: a % 101 = b % 101 := Iff.mp (ZMod.natCast_eq_natCast_iff' a b 101) h5
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b
Tactic:
rw [Finset.mem_range] at ha hb
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a < 101
b : ℕ
hb : b < 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a < 101
b : ℕ
hb : b < 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b
Tactic:
rwa [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at h8
Proof state after:
no goals
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
⊢ ↑a = ↑b
Tactic:
linear_combination hgab
Proof state after:
no goals
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ Finset.image g (Finset.range 101) = Finset.univ
Tactic:
rw [Finset.eq_univ_iff_forall]
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∀ (x : ZMod 101), x ∈ Finset.image g (Finset.range 101)
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∀ (x : ZMod 101), x ∈ Finset.image g (Finset.range 101)
Tactic:
intro a
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ a ∈ Finset.image g (Finset.range 101)
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ a ∈ Finset.image g (Finset.range 101)
Tactic:
rw [Finset.mem_image]
Proof state after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ ∃ a_1 ∈ Finset.range 101, g a_1 = a
Theorem: IntegersInACircle.lemma2
Proof state before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ ∃ a_1 ∈ Finset.range 101, g a_1 = a
Tactic:
use (a - y).val
Proof state after:
case h
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101 ∧ g (a - y).val = a
Theorem: IntegersInACircle.lemma2
Proof state before:
case h
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101 ∧ g (a - y).val = a
Tactic:
constructor
Proof state after:
case h.left
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101

case h.right
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ g (a - y).val = a
Theorem: IntegersInACircle.lemma2
Proof state before:
case h.left
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101
Tactic:
exact Finset.mem_range.mpr (ZMod.val_lt (a - y))
Proof state after:
no goals
Theorem: IntegersInACircle.lemma2
Proof state before:
case h.right
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ g (a - y).val = a
Tactic:
simp [g]
Proof state after:
no goals
Theorem: Imo2006P5.Int.natAbs_eq_of_chain_dvd
Proof state before:
l : Cycle ℤ
x y : ℤ
hl : Cycle.Chain (fun x x_1 => x ∣ x_1) l
hx : x ∈ l
hy : y ∈ l
⊢ x.natAbs = y.natAbs
Tactic:
rw [Cycle.chain_iff_pairwise] at hl
Proof state after:
l : Cycle ℤ
x y : ℤ
hl : ∀ a ∈ l, ∀ b ∈ l, a ∣ b
hx : x ∈ l
hy : y ∈ l
⊢ x.natAbs = y.natAbs
Theorem: Imo2006P5.Int.natAbs_eq_of_chain_dvd
Proof state before:
l : Cycle ℤ
x y : ℤ
hl : ∀ a ∈ l, ∀ b ∈ l, a ∣ b
hx : x ∈ l
hy : y ∈ l
⊢ x.natAbs = y.natAbs
Tactic:
exact Int.natAbs_eq_of_dvd_dvd (hl x hx y hy) (hl y hy x hx)
Proof state after:
no goals
Theorem: Imo2006P5.Int.add_eq_add_of_natAbs_eq_of_natAbs_eq
Proof state before:
a b c d : ℤ
hne : a ≠ b
h₁ : (c - a).natAbs = (d - b).natAbs
h₂ : (c - b).natAbs = (d - a).natAbs
⊢ a + b = c + d
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
let C : Cycle ℤ := (periodicOrbit (fun x => P.eval x) t).map fun x => P.eval x - x
Proof state after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
have HC : ∀ {n : ℕ}, (fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t ∈ C := by
  intro n
  rw [Cycle.mem_map, Function.iterate_succ_apply']
  exact ⟨_, iterate_mem_periodicOrbit ht n, rfl⟩
Proof state after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
have Habs :
  ∀ m n : ℕ,
    ((fun x => P.eval x)^[m + 1] t - (fun x => P.eval x)^[m] t).natAbs =
      ((fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t).natAbs :=
  fun m n => Int.natAbs_eq_of_chain_dvd Hdvd HC HC
Proof state after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
⊢ ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Tactic:
intro n
Proof state after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Tactic:
rw [Cycle.mem_map, Function.iterate_succ_apply']
Proof state after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ ∃ a ∈ periodicOrbit (fun x => Polynomial.eval x P) t,
    Polynomial.eval a P - a =
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ ∃ a ∈ periodicOrbit (fun x => Polynomial.eval x P) t,
    Polynomial.eval a P - a =
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t
Tactic:
exact ⟨_, iterate_mem_periodicOrbit ht n, rfl⟩
Proof state after:
no goals
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ Cycle.Chain (fun x x_1 => x ∣ x_1) C
Tactic:
rw [Cycle.chain_map, periodicOrbit_chain' _ ht]
Proof state after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ ∀ (n : ℕ),
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ ∀ (n : ℕ),
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
Tactic:
intro n
Proof state after:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
n : ℕ
⊢ Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
n : ℕ
⊢ Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t ∣
    Polynomial.eval ((fun x => Polynomial.eval x P)^[n + 1] t) P - (fun x => Polynomial.eval x P)^[n + 1] t
Tactic:
convert sub_dvd_eval_sub ((fun x => P.eval x)^[n + 1] t) ((fun x => P.eval x)^[n] t) P <;>
  rw [Function.iterate_succ_apply']
Proof state after:
no goals
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
case pos
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
have Heq :
  ∀ m n : ℕ,
    (fun x => P.eval x)^[m + 1] t - (fun x => P.eval x)^[m] t =
      (fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t :=
  fun m n => Cycle.chain_iff_pairwise.1 HC' _ HC _ HC
Proof state after:
case pos
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Theorem: Imo2006P5.Polynomial.isPeriodicPt_eval_two
Proof state before:
case pos
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
Tactic:
rcases ht with ⟨_ | k, hk, hk'⟩
Proof state after:
case pos.intro.zero.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
hk : 0 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) 0 t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t

case pos.intro.succ.intro
P : ℤ[X]
t : ℤ
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
IH : ∀ (n : ℕ), ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
k : ℕ
hk : k + 1 > 0
hk' : IsPeriodicPt (fun x => Polynomial.eval x P) (k + 1) t
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t