awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (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)

Tactic:
⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩

Premises used: HSub.hSub, Nat.lt_succ_self, And.intro, Iff.intro, LT.lt.trans, OfNat.ofNat, Nat.succ, Function.minimalPeriod
-- 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)
pos₁ :
  ∀ (H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)),
    r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
⊢ (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)

Tactic:
refine ⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
-- 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
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
pos : ∀ (hM' : n = minimalPeriod f x - succ 0), r (f^[n] x) (f^[n + 1] x)
pos₁ : ∀ (hM' : n < minimalPeriod f x - succ 0), r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'

Premises used: eq_or_lt_of_le, Nat.lt_succ_iff, Iff.mp
-- 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
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + 1] x)
pos₁ : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
pos₂ pos₃ pos₄ pos₅ : r (f^[minimalPeriod f x - succ 0] x) x
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
rwa [hM', hM, iterate_minimalPeriod]

Premises used: Function.iterate_minimalPeriod
-- 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
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
H _ hM'
-- 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
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
exact H _ hM'
-- 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
pos : r (f^[minimalPeriod f x - succ 0] x) x
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)

Tactic:
rw [iterate_zero_apply]

Premises used: Function.iterate_zero_apply
-- 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) x

Tactic:
nth_rw 3 [← @iterate_minimalPeriod α f x]

Premises used: Function.iterate_minimalPeriod
-- 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + succ 0] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)

Tactic:
nth_rw 2 [← hM]
-- 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + succ 0] x)

Tactic:
H _ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self
-- 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + succ 0] x)

Tactic:
exact H _ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
neg : Cycle.Chain r Cycle.nil ↔ ∀ n < 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_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_notMem_periodicPts hx]

Premises used: Function.periodicOrbit_eq_nil_of_not_periodic_pt, Function.minimalPeriod_eq_zero_of_notMem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ n < 0, r (f^[n] x) (f^[n + 1] x)

Tactic:
simp
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
rw : (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [periodicOrbit_chain r]

Premises used: Function.periodicOrbit_chain
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
⟨fun H n => ?_, fun H n _ => H n⟩

Premises used: Iff.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
refine : ∀ (H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) (n : ℕ), r (f^[n] x) (f^[n + 1] x)
⊢ (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
refine ⟨fun H n => ?_, fun H n _ => H n⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
rw : r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
    ← iterate_succ_apply, minimalPeriod_apply hx]

Premises used: Function.iterate_mod_minimalPeriod_eq, Function.iterate_succ_apply, Function.minimalPeriod_apply
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)

Tactic:
H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))

Premises used: Function.minimalPeriod_pos_of_mem_periodicPts, Nat.mod_lt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)

Tactic:
exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))

Premises used: Function.minimalPeriod_pos_of_mem_periodicPts, Nat.mod_lt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ IsFixedPt (Prod.map f g) x ↔ IsFixedPt f x.1 ∧ IsFixedPt g x.2

Tactic:
Prod.ext_iff

Premises used: Prod.ext_iff, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
a : α
b : β
ha : IsFixedPt f a
hb : IsFixedPt g b
⊢ IsFixedPt (Prod.map f g) (a, b)

Tactic:
(isFixedPt_prodMap _).mpr ⟨ha, hb⟩

Premises used: Iff.mpr, And.intro, Function.isFixedPt_prodMap
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
x : α × β
⊢ IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.1 ∧ IsPeriodicPt g n x.2

Tactic:
simp [IsPeriodicPt]

Premises used: Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
a : α
b : β
n : ℕ
ha : IsPeriodicPt f n a
hb : IsPeriodicPt g n b
⊢ IsPeriodicPt (Prod.map f g) n (a, b)

Tactic:
(isPeriodicPt_prodMap _).mpr ⟨ha, hb⟩

Premises used: Iff.mpr, Function.isPeriodicPt_prodMap, And.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
⊢ IsFixedPt (Pi.map (α := α) (β := α) f) x ↔ ∀ (i : ι), IsFixedPt (f i) (x i)

Tactic:
funext_iff

Premises used: funext_iff, Pi.map, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
h : ∀ (i : ι), IsFixedPt (f i) (x i)
⊢ IsFixedPt (Pi.map (α := α) (β := α) f) x

