awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt (f ∘ g) n x
have rw : IsFixedPt (f^[n] ∘ g^[n]) x
Tactic: rw [IsPeriodicPt, hco.comp_iterate]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (hypothesis)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
have hfg₁ : IsFixedPt (f^[n] ∘ g^[n]) x
Tactic: rw [IsPeriodicPt, hco.comp_iterate] at hfg
Cleared hypotheses: hfg, hg
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m] x
have rw : f^[m % n] x
Tactic: rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
⊢ f^[m % n] x = f^[m] x
have conv_rhs : f^[m % n] x = f^[m] x
Tactic: conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
conv_rhs : f^[m % n] x = f^[m] x
⊢ f^[m % n] x = f^[m] x
have conv_rhs₁ : f^[m % n] x = f^[m % n] x
Tactic: conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
⊢ ∀ (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x), IsPeriodicPt f (m.gcd n) x
have refine_1 : ∀ (n : ℕ), IsPeriodicPt f 0 x → ∀ (hn : IsPeriodicPt f n x), IsPeriodicPt f (Nat.gcd 0 n) x
Tactic: refine Nat.gcd.induction m n (fun n _ hn => ?_) fun m n _ ih hm hn => ?_
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
refine_1 : ∀ (n : ℕ), IsPeriodicPt f 0 x → ∀ (hn : IsPeriodicPt f n x), IsPeriodicPt f (Nat.gcd 0 n) x
⊢ ∀ (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x), IsPeriodicPt f (m.gcd n) x
have refine_2 : ∀ (m n : ℕ),
  0 < m →
    ∀ (ih : ∀ (hm : IsPeriodicPt f (n % m) x) (hn : IsPeriodicPt f m x), IsPeriodicPt f ((n % m).gcd m) x)
      (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x), IsPeriodicPt f (m.gcd n) x
