awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (m * n) x

Tactic:
simp only [IsPeriodicPt, iterate_mul, hm.isFixedPt.iterate n]

Premises used: Function.IsPeriodicPt.isFixedPt, Function.IsPeriodicPt, Function.IsFixedPt.iterate, Function.iterate_mul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (n * m) x

Tactic:
simp only [mul_comm n, hm.mul_const n]

Premises used: Function.IsPeriodicPt.mul_const, mul_comm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
hn : m ∣ n
⊢ IsPeriodicPt f n x

Tactic:
let ⟨k, hk⟩ := hn
  hk.symm ▸ hm.mul_const k

Premises used: Eq.rec, Function.IsPeriodicPt, Function.IsPeriodicPt.mul_const, Eq.symm, _private.0.Function.IsPeriodicPt.trans_dvd.match_1
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
rw : IsFixedPt f^[n]^[m] x
⊢ IsPeriodicPt f^[m] n x

Tactic:
rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]

Premises used: Function.IsPeriodicPt, Function.iterate_mul, mul_comm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x

Tactic:
hf.isFixedPt.iterate m

Premises used: Function.IsPeriodicPt.isFixedPt, Function.IsFixedPt.iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x

Tactic:
exact hf.isFixedPt.iterate m

Premises used: Function.IsPeriodicPt.isFixedPt, Function.IsFixedPt.iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
rw : IsFixedPt (f^[n] ∘ g^[n]) x
⊢ IsPeriodicPt (f ∘ g) n x

Tactic:
rw [IsPeriodicPt, hco.comp_iterate]

Premises used: Function.IsPeriodicPt, Function.Commute.comp_iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x

Tactic:
IsFixedPt.comp hf hg

Premises used: Function.IsFixedPt.comp
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x

Tactic:
exact IsFixedPt.comp hf hg

Premises used: Function.IsFixedPt.comp
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f m x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt (f ∘ g) (m.lcm n) x

Tactic:
(hf.trans_dvd <| Nat.dvd_lcm_left _ _).comp hco (hg.trans_dvd <| Nat.dvd_lcm_right _ _)

Premises used: Function.IsPeriodicPt.trans_dvd, Nat.dvd_lcm_left, Function.IsPeriodicPt.comp, Nat.dvd_lcm_right
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x

Tactic:
rw [IsPeriodicPt, hco.comp_iterate] at hfg

Premises used: Function.IsPeriodicPt, Function.Commute.comp_iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
hfg₁ : IsFixedPt (f^[n] ∘ g^[n]) x
⊢ IsPeriodicPt g n x

Tactic:
rw [IsPeriodicPt, hco.comp_iterate] at hfg

Premises used: Function.IsPeriodicPt, Function.Commute.comp_iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
hfg.left_of_comp hg

Premises used: Function.IsFixedPt.left_of_comp, Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
exact hfg.left_of_comp hg

Premises used: Function.IsFixedPt.left_of_comp
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
rw : f^[m % n] x
| f^[m] x

Tactic:
rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

Premises used: Function.iterate_add_apply, Nat.mod_add_div, Function.IsPeriodicPt.mul_const, Function.IsFixedPt.eq
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
conv_rhs : f^[m % n] x = f^[m] x
conv_rhs₁ : f^[m % n] x = f^[m % n] x
⊢ f^[m % n] x = f^[m] x

Tactic:
conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

Premises used: Function.iterate_add_apply, Nat.mod_add_div, Function.IsPeriodicPt.mul_const, Function.IsFixedPt.eq
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m % n) x

Tactic:
(hn.iterate_mod_apply m).trans hm

Premises used: Function.IsPeriodicPt.iterate_mod_apply, Function.IsPeriodicPt, Function.IsFixedPt, Eq.trans
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
revert : ∀ (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x), IsPeriodicPt f (m.gcd n) x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
revert hm hn
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
⊢ ∀ (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x), IsPeriodicPt f (m.gcd n) x

