[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f (n + m) x
[PROOFSTEP]
rw [IsPeriodicPt, iterate_add]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x
[PROOFSTEP]
exact hn.comp hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
rw [IsPeriodicPt, iterate_add] at hn 
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
exact hn.left_of_comp hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
[PROOFSTEP]
rw [add_comm] at hn 
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
[PROOFSTEP]
exact hn.left_of_add hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m - n) x
[PROOFSTEP]
cases' le_total n m with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x
[PROOFSTEP]
refine' left_of_add _ hn
[GOAL]
case inl
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x
[PROOFSTEP]
rwa [tsub_add_cancel_of_le h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x
[PROOFSTEP]
apply isPeriodicPt_zero
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (m * n) x
[PROOFSTEP]
simp only [IsPeriodicPt, iterate_mul, hm.isFixedPt.iterate n]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (n * m) x
[PROOFSTEP]
simp only [mul_comm n, hm.mul_const n]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt f^[m] n x
[PROOFSTEP]
rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x
[PROOFSTEP]
exact hf.isFixedPt.iterate m
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt (f ∘ g) n x
[PROOFSTEP]
rw [IsPeriodicPt, hco.comp_iterate]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x
[PROOFSTEP]
exact IsFixedPt.comp hf hg
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
rw [IsPeriodicPt, hco.comp_iterate] at hfg 
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
[PROOFSTEP]
exact hfg.left_of_comp hg
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
⊢ f^[m % n] x = f^[m] x
[PROOFSTEP]
conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x
[PROOFSTEP]
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x
[PROOFSTEP]
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x
[PROOFSTEP]
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd m n) x
[PROOFSTEP]
revert hm hn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (Nat.gcd m n) x
[PROOFSTEP]
refine' Nat.gcd.induction m n (fun n _ hn => _) fun m n _ ih hm hn => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ n : ℕ
x✝ : IsPeriodicPt f 0 x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd 0 n) x
[PROOFSTEP]
rwa [Nat.gcd_zero_left]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd m n) x
[PROOFSTEP]
rw [Nat.gcd_rec]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f (Nat.gcd (n % m) m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd (n % m) m) x
[PROOFSTEP]
exact ih (hn.mod hm) hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
⊢ x = y
[PROOFSTEP]
rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f (f^[Nat.pred n] x) = x
[PROOFSTEP]
rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
hm : IsPeriodicPt f m (f^[n] x)
⊢ IsPeriodicPt f m x
[PROOFSTEP]
rcases hx with ⟨r, hr, hr'⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x
[PROOFSTEP]
suffices n ≤ (n / r + 1) * r by
  -- porting note: convert used to unfold IsPeriodicPt
  change _ = _
  convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
    rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ IsPeriodicPt f m x
