awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
⊢ periodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f
have simp : minimalPeriod f x = 0 ↔ x ∉ periodicPts f
Tactic: simp only [periodicOrbit.eq_1, Cycle.coe_eq_nil, List.map_eq_nil_iff, List.range_eq_nil]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ y ∈ periodicOrbit f x ↔ ∃ (n : ℕ), f^[n] x = y
have simp : (∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ (n : ℕ), f^[n] x = y
Tactic: simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ (∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ (n : ℕ), f^[n] x = y
have mpr : (∃ (n : ℕ), f^[n] x = y) → ∃ a < minimalPeriod f x, f^[a] x = y
Tactic: use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ ∃ a < minimalPeriod f x, f^[a] x = f^[n] x
have right : f^[n % minimalPeriod f x] x = f^[n] x
Tactic: use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n % minimalPeriod f x] x = f^[n] x
have right : f^[n] x = f^[n] x
Tactic: rw [iterate_mod_minimalPeriod_eq]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
⊢ (periodicOrbit f x).Nodup
have rw : ∀ x_1 ∈ List.range (minimalPeriod f x), ∀ y ∈ List.range (minimalPeriod f x), f^[x_1] x = f^[y] x → x_1 = y
Tactic: rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on List.nodup_range]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
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
have rw : ∀ (hm : m < minimalPeriod f x) (n : ℕ) (hn : n < minimalPeriod f x) (hmn : f^[m] x = f^[n] x), m = n
Tactic: rw [List.mem_range] at hm hn
Cleared hypotheses: hm, n, hn, hmn
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m = n
have rwa : ∀ (hmn : m = n), m = n
Tactic: rwa [iterate_eq_iterate_iff_of_lt_minimalPeriod hm hn] at hmn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
have pos : ∀ (hx : x ∈ periodicPts f), Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Tactic: by_cases hx : x ∈ periodicPts f
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
pos : ∀ (hx : x ∈ periodicPts f), Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
have neg : ∀ (hx : x ∉ periodicPts f), Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Tactic: by_cases hx : x ∈ periodicPts f
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
have hx' : 0 < minimalPeriod f x
Tactic: have hx' := minimalPeriod_pos_of_mem_periodicPts hx
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
have hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
Tactic: have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
have pos : (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) ↔
  ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
Tactic: rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) ↔
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
have pos : (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) →
  ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
Tactic: refine ⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
pos :
  (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) →
    ∀ 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) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) ↔
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
have pos₁ : ∀ (H : ∀ 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)
Tactic: refine ⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
have pos : ∀ (hM' : n = minimalPeriod f x - succ 0), r (f^[n] x) (f^[n + 1] x)
Tactic: rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
pos : ∀ (hM' : n = minimalPeriod f x - succ 0), r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[n] x) (f^[n + 1] x)
have pos₁ : ∀ (hM' : n < minimalPeriod f x - succ 0), r (f^[n] x) (f^[n + 1] x)
Tactic: rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] 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)
have pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + 1] x)
Tactic: rwa [hM', hM, iterate_minimalPeriod]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + 1] x)
⊢ r (f^[n] x) (f^[n + 1] x)
have pos₁ : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
Tactic: rwa [hM', hM, iterate_minimalPeriod]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + 1] x)
pos₁ : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
⊢ r (f^[n] x) (f^[n + 1] x)
have pos₂ : r (f^[minimalPeriod f x - succ 0] x) x
Tactic: rwa [hM', hM, iterate_minimalPeriod]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < 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)
have pos : r (f^[minimalPeriod f x - succ 0] x) x
Tactic: rw [iterate_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) x
have pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
Tactic: nth_rw 3 [← @iterate_minimalPeriod α f x]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
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 < 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)
have pos : r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + succ 0] x)
Tactic: nth_rw 2 [← hM]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
have neg : Cycle.Chain r Cycle.nil ↔ ∀ n < 0, r (f^[n] x) (f^[n + 1] x)
Tactic: rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_notMem_periodicPts hx]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
have rw : (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
Tactic: rw [periodicOrbit_chain r]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
have refine : ∀ (H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) (n : ℕ), r (f^[n] x) (f^[n + 1] x)
Tactic: refine ⟨fun H n => ?_, fun H n _ => H n⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)
have rw : r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)
Tactic: rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
    ← iterate_succ_apply, minimalPeriod_apply hx]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