Tactic:
Nat.gcd.induction m n (fun n _ hn => ?_) fun m n _ ih hm hn => ?_

Premises used: Nat.gcd.induction
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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
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
⊢ ∀ (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 => ?_
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n_1 n : ℕ
h : IsPeriodicPt f 0 x
hn refine_1 refine_1₁ refine_1₂ refine_1₃ : IsPeriodicPt f n x
⊢ IsPeriodicPt f (Nat.gcd 0 n) x

Tactic:
rwa [Nat.gcd_zero_left]

Premises used: Nat.gcd_zero_left
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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
refine_2 : IsPeriodicPt f ((n % m).gcd m) x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
rw [Nat.gcd_rec]

Premises used: Nat.gcd_rec
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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 ((n % m).gcd m) x

Tactic:
ih (hn.mod hm) hm

Premises used: Function.IsPeriodicPt.mod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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 ((n % m).gcd m) x

Tactic:
exact ih (hn.mod hm) hm

Premises used: Function.IsPeriodicPt.mod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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)
rw₅ rw₆ : f^[n.pred] (f y) = f^[n.pred] (f y)
⊢ x = y

Tactic:
rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]

Premises used: Function.iterate_pred_comp_of_pos, Function.IsFixedPt.eq, Function.comp_apply
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x y : α
m n : ℕ
hx : IsPeriodicPt f m x
hy : IsPeriodicPt f n y
hm : 0 < m
hn : 0 < n
h : f x = f y
⊢ x = y

Tactic:
(hx.mul_const n).eq_of_apply_eq_same (hy.const_mul m) (Nat.mul_pos hm hn) h

Premises used: Nat.mul_pos, Function.IsPeriodicPt.mul_const, Function.IsPeriodicPt.const_mul, Function.IsPeriodicPt.eq_of_apply_eq_same
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ x ∈ ptsOfPeriod f n ↔ IsPeriodicPt f n x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.IsPeriodicPt, Function.ptsOfPeriod, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
g : α → β
h : Semiconj g fa fb
n : ℕ
⊢ MapsTo g (ptsOfPeriod fa n) (ptsOfPeriod fb n)

Tactic:
(h.iterate_right n).mapsTo_fixedPoints

Premises used: setOf, Function.fixedPoints, Function.Semiconj.mapsTo_fixedPoints, Function.IsPeriodicPt, Function.ptsOfPeriod, Function.Semiconj.iterate_right
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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
rw₂ rw₃ : x = x
⊢ f (f^[n.pred] x) = x

Tactic:
rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]

Premises used: Function.comp_iterate_pred_of_pos, Function.IsFixedPt.eq, Function.comp_apply
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ x ∈ periodicPts f

Tactic:
⟨n, hn, hx⟩

Premises used: Set.Mem, setOf, And.intro, Function.periodicPts, Exists.intro
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ x ∈ periodicPts f ↔ ∃ n > 0, IsPeriodicPt f n x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : x ∈ periodicPts f
⊢ ∃ n > 0, IsPeriodicPt f n x

Tactic:
rw [mem_periodicPts] at h

Premises used: Function.mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : ∃ n > 0, IsPeriodicPt f n x
rcases : ∀ n > 0, ∀ (h : IsPeriodicPt f n x), x ∈ range f
⊢ x ∈ range f

Tactic:
rcases h with ⟨n, _, h⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
h₁ : f (f^[n - 1] x) = x
⊢ x ∈ range f

Tactic:
use f^[n - 1] x

Premises used: HSub.hSub, Nat.iterate, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
h₁ : f^[1] (f^[n - 1] x) = x
⊢ f (f^[n - 1] x) = x

Tactic:
nth_rw 1 [← iterate_one f]

Premises used: Function.iterate_one
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
h₁ : f^[n] x = x
⊢ f^[1] (f^[n - 1] x) = x