[PROOFSTEP]
change _ = _
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ f^[m] x = x
[PROOFSTEP]
convert (hm.apply_iterate ((n / r + 1) * r - n)).eq
[GOAL]
case h.e'_2.h.e'_4
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
[PROOFSTEP]
rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
[PROOFSTEP]
rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r
[PROOFSTEP]
rw [add_mul, one_mul]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r
[PROOFSTEP]
exact (Nat.lt_div_mul_add hr).le
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
x : α
⊢ x ∈ ⋃ (n : ℕ) (_ : n > 0), ptsOfPeriod f n ↔ x ∈ periodicPts f
[PROOFSTEP]
simp [mem_periodicPts]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x
[PROOFSTEP]
delta minimalPeriod
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x
[PROOFSTEP]
exact (Nat.find_spec hx).2
[GOAL]
case neg
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ IsPeriodicPt f 0 x
[PROOFSTEP]
exact isPeriodicPt_zero f x
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x
[PROOFSTEP]
rw [iterate_add_apply]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ f^[minimalPeriod f x] x = x
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod f x
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x
[PROOFSTEP]
simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : ¬x ∈ periodicPts f
⊢ minimalPeriod f x = 0
[PROOFSTEP]
simp only [minimalPeriod, dif_neg hx]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : ¬x ∈ periodicPts f
⊢ ¬0 < minimalPeriod f x
[PROOFSTEP]
simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 0 ↔ ¬x ∈ periodicPts f
[PROOFSTEP]
rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n
[PROOFSTEP]
rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find (_ : x ∈ periodicPts f) ≤ n
[PROOFSTEP]
exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ minimalPeriod f (f^[n] x) = minimalPeriod f x
[PROOFSTEP]
apply
  (IsPeriodicPt.minimalPeriod_le (minimalPeriod_pos_of_mem_periodicPts hx) _).antisymm
    ((isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate hx (isPeriodicPt_minimalPeriod f _)).minimalPeriod_le
      (minimalPeriod_pos_of_mem_periodicPts _))
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod f x).apply_iterate n
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f
[PROOFSTEP]
rcases hx with ⟨m, hm, hx⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f
[PROOFSTEP]
exact ⟨m, hm, hx.apply_iterate n⟩
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m ≤ n
[PROOFSTEP]
by_contra' hmn'
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
⊢ False
[PROOFSTEP]
rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn 
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False
[PROOFSTEP]
exact
  ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
            (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
              (minimalPeriod_pos_iff_mem_periodicPts.1 ((zero_le m).trans_lt hm)) hmn)).trans
        (Nat.sub_le m n)).not_lt
    hm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt f x
[PROOFSTEP]
rw [← iterate_one f]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt f^[1] x
[PROOFSTEP]
refine' Function.IsPeriodicPt.isFixedPt _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x
[PROOFSTEP]
rw [← h]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod f x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : IsFixedPt f x
⊢ minimalPeriod f x = 1
[PROOFSTEP]
exact
  ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
    (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y✝ : α
m n : ℕ
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y
[PROOFSTEP]
simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x = p ^ (k + 1)
[PROOFSTEP]
apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out
[GOAL]
case h₁
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ ¬minimalPeriod f x ∣ p ^ k
[PROOFSTEP]
rwa [← isPeriodicPt_iff_minimalPeriod_dvd]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x ∣ p ^ (k + 1)
[PROOFSTEP]
rwa [← isPeriodicPt_iff_minimalPeriod_dvd]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
⊢ minimalPeriod (f ∘ g) x ∣ lcm (minimalPeriod f x) (minimalPeriod g x)
[PROOFSTEP]
rw [← isPeriodicPt_iff_minimalPeriod_dvd]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
⊢ IsPeriodicPt (f ∘ g) (lcm (minimalPeriod f x) (minimalPeriod g x)) x
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x
[PROOFSTEP]
apply h.minimalPeriod_of_comp_dvd_mul.antisymm
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
suffices :
  ∀ {f g : α → α},
    Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
this :
  ∀ {f g : α → α},
    Function.Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
exact hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
[GOAL]
case this
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Function.Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
intro f g h hco
[GOAL]
case this
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
[PROOFSTEP]
refine' hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h _ _).minimalPeriod_dvd
[GOAL]
case this.refine'_1
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod _ _).const_mul _
[GOAL]
case this.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod _ _).mul_const _
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply IsPeriodicPt.minimalPeriod_dvd
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
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]
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact (isPeriodicPt_minimalPeriod f x).iterate _
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
[GOAL]
case a
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
apply Nat.dvd_of_mul_dvd_mul_right h
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _), mul_comm]
[GOAL]
case a
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x
[PROOFSTEP]
apply IsPeriodicPt.minimalPeriod_dvd
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x
[PROOFSTEP]
rw [IsPeriodicPt, IsFixedPt, iterate_mul]
[GOAL]
case a.hx
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : 0 < gcd (minimalPeriod f x) n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod _ _
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ Cycle.length (periodicOrbit f x) = minimalPeriod f x
[PROOFSTEP]
rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ periodicOrbit f x = Cycle.nil ↔ ¬x ∈ periodicPts f
[PROOFSTEP]
simp [periodicOrbit]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 0 ↔ ¬x ∈ periodicPts f
[PROOFSTEP]
exact minimalPeriod_eq_zero_iff_nmem_periodicPts
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y
[PROOFSTEP]
simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ a, a < minimalPeriod f x ∧ f^[a] x = y) ↔ ∃ n, f^[n] x = y
[PROOFSTEP]
use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
⊢ (∃ n, f^[n] x = y) → ∃ a, a < minimalPeriod f x ∧ f^[a] x = y
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∃ a, a < minimalPeriod f x ∧ f^[a] x = f^[n] x
[PROOFSTEP]
use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)
[GOAL]
case right
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n % minimalPeriod f x] x = f^[n] x
[PROOFSTEP]
rw [iterate_mod_minimalPeriod_eq]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ Cycle.Nodup (periodicOrbit f x)
[PROOFSTEP]
rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on (List.nodup_range _)]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ List.range (minimalPeriod f x) → ∀ (y : ℕ), y ∈ List.range (minimalPeriod f x) → f^[x_1] x = f^[y] x → x_1 = y
[PROOFSTEP]
intro m hm n hn hmn
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : f^[m] x = f^[n] x
⊢ m = n
[PROOFSTEP]
rw [List.mem_range] at hm hn 
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m = n
[PROOFSTEP]
rwa [eq_iff_lt_minimalPeriod_of_iterate_eq hm hn] at hmn 
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n =
    List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))