Tactic:
isFixedPt_piMap.mpr h

Premises used: Iff.mpr, Function.isFixedPt_piMap
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
n : ℕ
⊢ IsPeriodicPt (Pi.map (α := α) (β := α) f) n x ↔ ∀ (i : ι), IsPeriodicPt (f i) n (x i)

Tactic:
simp [IsPeriodicPt]

Premises used: Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
n : ℕ
h : ∀ (i : ι), IsPeriodicPt (f i) n (x i)
⊢ IsPeriodicPt (Pi.map (α := α) (β := α) f) n x

Tactic:
isPeriodicPt_piMap.mpr h

Premises used: Iff.mpr, Function.isPeriodicPt_piMap
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ period m a = minimalPeriod (fun (x : α) ↦ m • x) a

Tactic:
rfl

Premises used: MulAction.period, rfl
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
rw : m ^ minimalPeriod (fun (x : α) ↦ m • x) a • a = a
rw₁ : (fun (x : α) ↦ m • x)^[minimalPeriod (fun (x : α) ↦ m • x) a] a = a
rw₂ rw₃ : a = a
⊢ m ^ period m a • a = a

Tactic:
rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]

Premises used: Function.iterate_minimalPeriod, MulAction.period_eq_minimalPeriod, smul_iterate_apply
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
rw : IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ (fun (x : α) ↦ m • x)^[n] a = a
rw₁ : IsFixedPt (fun (x : α) ↦ m • x)^[n] a ↔ (fun (x : α) ↦ m • x)^[n] a = a
rw₂ rw₃ : (fun (x : α) ↦ m • x)^[n] a = a ↔ (fun (x : α) ↦ m • x)^[n] a = a
⊢ IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ m ^ n • a = a

Tactic:
rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]

Premises used: Function.IsPeriodicPt, Function.IsFixedPt, smul_iterate_apply
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
rw : m ^ n • a = a ↔ minimalPeriod (fun (x : α) ↦ m • x) a ∣ n
rw₁ : m ^ n • a = a ↔ IsPeriodicPt (fun (x : α) ↦ m • x) n a
rw₂ rw₃ : m ^ n • a = a ↔ m ^ n • a = a
⊢ m ^ n • a = a ↔ period m a ∣ n

Tactic:
rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]

Premises used: MulAction.isPeriodicPt_smul_iff, MulAction.period_eq_minimalPeriod, Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : g ^ n • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)
rw₁ : g ^ n • a = a ↔ period g a ∣ n
rw₂ rw₃ : period g a ∣ n ↔ period g a ∣ n
⊢ HPow.hPow (β := ℤ) g (↑n : ℤ) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)

Tactic:
rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]

Premises used: zpow_natCast, MulAction.pow_smul_eq_iff_period_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₁ : (g ^ (n + 1))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₂ : a = g ^ (n + 1) • a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₃ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₄ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑(n + 1) : ℤ)
rw₅ : g ^ (n + 1) • a = a ↔ period g a ∣ n + 1
rw₆ rw₇ : period g a ∣ n + 1 ↔ period g a ∣ n + 1
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))

Tactic:
rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]

Premises used: zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, MulAction.pow_smul_eq_iff_period_dvd, zpow_neg, Int.natCast_dvd_natCast
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
⊢ g ^ j • a = a ↔ (↑(period g a) : ℤ) ∣ j

Tactic:
match j with
  | (n : ℕ) => rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]
  | -(n + 1 : ℕ) =>
    rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
rw : m ^ (n % period m a) • a
| m ^ n • a

Tactic:
rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Premises used: Iff.mpr, pow_add, Nat.mod_add_div, MulAction.pow_smul_eq_iff_period_dvd, dvd_mul_right, MulAction.period, SemigroupAction.mul_smul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
conv_rhs : m ^ (n % period m a) • a = m ^ n • a
conv_rhs₁ : m ^ (n % period m a) • a = m ^ (n % period m a) • a
⊢ m ^ (n % period m a) • a = m ^ n • a

Tactic:
conv_rhs => rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Premises used: Iff.mpr, pow_add, Nat.mod_add_div, MulAction.pow_smul_eq_iff_period_dvd, dvd_mul_right, MulAction.period, SemigroupAction.mul_smul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
rw : g ^ (j % (↑(period g a) : ℤ)) • a
| g ^ j • a

