awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f

Tactic:
⟨m, hm, hx.apply_iterate n⟩

Premises used: Set.Mem, setOf, Function.IsPeriodicPt.apply_iterate, And.intro, Function.periodicPts, Exists.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f

Tactic:
exact ⟨m, hm, hx.apply_iterate n⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ minimalPeriod f (f x) = minimalPeriod f x

Tactic:
minimalPeriod_apply_iterate hx 1

Premises used: Nat.iterate, Function.minimalPeriod_apply_iterate, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
by_contra! : ∀ (hmn' : n < m), False
⊢ m ≤ n

Tactic:
by_contra! hmn'
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
⊢ f^[m - n] (f^[n] x) = f^[n] x

Tactic:
rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn

Premises used: Function.iterate_add_apply, Nat.add_sub_of_le, LT.lt.le, add_comm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
hmn₁ : f^[m - n] (f^[n] x) = f^[n] x
⊢ n < m

Tactic:
rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn

Premises used: Function.iterate_add_apply, Nat.add_sub_of_le, LT.lt.le, add_comm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False

Tactic:
((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
    (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
      (minimalPeriod_pos_iff_mem_periodicPts.1 hm.pos) hmn)).trans (Nat.sub_le m n)).not_gt hm

Premises used: Function.IsPeriodicPt.minimalPeriod_le, LT.lt.pos, Nat.sub_le, Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate, LE.le.not_gt, Function.minimalPeriod_pos_iff_mem_periodicPts, Iff.mp, LE.le.trans, tsub_pos_of_lt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False

Tactic:
exact ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
    (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
      (minimalPeriod_pos_iff_mem_periodicPts.1 hm.pos) hmn)).trans (Nat.sub_le m n)).not_gt hm

Premises used: Function.IsPeriodicPt.minimalPeriod_le, LT.lt.pos, Nat.sub_le, Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate, LE.le.not_gt, Function.minimalPeriod_pos_iff_mem_periodicPts, Iff.mp, LE.le.trans, tsub_pos_of_lt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ InjOn.{0, u_1} (β := α) (fun (x_1 : ℕ) ↦ f^[x_1] x) (Iio (minimalPeriod f x))

Tactic:
fun _m hm _n hn hmn ↦ (le_of_lt_minimalPeriod_of_iterate_eq hm hmn).antisymm
    (le_of_lt_minimalPeriod_of_iterate_eq hn hmn.symm)

Premises used: LE.le.antisymm, Function.le_of_lt_minimalPeriod_of_iterate_eq, Set.InjOn, Eq.symm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hn : n < minimalPeriod f x
⊢ f^[m] x = f^[n] x ↔ m = n

Tactic:
iterate_injOn_Iio_minimalPeriod.eq_iff hm hn

Premises used: Function.iterate_injOn_Iio_minimalPeriod, Set.InjOn.eq_iff
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
x : α
⊢ minimalPeriod id x = 1

Tactic:
((is_periodic_id _ _).minimalPeriod_le Nat.one_pos).antisymm
    (Nat.succ_le_of_lt ((is_periodic_id _ _).minimalPeriod_pos Nat.one_pos))

Premises used: Function.IsPeriodicPt.minimalPeriod_le, Nat.one_pos, Nat.succ_le_of_lt, LE.le.antisymm, Function.is_periodic_id, Function.IsPeriodicPt.minimalPeriod_pos
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
refine_1 : ∀ (h : minimalPeriod f x = 1), IsFixedPt f x
refine_2 : ∀ (h : IsFixedPt f x), minimalPeriod f x = 1
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
refine_1 : IsFixedPt f^[1] x
⊢ IsFixedPt f x

Tactic:
rw [← iterate_one f]

Premises used: Function.iterate_one
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f^[1] x

Tactic:
Function.IsPeriodicPt.isFixedPt ?_

Premises used: Function.IsPeriodicPt.isFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
refine_1 : IsPeriodicPt f (minimalPeriod f x) x
⊢ IsPeriodicPt f 1 x

Tactic:
rw [← h]
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
isPeriodicPt_minimalPeriod f x

Premises used: Function.isPeriodicPt_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
exact isPeriodicPt_minimalPeriod f x