Tactic:
rw [← iterate_add_apply, Nat.add_sub_cancel' (by lia)]

Premises used: Function.iterate_add_apply, Nat.add_sub_cancel'
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
⊢ f^[n] x = x

Tactic:
h

Premises used: Function.IsPeriodicPt, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
left : n > 0
h : IsPeriodicPt f n x
⊢ f^[n] x = x

Tactic:
exact h
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hx : x ∈ periodicPts f
hm : IsPeriodicPt f m (f^[n] x)
rcases : ∀ (r : ℕ) (hr : r > 0) (hr' : IsPeriodicPt f r x), IsPeriodicPt f m x
⊢ IsPeriodicPt f m x

Tactic:
rcases hx with ⟨r, hr, hr'⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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] (f^[(n / r + 1) * r - n] (f^[n] x)) = f^[(n / r + 1) * r - n] (f^[n] x)

Tactic:
(hm.apply_iterate ((n / r + 1) * r - n)).eq

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Function.IsFixedPt.eq, Function.IsPeriodicPt.apply_iterate, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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 h₁ : x = f^[(n / r + 1) * r - n] (f^[n] x)
⊢ f^[m] x = x

Tactic:
convert! (hm.apply_iterate ((n / r + 1) * r - n)).eq

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Function.IsFixedPt.eq, Function.IsPeriodicPt.apply_iterate, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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
h₃ h₄ : x = x
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)

Tactic:
rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]

Premises used: Function.iterate_add_apply, Function.IsFixedPt.eq, Function.iterate_mul, Nat.sub_add_cancel, Function.IsPeriodicPt.iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
suffices : n ≤ (n / r + 1) * r
⊢ IsPeriodicPt f m x

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]
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
rw : n ≤ n / r * r + r
⊢ n ≤ (n / r + 1) * r

Tactic:
rw [Nat.add_mul, one_mul]

Premises used: Nat.add_mul, one_mul
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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 * r + r

Tactic:
(Nat.lt_div_mul_add hr).le

Premises used: Nat.lt_div_mul_add, LT.lt.le
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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 * r + r

Tactic:
exact (Nat.lt_div_mul_add hr).le

Premises used: Nat.lt_div_mul_add, LT.lt.le
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), ⋃ (_ : n > 0), ptsOfPeriod f n) x ↔ x ∈ periodicPts f

Tactic:
simp [mem_periodicPts]

Premises used: Function.mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
⊢ ⋃ (n : ℕ+), ptsOfPeriod f (↑n : ℕ) = periodicPts f

Tactic:
iSup_subtype.trans <| bUnion_ptsOfPeriod f

Premises used: iSup_subtype, Function.bUnion_ptsOfPeriod, Set.iUnion, Eq.trans, PNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
g : α → β
h : Semiconj g fa fb
⊢ MapsTo g (periodicPts fa) (periodicPts fb)

Tactic:
fun _ ⟨n, hn, hx⟩ => ⟨n, hn, hx.map h⟩

Premises used: Membership.mem, Set.MapsTo, And.intro, Function.periodicPts, _private.0.Function.Semiconj.mapsTo_periodicPts.match_1, Exists.intro, Function.IsPeriodicPt.map
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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
neg : ∀ (hx : x ∉ periodicPts f), IsPeriodicPt f 0 x
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) h else 0) x

Tactic:
split_ifs with hx
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) hx) x

Tactic:
(Nat.find_spec hx).2

Premises used: And.right, Nat.find_spec
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) hx) x

Tactic:
exact (Nat.find_spec hx).2

Premises used: And.right, Nat.find_spec
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x

Tactic:
isPeriodicPt_zero f x

Premises used: Function.isPeriodicPt_zero
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x

Tactic:
exact isPeriodicPt_zero f x

Premises used: Function.isPeriodicPt_zero
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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
neg neg₁ : ∀ (hx : x ∉ periodicPts f), IsPeriodicPt f 0 x
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x

