case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod (f^[n]) x ∣ minimalPeriod f x / gcd (minimalPeriod f x) n

case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n ∣ minimalPeriod (f^[n]) x
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod (f^[n]) x = minimalPeriod f x / gcd (minimalPeriod f x) n
apply Nat.dvd_antisymm
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ IsPeriodicPt (f^[n]) (minimalPeriod f x / gcd (minimalPeriod f x) n) x
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod (f^[n]) x ∣ minimalPeriod f x / gcd (minimalPeriod f x) n
apply IsPeriodicPt.minimalPeriod_dvd
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ (f^[n / gcd (minimalPeriod f x) n]^[minimalPeriod f x]) x = x
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ IsPeriodicPt (f^[n]) (minimalPeriod f x / gcd (minimalPeriod f x) n) x
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]
no goals
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ (f^[n / gcd (minimalPeriod f x) n]^[minimalPeriod f x]) x = x
exact (isPeriodicPt_minimalPeriod f x).iterate _
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n ∣ minimalPeriod (f^[n]) x * (n / gcd (minimalPeriod f x) n)
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n ∣ minimalPeriod (f^[n]) x
apply coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n * gcd (minimalPeriod f x) n ∣
    minimalPeriod (f^[n]) x * (n / gcd (minimalPeriod f x) n) * gcd (minimalPeriod f x) n
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n ∣ minimalPeriod (f^[n]) x * (n / gcd (minimalPeriod f x) n)
apply Nat.dvd_of_mul_dvd_mul_right h
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x ∣ n * minimalPeriod (f^[n]) x
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x / gcd (minimalPeriod f x) n * gcd (minimalPeriod f x) n ∣
    minimalPeriod (f^[n]) x * (n / gcd (minimalPeriod f x) n) * gcd (minimalPeriod f x) n
rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
  mul_comm]
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ IsPeriodicPt f (n * minimalPeriod (f^[n]) x) x
case a
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x ∣ n * minimalPeriod (f^[n]) x
apply IsPeriodicPt.minimalPeriod_dvd
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ (f^[n]^[minimalPeriod (f^[n]) x]) x = x
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ IsPeriodicPt f (n * minimalPeriod (f^[n]) x) x
rw [IsPeriodicPt, IsFixedPt, iterate_mul]
no goals
case a.hx
α : Type u_1
β : Type ?u.28238
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ (f^[n]^[minimalPeriod (f^[n]) x]) x = x
exact isPeriodicPt_minimalPeriod _ _