Premises used: Function.isPeriodicPt_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Tactic:
((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
        (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

Premises used: Function.IsPeriodicPt.minimalPeriod_le, Nat.one_pos, Nat.succ_le_of_lt, LE.le.antisymm, Function.IsFixedPt.isPeriodicPt, Function.IsPeriodicPt.minimalPeriod_pos, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Tactic:
exact
      ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
        (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

Premises used: Function.IsPeriodicPt.minimalPeriod_le, Nat.one_pos, Nat.succ_le_of_lt, LE.le.antisymm, Function.IsFixedPt.isPeriodicPt, Function.IsPeriodicPt.minimalPeriod_pos, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
inst : Subsingleton α
⊢ minimalPeriod f x = 1

Tactic:
simp [nontriviality]
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hx : IsPeriodicPt f n x
hn : n < minimalPeriod f x
⊢ n = 0

Tactic:
Eq.symm <|
    (eq_or_lt_of_le <| n.zero_le).resolve_right fun hn0 => not_lt.2 (hx.minimalPeriod_le hn0) hn

Premises used: Iff.mpr, Function.IsPeriodicPt.minimalPeriod_le, Nat.zero_le, eq_or_lt_of_le, not_lt, Or.resolve_right, Eq.symm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ∣ n

Tactic:
(eq_or_lt_of_le <| n.zero_le).elim (fun hn0 => hn0 ▸ Nat.dvd_zero _) fun hn0 =>
    Nat.dvd_iff_mod_eq_zero.2 <|
      (hx.mod <| isPeriodicPt_minimalPeriod f x).eq_zero_of_lt_minimalPeriod <|
        Nat.mod_lt _ <| hx.minimalPeriod_pos hn0

Premises used: Iff.mpr, Nat.zero_le, Function.IsPeriodicPt.eq_zero_of_lt_minimalPeriod, Function.isPeriodicPt_minimalPeriod, Nat.dvd_zero, Eq.rec, eq_or_lt_of_le, Nat.mod_lt, Function.IsPeriodicPt.mod, Nat.dvd_iff_mod_eq_zero, Function.IsPeriodicPt.minimalPeriod_pos, Or.elim, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ IsPeriodicPt f n x ↔ minimalPeriod f x ∣ n

Tactic:
⟨IsPeriodicPt.minimalPeriod_dvd, fun h => (isPeriodicPt_minimalPeriod f x).trans_dvd h⟩

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.minimalPeriod_dvd, Function.IsPeriodicPt.trans_dvd, Iff.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
f : α → α
x : α
g : β → β
y : β
simp_rw : minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), minimalPeriod f x ∣ n ↔ minimalPeriod g y ∣ n
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y

Tactic:
simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]

Premises used: Nat.dvd_right_iff_eq, Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
rw : IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x
⊢ minimalPeriod (f ∘ g) x ∣ (minimalPeriod f x).lcm (minimalPeriod g x)

Tactic:
rw [← isPeriodicPt_iff_minimalPeriod_dvd]

Premises used: Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x

Tactic:
(isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.comp_lcm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x

Tactic:
exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.comp_lcm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a : minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n
a₁ : minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x
⊢ minimalPeriod f^[n] x = minimalPeriod f x / (minimalPeriod f x).gcd n

Tactic:
apply Nat.dvd_antisymm

Premises used: Nat.dvd_antisymm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a : IsPeriodicPt f^[n] (minimalPeriod f x / (minimalPeriod f x).gcd n) x
⊢ minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n

Tactic:
apply IsPeriodicPt.minimalPeriod_dvd

Premises used: Function.IsPeriodicPt.minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a : f^[n / (minimalPeriod f x).gcd n]^[minimalPeriod f x] x = x
⊢ IsPeriodicPt f^[n] (minimalPeriod f x / (minimalPeriod f x).gcd n) x

Tactic:
rw [IsPeriodicPt, IsFixedPt, ← iterate_mul, ← Nat.mul_div_assoc _ (gcd_dvd_left _ _),
      mul_comm, Nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, iterate_mul]

Premises used: Nat.gcd_dvd_left, Function.IsPeriodicPt, Function.iterate_mul, mul_comm, Nat.gcd_dvd_right, Function.IsFixedPt, Nat.mul_div_assoc
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n / (minimalPeriod f x).gcd n]^[minimalPeriod f x] x = x

Tactic:
(isPeriodicPt_minimalPeriod f x).iterate _

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt, Function.IsPeriodicPt.iterate, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n / (minimalPeriod f x).gcd n]^[minimalPeriod f x] x = x

Tactic:
exact (isPeriodicPt_minimalPeriod f x).iterate _

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a : minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n)
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x