Premises used: Function.isPeriodicPt_zero, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ f^[minimalPeriod f x] x = x

Tactic:
isPeriodicPt_minimalPeriod f x

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
rw : f^[n] (f^[minimalPeriod f x] x) = f^[n] x
⊢ f^[n + minimalPeriod f x] x = f^[n] x

Tactic:
rw [iterate_add_apply]

Premises used: Function.iterate_add_apply
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
e_a : f^[minimalPeriod f x] x = x
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x

Tactic:
congr
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[minimalPeriod f x] x = x

Tactic:
isPeriodicPt_minimalPeriod f x

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[minimalPeriod f x] x = x

Tactic:
exact isPeriodicPt_minimalPeriod f x

Premises used: Function.isPeriodicPt_minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n % minimalPeriod f x] x = f^[n] x

Tactic:
(isPeriodicPt_minimalPeriod f x).iterate_mod_apply n

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.iterate_mod_apply
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x

Tactic:
simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]

Premises used: GT.gt.lt, dif_pos, And.left, Function.minimalPeriod, Nat.find_spec
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ 0 < minimalPeriod f x

Tactic:
classical
  simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]

Premises used: dif_pos, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ minimalPeriod f x = 0

Tactic:
simp only [minimalPeriod, dif_neg hx]

Premises used: dif_neg, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ 0 < minimalPeriod f x

Tactic:
minimalPeriod_pos_of_mem_periodicPts <| mk_mem_periodicPts hn hx

Premises used: Function.minimalPeriod_pos_of_mem_periodicPts, Function.mk_mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
h : x ∉ periodicPts f
⊢ ¬0 < minimalPeriod f x

Tactic:
simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff]

Premises used: lt_irrefl, dif_neg, not_false_iff, OfNat.ofNat, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
rw : minimalPeriod f x = 0 ↔ ¬0 < minimalPeriod f x
rw₁ : minimalPeriod f x = 0 ↔ minimalPeriod f x ≤ 0
rw₂ rw₃ : minimalPeriod f x = 0 ↔ minimalPeriod f x = 0
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Tactic:
rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]

Premises used: not_lt, Function.minimalPeriod_pos_iff_mem_periodicPts, nonpos_iff_eq_zero
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
rw : Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) ⋯ ≤ n
⊢ minimalPeriod f x ≤ n

Tactic:
rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]

Premises used: dif_pos, Function.mk_mem_periodicPts, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) ⋯ ≤ n

Tactic:
Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

Premises used: Nat.find_min', And.intro, Function.mk_mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) ⋯ ≤ n

Tactic:
exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

Premises used: Nat.find_min', And.intro, Function.mk_mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
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
rw₁ rw₂ rw₃ : Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt f n x) ⋯ ≤ n
⊢ minimalPeriod f x ≤ n

Tactic:
classical
  rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
  exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

Premises used: dif_pos, Function.mk_mem_periodicPts, Function.minimalPeriod
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
f₁ : IsPeriodicPt f (minimalPeriod f x) (f^[n] x)
f₂ : f^[n] x ∈ periodicPts f
⊢ minimalPeriod f (f^[n] x) = minimalPeriod f 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 _))

Premises used: Function.IsPeriodicPt.minimalPeriod_le, Function.isPeriodicPt_minimalPeriod, LE.le.antisymm, Function.minimalPeriod_pos_of_mem_periodicPts, Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)

Tactic:
(isPeriodicPt_minimalPeriod f x).apply_iterate n

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.apply_iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)

Tactic:
exact (isPeriodicPt_minimalPeriod f x).apply_iterate n

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.apply_iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
rcases : ∀ (m : ℕ) (hm : m > 0) (hx : IsPeriodicPt f m x), f^[n] x ∈ periodicPts f
⊢ f^[n] x ∈ periodicPts f

Tactic:
rcases hx with ⟨m, hm, hx⟩