Tactic:
rw [← Int.emod_add_mul_ediv j (period g a), zpow_add, mul_smul,
    zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Premises used: Iff.mpr, zpow_add, MulAction.zpow_smul_eq_iff_period_dvd, Nat.cast, Int.emod_add_mul_ediv, dvd_mul_right, MulAction.period, SemigroupAction.mul_smul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
conv_rhs : g ^ (j % (↑(period g a) : ℤ)) • a = g ^ j • a
conv_rhs₁ : g ^ (j % (↑(period g a) : ℤ)) • a = g ^ (j % (↑(period g a) : ℤ)) • a
⊢ g ^ (j % (↑(period g a) : ℤ)) • a = g ^ j • a

Tactic:
conv_rhs => rw [← Int.emod_add_mul_ediv j (period g a), zpow_add, mul_smul,
    zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Premises used: Iff.mpr, zpow_add, MulAction.zpow_smul_eq_iff_period_dvd, Nat.cast, Int.emod_add_mul_ediv, dvd_mul_right, MulAction.period, SemigroupAction.mul_smul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
rw : m ^ ((n + period m a) % period m a) • a = m ^ n • a
rw₁ : m ^ (n % period m a) • a = m ^ n • a
rw₂ rw₃ : m ^ n • a = m ^ n • a
⊢ m ^ (n + period m a) • a = m ^ n • a

Tactic:
rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]

Premises used: Nat.add_mod_right, MulAction.pow_mod_period_smul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
rw : m ^ ((period m a + n) % period m a) • a = m ^ n • a
rw₁ : m ^ (n % period m a) • a = m ^ n • a
rw₂ rw₃ : m ^ n • a = m ^ n • a
⊢ m ^ (period m a + n) • a = m ^ n • a

Tactic:
rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]

Premises used: MulAction.pow_mod_period_smul, Nat.add_mod_left
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
rw : g ^ ((i + (↑(period g a) : ℤ)) % (↑(period g a) : ℤ)) • a = g ^ i • a
rw₁ : g ^ (i % (↑(period g a) : ℤ)) • a = g ^ i • a
rw₂ rw₃ : g ^ i • a = g ^ i • a
⊢ g ^ (i + (↑(period g a) : ℤ)) • a = g ^ i • a

Tactic:
rw [← zpow_mod_period_smul, Int.add_emod_right, zpow_mod_period_smul]

Premises used: Int.add_emod_right, MulAction.zpow_mod_period_smul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
rw : g ^ (((↑(period g a) : ℤ) + i) % (↑(period g a) : ℤ)) • a = g ^ i • a
rw₁ : g ^ (i % (↑(period g a) : ℤ)) • a = g ^ i • a
rw₂ rw₃ : g ^ i • a = g ^ i • a
⊢ g ^ ((↑(period g a) : ℤ) + i) • a = g ^ i • a

Tactic:
rw [← zpow_mod_period_smul, Int.add_emod_left, zpow_mod_period_smul]

Premises used: MulAction.zpow_mod_period_smul, Int.add_emod_left
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℕ
rw : a ^ n • b = b ↔ period a b ∣ n
rw₁ rw₂ : period a b ∣ n ↔ period a b ∣ n
⊢ a ^ n • b = b ↔ minimalPeriod (fun (x : α) ↦ a • x) b ∣ n

Tactic:
rw [← period_eq_minimalPeriod, pow_smul_eq_iff_period_dvd]

Premises used: MulAction.pow_smul_eq_iff_period_dvd, MulAction.period_eq_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℤ
rw : a ^ n • b = b ↔ (↑(period a b) : ℤ) ∣ n
rw₁ rw₂ : (↑(period a b) : ℤ) ∣ n ↔ (↑(period a b) : ℤ) ∣ n
⊢ a ^ n • b = b ↔ (↑(minimalPeriod (fun (x : α) ↦ a • x) b) : ℤ) ∣ n

Tactic:
rw [← period_eq_minimalPeriod, zpow_smul_eq_iff_period_dvd]