Tactic:
apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)

Premises used: Nat.coprime_div_gcd_div_gcd, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a :
  minimalPeriod f x / (minimalPeriod f x).gcd n * (minimalPeriod f x).gcd n ∣
    minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n) * (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n)

Tactic:
apply Nat.dvd_of_mul_dvd_mul_right h

Premises used: Nat.dvd_of_mul_dvd_mul_right
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a : minimalPeriod f x ∣ n * minimalPeriod f^[n] x
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n * (minimalPeriod f x).gcd n ∣
    minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n) * (minimalPeriod f x).gcd n

Tactic:
rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
      mul_comm]

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel, mul_assoc, mul_comm, Nat.gcd_dvd_right
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a : IsPeriodicPt f (n * minimalPeriod f^[n] x) x
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x

Tactic:
apply IsPeriodicPt.minimalPeriod_dvd

Premises used: Function.IsPeriodicPt.minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
a : f^[n]^[minimalPeriod f^[n] x] x = x
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x

Tactic:
rw [IsPeriodicPt, IsFixedPt, iterate_mul]

Premises used: Function.IsPeriodicPt, Function.iterate_mul, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x

Tactic:
isPeriodicPt_minimalPeriod _ _

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x

Tactic:
exact isPeriodicPt_minimalPeriod _ _

Premises used: Function.isPeriodicPt_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : n ≠ 0
⊢ minimalPeriod f^[n] x = minimalPeriod f x / (minimalPeriod f x).gcd n

Tactic:
minimalPeriod_iterate_eq_div_gcd_aux <| gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero h)

Premises used: Nat.pos_of_ne_zero, Nat.gcd_pos_of_pos_right, _private.0.Function.minimalPeriod_iterate_eq_div_gcd_aux
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : x ∈ periodicPts f
⊢ minimalPeriod f^[n] x = minimalPeriod f x / (minimalPeriod f x).gcd n

Tactic:
minimalPeriod_iterate_eq_div_gcd_aux <|
    gcd_pos_of_pos_left n (minimalPeriod_pos_iff_mem_periodicPts.mpr h)

Premises used: Iff.mpr, Nat.gcd_pos_of_pos_left, Function.minimalPeriod_pos_iff_mem_periodicPts, _private.0.Function.minimalPeriod_iterate_eq_div_gcd_aux
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ periodicOrbit f x = (↑(List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) : Cycle α)

Tactic:
rfl

Premises used: Function.periodicOrbit, rfl
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ periodicOrbit f x = Cycle.map (fun (n : ℕ) ↦ f^[n] x) (↑(List.range (minimalPeriod f x)) : Cycle ℕ)

Tactic:
rfl

Premises used: Function.periodicOrbit, Quot.map, Quotient.map', Cycle.map, rfl
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
rw :
  Cycle.length.{u_1} (α := α) (↑(List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) : Cycle α) =
    minimalPeriod f x
rw₁ : List.length.{u_1} (α := α) (List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) = minimalPeriod f x
rw₂ : (List.range (minimalPeriod f x)).length = minimalPeriod f x
rw₃ rw₄ : minimalPeriod f x = minimalPeriod f x
⊢ (periodicOrbit f x).length = minimalPeriod f x

Tactic:
rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]

Premises used: List.length_range, Cycle.length_coe, Function.periodicOrbit, List.length_map
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
simp : minimalPeriod f x = 0 ↔ x ∉ periodicPts f
⊢ periodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f

Tactic:
simp only [periodicOrbit.eq_1, Cycle.coe_eq_nil, List.map_eq_nil_iff, List.range_eq_nil]

Premises used: List.map_eq_nil_iff, Cycle.coe_eq_nil, List.range_eq_nil, Function.periodicOrbit.eq_1
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Tactic:
minimalPeriod_eq_zero_iff_notMem_periodicPts

Premises used: Function.minimalPeriod_eq_zero_iff_notMem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Tactic:
exact minimalPeriod_eq_zero_iff_notMem_periodicPts

Premises used: Function.minimalPeriod_eq_zero_iff_notMem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : x ∉ periodicPts f
⊢ periodicOrbit f x = Cycle.nil

Tactic:
periodicOrbit_eq_nil_iff_not_periodic_pt.2 h