Tactic: refine Nat.gcd.induction m n (fun n _ hn => ?_) fun m n _ ih hm hn => ?_
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m_1 n_1 m n : ℕ
h : 0 < m
ih : ∀ (hm : IsPeriodicPt f (n % m) x) (hn : IsPeriodicPt f m x), IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x
have refine_2 : IsPeriodicPt f ((n % m).gcd m) x
Tactic: rw [Nat.gcd_rec]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
⊢ x = y
have rw : f^[n] x = y
Tactic: rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
rw : f^[n] x = y
⊢ x = y
have rw₁ : f^[n] x = f^[n] y
Tactic: rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
rw : f^[n] x = y
rw₁ : f^[n] x = f^[n] y
⊢ x = y
have rw₂ : (f^[n.pred] ∘ f) x = (f^[n.pred] ∘ f) y
Tactic: rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
rw : f^[n] x = y
rw₁ : f^[n] x = f^[n] y
rw₂ : (f^[n.pred] ∘ f) x = (f^[n.pred] ∘ f) y
⊢ x = y
have rw₃ : f^[n.pred] (f x) = (f^[n.pred] ∘ f) y
Tactic: rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
rw : f^[n] x = y
rw₁ : f^[n] x = f^[n] y
rw₂ : (f^[n.pred] ∘ f) x = (f^[n.pred] ∘ f) y
rw₃ : f^[n.pred] (f x) = (f^[n.pred] ∘ f) y
⊢ x = y
have rw₄ : f^[n.pred] (f x) = f^[n.pred] (f y)
Tactic: rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
rw : f^[n] x = y
rw₁ : f^[n] x = f^[n] y
rw₂ : (f^[n.pred] ∘ f) x = (f^[n.pred] ∘ f) y
rw₃ : f^[n.pred] (f x) = (f^[n.pred] ∘ f) y
rw₄ : f^[n.pred] (f x) = f^[n.pred] (f y)
⊢ x = y
have rw₅ : f^[n.pred] (f y) = f^[n.pred] (f y)
Tactic: rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f (f^[n.pred] x) = x
have rw : (f ∘ f^[n.pred]) x = x
Tactic: rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
rw : (f ∘ f^[n.pred]) x = x
⊢ f (f^[n.pred] x) = x
have rw₁ : f^[n] x = x
Tactic: rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
rw : (f ∘ f^[n.pred]) x = x
rw₁ : f^[n] x = x
⊢ f (f^[n.pred] x) = x
have rw₂ : x = x
Tactic: rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (hypothesis)
Goal:
α : Type u_1
f : α → α
x : α
h : x ∈ periodicPts f
⊢ x ∈ range f
have h₁ : ∃ n > 0, IsPeriodicPt f n x
Tactic: rw [mem_periodicPts] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
h : ∃ n > 0, IsPeriodicPt f n x
⊢ x ∈ range f
have rcases : ∀ n > 0, ∀ (h : IsPeriodicPt f n x), x ∈ range f
Tactic: rcases h with ⟨n, _, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
⊢ x ∈ range f
have h₁ : f (f^[n - 1] x) = x
Tactic: use f^[n - 1] x
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
⊢ f (f^[n - 1] x) = x
have h₁ : f^[1] (f^[n - 1] x) = x
Tactic: nth_rw 1 [← iterate_one f]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
⊢ f^[1] (f^[n - 1] x) = x
have h₁ : f^[n] x = x
Tactic: rw [← iterate_add_apply, Nat.add_sub_cancel' (by lia)]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hx : x ∈ periodicPts f
hm : IsPeriodicPt f m (f^[n] x)
⊢ IsPeriodicPt f m x
have rcases : ∀ (r : ℕ) (hr : r > 0) (hr' : IsPeriodicPt f r x), IsPeriodicPt f m x
Tactic: rcases hx with ⟨r, hr, hr'⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
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
have h : x = f^[(n / r + 1) * r - n] (f^[n] x)
Tactic: convert! (hm.apply_iterate ((n / r + 1) * r - n)).eq
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
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)
have h : x = f^[(n / r + 1) * r - n + n] x
Tactic: rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
h : x = f^[(n / r + 1) * r - n + n] x
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
have h₁ : x = f^[(n / r + 1) * r] x
Tactic: rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
h : x = f^[(n / r + 1) * r - n + n] x
h₁ : x = f^[(n / r + 1) * r] x
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
have h₂ : x = f^[n / r + 1]^[r] x
Tactic: rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
h : x = f^[(n / r + 1) * r - n + n] x
h₁ : x = f^[(n / r + 1) * r] x
h₂ : x = f^[n / r + 1]^[r] x
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
have h₃ : x = x
Tactic: rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x
have suffices : n ≤ (n / r + 1) * r
Tactic: suffices n ≤ (n / r + 1) * r by
    unfold IsPeriodicPt IsFixedPt
    convert! (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
      rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r
have rw : n ≤ n / r * r + r
Tactic: rw [Nat.add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) x
have pos : ∀ (hx : x ∈ periodicPts f), IsPeriodicPt f (Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) hx) x
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
pos : ∀ (hx : x ∈ periodicPts f), IsPeriodicPt f (Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) hx) x
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) x
have neg : ∀ (hx : x ∉ periodicPts f), IsPeriodicPt f 0 x
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x
have delta : IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) x
Tactic: classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
delta :
  IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) x
⊢ IsPeriodicPt f (minimalPeriod f x) x
have pos : ∀ (hx : x ∈ periodicPts f), IsPeriodicPt f (Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) hx) x
Tactic: classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
delta :
  IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) x
pos : ∀ (hx : x ∈ periodicPts f), IsPeriodicPt f (Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) hx) x
⊢ IsPeriodicPt f (minimalPeriod f x) x
have neg : ∀ (hx : x ∉ periodicPts f), IsPeriodicPt f 0 x
Tactic: classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x
have rw : f^[n] (f^[minimalPeriod f x] x) = f^[n] x
Tactic: rw [iterate_add_apply]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x
have e_a : f^[minimalPeriod f x] x = x
Tactic: congr
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f
have rw : minimalPeriod f x = 0 ↔ ¬0 < minimalPeriod f x
Tactic: rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
rw : minimalPeriod f x = 0 ↔ ¬0 < minimalPeriod f x
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f
have rw₁ : minimalPeriod f x = 0 ↔ minimalPeriod f x ≤ 0
Tactic: rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
rw : minimalPeriod f x = 0 ↔ ¬0 < minimalPeriod f x
rw₁ : minimalPeriod f x = 0 ↔ minimalPeriod f x ≤ 0
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f
have rw₂ : minimalPeriod f x = 0 ↔ minimalPeriod f x = 0
Tactic: rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n
have rw : Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) sorry ≤ n
Tactic: rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n
have rw : (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) ≤ n
Tactic: classical
  rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
  exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