[PROOFSTEP]
apply List.ext_nthLe _ fun m _ _ => _
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ List.length (List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n) =
    List.length (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))
[PROOFSTEP]
simp [minimalPeriod_apply_iterate hx]
[GOAL]
α : Type u_1
β : Type u_2
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∀ (m : ℕ) (x_1 : m < List.length (List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n))
    (x_2 : m < List.length (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x))))),
    List.nthLe (List.rotate (List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))) n) m x_1 =
      List.nthLe (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))) m x_2
[PROOFSTEP]
simp [List.nthLe_rotate, iterate_add_apply]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
by_cases hx : x ∈ periodicPts f
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
have hx' := minimalPeriod_pos_of_mem_periodicPts hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
[GOAL]
case pos
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
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 : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)) ↔
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
refine' ⟨_, fun H => ⟨_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
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 : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)) →
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rintro ⟨hr, H⟩ n hn
[GOAL]
case pos.refine'_1.intro
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
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 : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
cases' eq_or_lt_of_le (lt_succ_iff.1 hn) with hM' hM'
[GOAL]
case pos.refine'_1.intro.inl
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
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 : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] 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)
[PROOFSTEP]
rwa [hM', hM, iterate_minimalPeriod]
[GOAL]
case pos.refine'_1.intro.inr
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
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 : ℕ), m < minimalPeriod f x - succ 0 → r (f^[m] x) (f^[succ m] 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)
[PROOFSTEP]
exact H _ hM'
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
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 : ℕ), 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)
[PROOFSTEP]
rw [iterate_zero_apply]
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
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 : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) x
[PROOFSTEP]
nth_rw 3 [← @iterate_minimalPeriod α f x]
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
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 : ℕ), 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] x)
[PROOFSTEP]
nth_rw 2 [← hM]
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
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 : ℕ), 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)
[PROOFSTEP]
exact H _ (Nat.lt_succ_self _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_nmem_periodicPts hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ (n : ℕ), n < 0 → r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [periodicOrbit_chain r]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
refine' ⟨fun H n => _, fun H n _ => H n⟩
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)
[PROOFSTEP]
rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n), ← iterate_succ_apply,
  minimalPeriod_apply hx]