Premises used: Iff.mpr, Function.periodicOrbit_eq_nil_iff_not_periodic_pt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
simp : (∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ (n : ℕ), f^[n] x = y
⊢ y ∈ periodicOrbit f x ↔ ∃ (n : ℕ), f^[n] x = y

Tactic:
simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]

Premises used: Cycle.mem_coe_iff, List.mem_range, Function.periodicOrbit, List.mem_map
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
mpr : (∃ (n : ℕ), f^[n] x = y) → ∃ a < minimalPeriod f x, f^[a] x = y
⊢ (∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ (n : ℕ), f^[n] x = y

Tactic:
use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
right : f^[n % minimalPeriod f x] x = f^[n] x
⊢ ∃ a < minimalPeriod f x, f^[a] x = f^[n] x

Tactic:
use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)

Premises used: Function.minimalPeriod_pos_of_mem_periodicPts, Nat.mod_lt, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
right right₁ : f^[n] x = f^[n] x
⊢ f^[n % minimalPeriod f x] x = f^[n] x

Tactic:
rw [iterate_mod_minimalPeriod_eq]

Premises used: Function.iterate_mod_minimalPeriod_eq
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicOrbit f x

Tactic:
simp [hx]
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ ∃ (n : ℕ), f^[n] x = x

Tactic:
simpa only [← mem_periodicOrbit_iff hx] using iterate_mem_periodicOrbit hx 0

Premises used: OfNat.ofNat, Function.iterate_mem_periodicOrbit, Function.mem_periodicOrbit_iff
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ x ∈ periodicOrbit f x

Tactic:
simp [hx]
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
rw : ∀ x_1 ∈ List.range (minimalPeriod f x), ∀ y ∈ List.range (minimalPeriod f x), f^[x_1] x = f^[y] x → x_1 = y
⊢ (periodicOrbit f x).Nodup

Tactic:
rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on List.nodup_range]

Premises used: List.nodup_map_iff_inj_on, Cycle.nodup_coe_iff, Function.periodicOrbit, List.nodup_range
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : f^[m] x = f^[n] x
rw : ∀ (hm : m < minimalPeriod f x) (n : ℕ) (hn : n < minimalPeriod f x) (hmn : f^[m] x = f^[n] x), m = n
⊢ m = n

Tactic:
rw [List.mem_range] at hm hn

Premises used: List.mem_range
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
rwa rwa₁ rwa₂ rwa₃ : ∀ (hmn : m = n), m = n
⊢ m = n

Tactic:
rwa [iterate_eq_iterate_iff_of_lt_minimalPeriod hm hn] at hmn

Premises used: Function.iterate_eq_iterate_iff_of_lt_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ List.length.{u_1} (α := α) (List.rotate (List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) n) =
    List.length.{u_1} (α := α) (List.map (fun (n_1 : ℕ) ↦ f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))

Tactic:
simp [minimalPeriod_apply_iterate hx]

Premises used: Function.minimalPeriod_apply_iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n m : ℕ
h : m < List.length.{u_1} (α := α) (List.rotate (List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) n)
h_1 :
  m < List.length.{u_1} (α := α) (List.map (fun (n_1 : ℕ) ↦ f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))
⊢ List.get (List.rotate (List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) n)
      (⟨m, h⟩ :
        Fin
          (List.length.{u_1} (α := α)
            (List.rotate (List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) n))) =
    List.get (List.map (fun (n_1 : ℕ) ↦ f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))
      (⟨m, h_1⟩ :
        Fin
          (List.length.{u_1} (α := α)
            (List.map (fun (n_1 : ℕ) ↦ f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))))

Tactic:
simp [List.getElem_rotate, iterate_add_apply]

Premises used: Function.iterate_add_apply, List.getElem_rotate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ periodicOrbit f (f x) = periodicOrbit f x

Tactic:
periodicOrbit_apply_iterate_eq hx 1

Premises used: Function.periodicOrbit_apply_iterate_eq, Nat.iterate, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
pos : ∀ (hx : x ∈ periodicPts f), Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
neg : ∀ (hx : x ∉ periodicPts f), Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
by_cases hx : x ∈ periodicPts f

Premises used: Function.periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x

Tactic:
have hx' := minimalPeriod_pos_of_mem_periodicPts hx
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
⊢ minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x

Tactic:
have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
pos :
  (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) ↔
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]

Premises used: Cycle.chain_range_succ, Cycle.map_coe, Function.periodicOrbit, Cycle.chain_map