rw : (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) ≤ n
⊢ minimalPeriod f x ≤ n
have rw₁ : Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) sorry ≤ n
Tactic: classical
  rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
  exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ minimalPeriod f (f^[n] x) = minimalPeriod f x
have f₁ : IsPeriodicPt f (minimalPeriod f x) (f^[n] x)
Tactic: 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 _))
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
f₁ : IsPeriodicPt f (minimalPeriod f x) (f^[n] x)
⊢ minimalPeriod f (f^[n] x) = minimalPeriod f x
have f₂ : f^[n] x ∈ periodicPts f
Tactic: 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 _))
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f
have rcases : ∀ (m : ℕ) (hm : m > 0) (hx : IsPeriodicPt f m x), f^[n] x ∈ periodicPts f
Tactic: rcases hx with ⟨m, hm, hx⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m ≤ n
have by_contra! : ∀ (hmn' : n < m), False
Tactic: by_contra! hmn'
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (hypothesis)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
⊢ False
have hmn₁ : 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
Cleared hypotheses: hmn, hmn'
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x
have refine_1 : ∀ (h : minimalPeriod f x = 1), IsFixedPt f x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
refine_1 : ∀ (h : minimalPeriod f x = 1), IsFixedPt f x
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x
have refine_2 : ∀ (h : IsFixedPt f x), minimalPeriod f x = 1
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f x
have refine_1 : IsFixedPt f^[1] x
Tactic: rw [← iterate_one f]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x
have refine_1 : IsPeriodicPt f (minimalPeriod f x) x
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → α
x : α
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y
have simp_rw : minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), minimalPeriod f x ∣ n ↔ minimalPeriod g y ∣ n
Tactic: simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ minimalPeriod (f ∘ g) x ∣ (minimalPeriod f x).lcm (minimalPeriod g x)
have rw : IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x
Tactic: rw [← isPeriodicPt_iff_minimalPeriod_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : 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
have a : minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
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
⊢ minimalPeriod f^[n] x = minimalPeriod f x / (minimalPeriod f x).gcd n
have a₁ : minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : 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
have a : IsPeriodicPt f^[n] (minimalPeriod f x / (minimalPeriod f x).gcd n) x
Tactic: apply IsPeriodicPt.minimalPeriod_dvd
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : 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
have a : f^[n / (minimalPeriod f x).gcd n]^[minimalPeriod f x] x = 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]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : 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
have a : minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n)
Tactic: apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : 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)
have 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
Tactic: apply Nat.dvd_of_mul_dvd_mul_right h
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : 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
have a : minimalPeriod f x ∣ n * minimalPeriod f^[n] x
Tactic: rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
      mul_comm]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x
have a : IsPeriodicPt f (n * minimalPeriod f^[n] x) x
Tactic: apply IsPeriodicPt.minimalPeriod_dvd
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x
have a : f^[n]^[minimalPeriod f^[n] x] x = x
Tactic: rw [IsPeriodicPt, IsFixedPt, iterate_mul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
⊢ (periodicOrbit f x).length = minimalPeriod f x
have rw : Cycle.length.{u_1} (α := α) (↑(List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) : Cycle α) =
  minimalPeriod f x
Tactic: rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
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
⊢ (periodicOrbit f x).length = minimalPeriod f x
have rw₁ : List.length.{u_1} (α := α) (List.map (fun (n : ℕ) ↦ f^[n] x) (List.range (minimalPeriod f x))) = minimalPeriod f x
Tactic: rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
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
⊢ (periodicOrbit f x).length = minimalPeriod f x
have rw₂ : (List.range (minimalPeriod f x)).length = minimalPeriod f x
Tactic: rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
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
⊢ (periodicOrbit f x).length = minimalPeriod f x
have rw₃ : minimalPeriod f x = minimalPeriod f x
Tactic: rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]