[GOAL]
α : Type u_1
β : Type u_2
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[succ (n % minimalPeriod f x)] x)
[PROOFSTEP]
exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))
[GOAL]
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n✝ : ℕ
f : α → α
g : β → β
n : ℕ
⊢ (Prod.map f g)^[n] = Prod.map f^[n] g^[n]
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
⊢ (Prod.map f g)^[Nat.zero] = Prod.map f^[Nat.zero] g^[Nat.zero]
[PROOFSTEP]
simp [*, Prod.map_comp_map]
[GOAL]
case succ
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
n✝ : ℕ
n_ih✝ : (Prod.map f g)^[n✝] = Prod.map f^[n✝] g^[n✝]
⊢ (Prod.map f g)^[Nat.succ n✝] = Prod.map f^[Nat.succ n✝] g^[Nat.succ n✝]
[PROOFSTEP]
simp [*, Prod.map_comp_map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x✝ : α × β
a : α
b : β
m n : ℕ
x : α × β
⊢ IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.fst ∧ IsPeriodicPt g n x.snd
[PROOFSTEP]
simp [IsPeriodicPt]
[GOAL]
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x✝ : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
x : α × β
⊢ ∀ (c : ℕ), minimalPeriod (Prod.map f g) x ∣ c ↔ Nat.lcm (minimalPeriod f x.fst) (minimalPeriod g x.snd) ∣ c
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
f✝ : α → α
g✝ : β → β
x : α × β
a : α
b : β
m n : ℕ
f : α → α
g : β → β
fst✝ : α
snd✝ : β
⊢ ∀ (c : ℕ),
    minimalPeriod (Prod.map f g) (fst✝, snd✝) ∣ c ↔
      Nat.lcm (minimalPeriod f (fst✝, snd✝).fst) (minimalPeriod g (fst✝, snd✝).snd) ∣ c
[PROOFSTEP]
simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod f x.fst ∣ minimalPeriod (Prod.map f g) x
[PROOFSTEP]
rw [minimalPeriod_prod_map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod f x.fst ∣ Nat.lcm (minimalPeriod f x.fst) (minimalPeriod g x.snd)
[PROOFSTEP]
exact Nat.dvd_lcm_left _ _
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod g x.snd ∣ minimalPeriod (Prod.map f g) x
[PROOFSTEP]
rw [minimalPeriod_prod_map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
a : α
b : β
m n : ℕ
⊢ minimalPeriod g x.snd ∣ Nat.lcm (minimalPeriod f x.fst) (minimalPeriod g x.snd)
[PROOFSTEP]
exact Nat.dvd_lcm_right _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod ((fun x x_1 => x • x_1) a) b ∣ n
[PROOFSTEP]
rw [← isPeriodicPt_iff_minimalPeriod_dvd, IsPeriodicPt, IsFixedPt, smul_iterate]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
⊢ a ^ n • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.ofNat a✝
[PROOFSTEP]
rw [Int.ofNat_eq_coe, zpow_ofNat, Int.coe_nat_dvd, pow_smul_eq_iff_minimalPeriod_dvd]
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.negSucc a✝
[PROOFSTEP]
rw [Int.negSucc_coe, zpow_neg, zpow_ofNat, inv_smul_eq_iff, eq_comm, dvd_neg, Int.coe_nat_dvd,
  pow_smul_eq_iff_minimalPeriod_dvd]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
⊢ a ^ (n % minimalPeriod ((fun x x_1 => x • x_1) a) b) • b = a ^ n • b
[PROOFSTEP]
conv_rhs =>
  rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
    pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
| a ^ n • b
[PROOFSTEP]
rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
    pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
| a ^ n • b
[PROOFSTEP]
rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
    pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
| a ^ n • b
[PROOFSTEP]
rw [← Nat.mod_add_div n (minimalPeriod ((· • ·) a) b), pow_add, mul_smul,
  pow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
⊢ a ^ (n % ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b)) • b = a ^ n • b
[PROOFSTEP]
conv_rhs =>
  rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
    zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
| a ^ n • b
[PROOFSTEP]
rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
    zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
| a ^ n • b
[PROOFSTEP]
rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
    zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
| a ^ n • b
[PROOFSTEP]
rw [← Int.emod_add_ediv n (minimalPeriod ((a • ·)) b), zpow_add, mul_smul,
  zpow_smul_eq_iff_minimalPeriod_dvd.mpr (dvd_mul_right _ _)]