⊢ m ^ period m a • a = a
have rw : m ^ minimalPeriod (fun (x : α) ↦ m • x) a • a = a
Tactic: rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
rw : m ^ minimalPeriod (fun (x : α) ↦ m • x) a • a = a
⊢ m ^ period m a • a = a
have rw₁ : (fun (x : α) ↦ m • x)^[minimalPeriod (fun (x : α) ↦ m • x) a] a = a
Tactic: rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
rw : m ^ minimalPeriod (fun (x : α) ↦ m • x) a • a = a
rw₁ : (fun (x : α) ↦ m • x)^[minimalPeriod (fun (x : α) ↦ m • x) a] a = a
⊢ m ^ period m a • a = a
have rw₂ : a = a
Tactic: rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
⊢ IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ m ^ n • a = a
have rw : IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ (fun (x : α) ↦ m • x)^[n] a = a
Tactic: rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
rw : IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ (fun (x : α) ↦ m • x)^[n] a = a
⊢ IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ m ^ n • a = a
have rw₁ : IsFixedPt (fun (x : α) ↦ m • x)^[n] a ↔ (fun (x : α) ↦ m • x)^[n] a = a
Tactic: rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
m : M
a : α
n : ℕ
rw : IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ (fun (x : α) ↦ m • x)^[n] a = a
rw₁ : IsFixedPt (fun (x : α) ↦ m • x)^[n] a ↔ (fun (x : α) ↦ m • x)^[n] a = a
⊢ IsPeriodicPt (fun (x : α) ↦ m • x) n a ↔ m ^ n • a = a
have rw₂ : (fun (x : α) ↦ m • x)^[n] a = a ↔ (fun (x : α) ↦ m • x)^[n] a = a
Tactic: rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ period m a ∣ n
have rw : m ^ n • a = a ↔ minimalPeriod (fun (x : α) ↦ m • x) a ∣ n
Tactic: rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
rw : m ^ n • a = a ↔ minimalPeriod (fun (x : α) ↦ m • x) a ∣ n
⊢ m ^ n • a = a ↔ period m a ∣ n
have rw₁ : m ^ n • a = a ↔ IsPeriodicPt (fun (x : α) ↦ m • x) n a
Tactic: rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
rw : m ^ n • a = a ↔ minimalPeriod (fun (x : α) ↦ m • x) a ∣ n
rw₁ : m ^ n • a = a ↔ IsPeriodicPt (fun (x : α) ↦ m • x) n a
⊢ m ^ n • a = a ↔ period m a ∣ n
have rw₂ : m ^ n • a = a ↔ m ^ n • a = a
Tactic: rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ HPow.hPow (β := ℤ) g (↑n : ℤ) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)
have rw : g ^ n • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)
Tactic: rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : g ^ n • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)
⊢ HPow.hPow (β := ℤ) g (↑n : ℤ) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)
have rw₁ : g ^ n • a = a ↔ period g a ∣ n
Tactic: rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : g ^ n • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)
rw₁ : g ^ n • a = a ↔ period g a ∣ n
⊢ HPow.hPow (β := ℤ) g (↑n : ℤ) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑n : ℤ)
have rw₂ : period g a ∣ n ↔ period g a ∣ n
Tactic: rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
have rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
Tactic: rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
have rw₁ : (g ^ (n + 1))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
Tactic: rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₁ : (g ^ (n + 1))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
have rw₂ : a = g ^ (n + 1) • a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
Tactic: rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₁ : (g ^ (n + 1))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₂ : a = g ^ (n + 1) • a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
have rw₃ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
Tactic: rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₁ : (g ^ (n + 1))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₂ : a = g ^ (n + 1) • a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₃ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
have rw₄ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑(n + 1) : ℤ)
Tactic: rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₁ : (g ^ (n + 1))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₂ : a = g ^ (n + 1) • a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₃ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₄ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑(n + 1) : ℤ)
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
have rw₅ : g ^ (n + 1) • a = a ↔ period g a ∣ n + 1
Tactic: rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
rw : (HPow.hPow (β := ℤ) g (↑(n + 1) : ℤ))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₁ : (g ^ (n + 1))⁻¹ • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₂ : a = g ^ (n + 1) • a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₃ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
rw₄ : g ^ (n + 1) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (↑(n + 1) : ℤ)
rw₅ : g ^ (n + 1) • a = a ↔ period g a ∣ n + 1
⊢ HPow.hPow (β := ℤ) g (-(↑(n + 1) : ℤ)) • a = a ↔ Dvd.dvd (α := ℤ) (↑(period g a) : ℤ) (-(↑(n + 1) : ℤ))
have rw₆ : period g a ∣ n + 1 ↔ period g a ∣ n + 1
Tactic: rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
| m ^ n • a
have rw : m ^ (n % period m a) • a
Tactic: rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (n % period m a) • a = m ^ n • a
have conv_rhs : m ^ (n % period m a) • a = m ^ n • a
Tactic: conv_rhs => rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
M : Type u
inst : Monoid M
inst_1 : MulAction M α
n : ℕ
m : M
a : α
conv_rhs : m ^ (n % period m a) • a = m ^ n • a
⊢ m ^ (n % period m a) • a = m ^ n • a
have conv_rhs₁ : m ^ (n % period m a) • a = m ^ (n % period m a) • a
Tactic: conv_rhs => rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
j : ℤ
g : G
a : α
| g ^ j • a
have rw : g ^ (j % (↑(period g a) : ℤ)) • a
Tactic: rw [← Int.emod_add_mul_ediv j (period g a), zpow_add, mul_smul,
    zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]