-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_iterate_eq_div_gcd_aux (h : 0 < gcd (minimalPeriod f x) n) :
    minimalPeriod f^[n] x = minimalPeriod f x / Nat.gcd (minimalPeriod f x) n

Proof state:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n

Tactic:
apply IsPeriodicPt.minimalPeriod_dvd

Result:
case a.hx
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsPeriodicPt f^[n] (minimalPeriod f x / (minimalPeriod f x).gcd n) x

Proof state:
case a.hx
α : 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 _

Result:
no goals

Proof state:
case a.hx
α : 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 _ _

Result:
no goals

Proof state:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ 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]

Result:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f^[n] x = minimalPeriod f x / (minimalPeriod f x).gcd n

Tactic:
apply Nat.dvd_antisymm

Result:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n

case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x

Proof state:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x

Tactic:
apply IsPeriodicPt.minimalPeriod_dvd

Result:
case a.hx
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x

Proof state:
case a.hx
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ 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]

Result:
case a.hx
α : 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

Proof state:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (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)

Result:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n)

Proof state:
case a.hx
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x

Tactic:
rw [IsPeriodicPt, IsFixedPt, iterate_mul]

Result:
case a.hx
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x

Proof state:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (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

Result:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ 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