Premises used: MulAction.zpow_smul_eq_iff_period_dvd, MulAction.period_eq_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℕ
rw : a ^ (n % period a b) • b = a ^ n • b
rw₁ rw₂ : a ^ n • b = a ^ n • b
⊢ a ^ (n % minimalPeriod (fun (x : α) ↦ a • x) b) • b = a ^ n • b

Tactic:
rw [← period_eq_minimalPeriod, pow_mod_period_smul]

Premises used: MulAction.pow_mod_period_smul, MulAction.period_eq_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℤ
rw : a ^ (n % (↑(period a b) : ℤ)) • b = a ^ n • b
rw₁ rw₂ : a ^ n • b = a ^ n • b
⊢ a ^ (n % (↑(minimalPeriod (fun (x : α) ↦ a • x) b) : ℤ)) • b = a ^ n • b

Tactic:
rw [← period_eq_minimalPeriod, zpow_mod_period_smul]

Premises used: MulAction.zpow_mod_period_smul, MulAction.period_eq_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (n : ℕ+) ↦ ptsOfPeriod f (↑n : ℕ)

Tactic:
fun m n => ⟨m * n, fun _ hx => hx.mul_const n, fun _ hx => hx.const_mul m⟩

Premises used: PNat.val, HMul.hMul, Directed, Function.IsPeriodicPt.mul_const, Function.IsPeriodicPt.const_mul, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
⊢ BijOn f (periodicPts f) (periodicPts f)

Tactic:
iUnion_pnat_ptsOfPeriod f ▸
    bijOn_iUnion_of_directed (directed_ptsOfPeriod_pnat f) fun i => bijOn_ptsOfPeriod f i.pos

Premises used: Function.directed_ptsOfPeriod_pnat, Function.iUnion_pnat_ptsOfPeriod, Function.bijOn_ptsOfPeriod, Eq.rec, PNat.pos, Set.bijOn_iUnion_of_directed
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
rw : minimalPeriod f x = p → ¬minimalPeriod f x = 1
⊢ minimalPeriod f x = p ↔ IsPeriodicPt f p x ∧ ¬IsFixedPt f x

Tactic:
rw [Function.isPeriodicPt_iff_minimalPeriod_dvd, Nat.dvd_prime hp.out,
    ← minimalPeriod_eq_one_iff_isFixedPt.not, or_and_right, and_not_self_iff, false_or,
    iff_self_and]

Premises used: Function.minimalPeriod_eq_one_iff_isFixedPt, and_not_self_iff, iff_self_and, Iff.not, Nat.dvd_prime, false_or, Function.isPeriodicPt_iff_minimalPeriod_dvd, or_and_right, Fact.out
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p → ¬minimalPeriod f x = 1

Tactic:
fun h ↦ ne_of_eq_of_ne h hp.out.ne_one

Premises used: ne_of_eq_of_ne, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p → ¬minimalPeriod f x = 1

Tactic:
exact fun h ↦ ne_of_eq_of_ne h hp.out.ne_one

Premises used: ne_of_eq_of_ne, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
⊢ Eq (α := ℕ)
    (if h : ∃ n > 0, IsPeriodicPt f n x then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0)
    (if h : ∃ n > 0, IsPeriodicPt f n x then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0)

Tactic:
grind
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
hper : IsPeriodicPt f p x
hfix : ¬IsFixedPt f x
⊢ minimalPeriod f x = p

Tactic:
minimalPeriod_eq_prime_iff.mpr ⟨hper, hfix⟩

Premises used: Iff.mpr, Function.minimalPeriod_eq_prime_iff, And.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
h₁ : ¬minimalPeriod f x ∣ p ^ k
h₂ : minimalPeriod f x ∣ p ^ (k + 1)
⊢ minimalPeriod f x = p ^ (k + 1)

Tactic:
apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out

Premises used: Nat.eq_prime_pow_of_dvd_least_prime_pow, Fact.out
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
h₁ h₂ h₃ h₄ : ¬IsPeriodicPt f (p ^ k) x
⊢ ¬minimalPeriod f x ∣ p ^ k

Tactic:
rwa [← isPeriodicPt_iff_minimalPeriod_dvd]

Premises used: Function.isPeriodicPt_iff_minimalPeriod_dvd