awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 % (↑(period g a) : ℤ)) • a = g ^ j • a
have conv_rhs : g ^ (j % (↑(period g a) : ℤ)) • a = g ^ j • a
Tactic: conv_rhs => rw [← Int.emod_add_mul_ediv j (period g a), zpow_add, mul_smul,
    zpow_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 : α
conv_rhs : g ^ (j % (↑(period g a) : ℤ)) • a = g ^ j • a
⊢ g ^ (j % (↑(period g a) : ℤ)) • a = g ^ j • a
have conv_rhs₁ : g ^ (j % (↑(period g a) : ℤ)) • a = g ^ (j % (↑(period g a) : ℤ)) • a
Tactic: conv_rhs => rw [← Int.emod_add_mul_ediv j (period g a), zpow_add, mul_smul,
    zpow_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 rw : m ^ ((n + period m a) % period m a) • a = m ^ n • a
Tactic: rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]
-- 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 + period m a) % period m a) • a = m ^ n • a
⊢ m ^ (n + period m a) • a = m ^ n • a
have rw₁ : m ^ (n % period m a) • a = m ^ n • a
Tactic: rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]
-- 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 + period m a) % period m a) • a = m ^ n • a
rw₁ : m ^ (n % period m a) • a = m ^ n • a
⊢ m ^ (n + period m a) • a = m ^ n • a
have rw₂ : m ^ n • a = m ^ n • a
Tactic: rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]
-- 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 ^ (period m a + n) • a = m ^ n • a
have rw : m ^ ((period m a + n) % period m a) • a = m ^ n • a
Tactic: rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]
-- 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 ^ ((period m a + n) % period m a) • a = m ^ n • a
⊢ m ^ (period m a + n) • a = m ^ n • a
have rw₁ : m ^ (n % period m a) • a = m ^ n • a
Tactic: rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]
-- 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 ^ ((period m a + n) % period m a) • a = m ^ n • a
rw₁ : m ^ (n % period m a) • a = m ^ n • a
⊢ m ^ (period m a + n) • a = m ^ n • a
have rw₂ : m ^ n • a = m ^ n • a
Tactic: rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ (i + (↑(period g a) : ℤ)) • a = g ^ i • a
have rw : g ^ ((i + (↑(period g a) : ℤ)) % (↑(period g a) : ℤ)) • a = g ^ i • a
Tactic: rw [← zpow_mod_period_smul, Int.add_emod_right, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
rw : g ^ ((i + (↑(period g a) : ℤ)) % (↑(period g a) : ℤ)) • a = g ^ i • a
⊢ g ^ (i + (↑(period g a) : ℤ)) • a = g ^ i • a
have rw₁ : g ^ (i % (↑(period g a) : ℤ)) • a = g ^ i • a
Tactic: rw [← zpow_mod_period_smul, Int.add_emod_right, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
rw : g ^ ((i + (↑(period g a) : ℤ)) % (↑(period g a) : ℤ)) • a = g ^ i • a
rw₁ : g ^ (i % (↑(period g a) : ℤ)) • a = g ^ i • a
⊢ g ^ (i + (↑(period g a) : ℤ)) • a = g ^ i • a
have rw₂ : g ^ i • a = g ^ i • a
Tactic: rw [← zpow_mod_period_smul, Int.add_emod_right, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ ((↑(period g a) : ℤ) + i) • a = g ^ i • a
have rw : g ^ (((↑(period g a) : ℤ) + i) % (↑(period g a) : ℤ)) • a = g ^ i • a
Tactic: rw [← zpow_mod_period_smul, Int.add_emod_left, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
rw : g ^ (((↑(period g a) : ℤ) + i) % (↑(period g a) : ℤ)) • a = g ^ i • a
⊢ g ^ ((↑(period g a) : ℤ) + i) • a = g ^ i • a
have rw₁ : g ^ (i % (↑(period g a) : ℤ)) • a = g ^ i • a
Tactic: rw [← zpow_mod_period_smul, Int.add_emod_left, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
i : ℤ
g : G
a : α
rw : g ^ (((↑(period g a) : ℤ) + i) % (↑(period g a) : ℤ)) • a = g ^ i • a
rw₁ : g ^ (i % (↑(period g a) : ℤ)) • a = g ^ i • a
⊢ g ^ ((↑(period g a) : ℤ) + i) • a = g ^ i • a
have rw₂ : g ^ i • a = g ^ i • a
Tactic: rw [← zpow_mod_period_smul, Int.add_emod_left, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod (fun (x : α) ↦ a • x) b ∣ n
have rw : a ^ n • b = b ↔ period a b ∣ n
Tactic: rw [← period_eq_minimalPeriod, 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 α
a : G
b : α
n : ℕ
rw : a ^ n • b = b ↔ period a b ∣ n
⊢ a ^ n • b = b ↔ minimalPeriod (fun (x : α) ↦ a • x) b ∣ n
have rw₁ : period a b ∣ n ↔ period a b ∣ n
Tactic: rw [← period_eq_minimalPeriod, 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 α
a : G
b : α
n : ℤ
⊢ a ^ n • b = b ↔ (↑(minimalPeriod (fun (x : α) ↦ a • x) b) : ℤ) ∣ n
have rw : a ^ n • b = b ↔ (↑(period a b) : ℤ) ∣ n
Tactic: rw [← period_eq_minimalPeriod, zpow_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 α
a : G
b : α
n : ℤ
rw : a ^ n • b = b ↔ (↑(period a b) : ℤ) ∣ n
⊢ a ^ n • b = b ↔ (↑(minimalPeriod (fun (x : α) ↦ a • x) b) : ℤ) ∣ n
have rw₁ : (↑(period a b) : ℤ) ∣ n ↔ (↑(period a b) : ℤ) ∣ n
Tactic: rw [← period_eq_minimalPeriod, zpow_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 α
a : G
b : α
n : ℕ
⊢ a ^ (n % minimalPeriod (fun (x : α) ↦ a • x) b) • b = a ^ n • b
have rw : a ^ (n % period a b) • b = a ^ n • b
Tactic: rw [← period_eq_minimalPeriod, pow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℕ
rw : a ^ (n % period a b) • b = a ^ n • b
⊢ a ^ (n % minimalPeriod (fun (x : α) ↦ a • x) b) • b = a ^ n • b
have rw₁ : a ^ n • b = a ^ n • b
Tactic: rw [← period_eq_minimalPeriod, pow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ (n % (↑(minimalPeriod (fun (x : α) ↦ a • x) b) : ℤ)) • b = a ^ n • b
have rw : a ^ (n % (↑(period a b) : ℤ)) • b = a ^ n • b
Tactic: rw [← period_eq_minimalPeriod, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type v
G : Type u
inst : Group G
inst_1 : MulAction G α
a : G
b : α
n : ℤ
rw : a ^ (n % (↑(period a b) : ℤ)) • b = a ^ n • b
⊢ a ^ (n % (↑(minimalPeriod (fun (x : α) ↦ a • x) b) : ℤ)) • b = a ^ n • b
have rw₁ : a ^ n • b = a ^ n • b
Tactic: rw [← period_eq_minimalPeriod, zpow_mod_period_smul]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p ↔ IsPeriodicPt f p x ∧ ¬IsFixedPt f x
have rw : minimalPeriod f x = p → ¬minimalPeriod f x = 1
Tactic: rw [Function.isPeriodicPt_iff_minimalPeriod_dvd, Nat.dvd_prime hp.out,
    ← minimalPeriod_eq_one_iff_isFixedPt.not, or_and_right, and_not_self_iff, false_or,
    iff_self_and]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
x : α
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)
have h₁ : ¬minimalPeriod f x ∣ p ^ k
Tactic: apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
h₁ : ¬minimalPeriod f x ∣ p ^ k
⊢ minimalPeriod f x = p ^ (k + 1)
have h₂ : minimalPeriod f x ∣ p ^ (k + 1)
Tactic: apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x
have apply : minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
Tactic: apply h.minimalPeriod_of_comp_dvd_mul.antisymm
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
have suffices : ∀ {f g : α → α},
  Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
Tactic: suffices ∀ {f g : α → α},
      Commute f g →
        Coprime (minimalPeriod f x) (minimalPeriod g x) →
          minimalPeriod f x ∣ minimalPeriod (f ∘ g) x from
    hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f_1 : α → α
x : α
g_1 : α → α
h_1 : Function.Commute f_1 g_1
hco_1 : (minimalPeriod f_1 x).Coprime (minimalPeriod g_1 x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
have refine_1 : IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
Tactic: refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f_1 : α → α
x : α
g_1 : α → α
h_1 : Function.Commute f_1 g_1
hco_1 : (minimalPeriod f_1 x).Coprime (minimalPeriod g_1 x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
refine_1 : IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
have refine_2 : IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
Tactic: refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
x : α
inst : Fintype α
⊢ minimalPeriod f x ≤ card α
have rw : (periodicOrbit f x).length ≤ card α
Tactic: rw [← periodicOrbit_length]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
⊢ x ∈ periodicPts f
have obtain : ∀ (m n : ℕ) (heq : f^[m] x = f^[n] x) (hne : m ≠ n), x ∈ periodicPts f
Tactic: obtain ⟨m, n, heq, hne⟩ : ∃ m n, f^[m] x = f^[n] x ∧ m ≠ n := by
    simpa [Injective] using not_injective_infinite_finite (f^[·] x)
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
⊢ x ∈ periodicPts f
have inl : ∀ (hlt : m < n), x ∈ periodicPts f
Tactic: rcases lt_or_gt_of_ne hne with hlt | hlt
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
inl : ∀ (hlt : m < n), x ∈ periodicPts f
⊢ x ∈ periodicPts f
have inr : ∀ (hlt : n < m), x ∈ periodicPts f
Tactic: rcases lt_or_gt_of_ne hne with hlt | hlt
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
inst : Finite α
⊢ Injective f ↔ periodicPts f = univ
have refine : ∀ (h : periodicPts f = univ), Injective f
Tactic: refine ⟨fun h ↦ eq_univ_iff_forall.mpr h.mem_periodicPts, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : periodicPts f = univ
⊢ Injective f
have rw : periodicPts f ⊆ range f
Tactic: rw [Finite.injective_iff_surjective, ← range_eq_univ, ← univ_subset_iff, ← h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x
have rw : minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
Tactic: rw [minimalPeriod_prodMap]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x
have rw : minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
Tactic: rw [minimalPeriod_prodMap]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
| minimalPeriod (Pi.map (α := α) (β := α) f) x
have simp : sInf {n : ℕ | 0 < n ∧ ∀ (i : ι), IsPeriodicPt (f i) n (x i)}
Tactic: simp [minimalPeriod_eq_sInf_n_pos_IsPeriodicPt]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
⊢ minimalPeriod (Pi.map (α := α) (β := α) f) x = sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
have conv_lhs : Eq (α := ℕ) (sInf {n : ℕ | 0 < n ∧ ∀ (i : ι), IsPeriodicPt (f i) n (x i)})
  (sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n})
Tactic: conv_lhs => simp [minimalPeriod_eq_sInf_n_pos_IsPeriodicPt]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
⊢ minimalPeriod (f i) (x i) ∣ minimalPeriod (Pi.map (α := α) (β := α) f) x
have simp : minimalPeriod (f i) (x i) ∣ sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
Tactic: simp only [minimalPeriod_piMap]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
⊢ minimalPeriod (f i) (x i) ∣ sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
have pos : ∀ (h : Set.Nonempty (α := ℕ) {n : ℕ | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}),
  minimalPeriod (f i) (x i) ∣ sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
Tactic: by_cases h : {n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Lemmas (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
pos :
  ∀ (h : Set.Nonempty (α := ℕ) {n : ℕ | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}),
    minimalPeriod (f i) (x i) ∣ sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
⊢ minimalPeriod (f i) (x i) ∣ sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
have neg : ∀ (h : ¬Set.Nonempty (α := ℕ) {n : ℕ | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}),
  minimalPeriod (f i) (x i) ∣ sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
Tactic: by_cases h : {n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
x : G → A
⊢ mulShift 1 x = x
have h : ∀ (h : G), mulShift 1 x h = x h
Tactic: ext h
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
g₁ g₂ : G
x : G → A
⊢ mulShift (g₁ * g₂) x = mulShift g₂ (mulShift g₁ x)
have h : ∀ (h : G), mulShift (g₁ * g₂) x h = mulShift g₂ (mulShift g₁ x) h
Tactic: ext h
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : TopologicalSpace A
g : G
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] (mulShift g)
have unfold : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : G → A) (h : G) ↦ x (g * h)
Tactic: unfold mulShift
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
G : Type u_2
U : Finset G
x : G → A
⊢ cylinder U x = (↑U : Set G).pi (α := fun (i : G) ↦ A) fun (i : G) ↦ {x i}
have h : ∀ (y : G → A),
  y ∈ cylinder U x ↔ Membership.mem (γ := Set (G → A)) ((↑U : Set G).pi (α := fun (i : G) ↦ A) fun (i : G) ↦ {x i}) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v h : G
⊢ A
have if : (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) h) → A
Tactic: if hmem : h ∈ p.support.image (v * ·) then
    -- package existence of a preimage under (v * ·)
    let ex : ∃ w, w ∈ p.support ∧ v * w = h := by
      simpa [Finset.mem_image] using hmem
    exact p.config (Classical.choose ex)
  else
    exact default
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v h : G
if : (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) h) → A
⊢ A
have if₁ : (hmem : h ∉ Finset.image (fun (x : G) ↦ v * x) p.support) → A
Tactic: if hmem : h ∈ p.support.image (v * ·) then
    -- package existence of a preimage under (v * ·)
    let ex : ∃ w, w ∈ p.support ∧ v * w = h := by
      simpa [Finset.mem_image] using hmem
    exact p.config (Classical.choose ex)
  else
    exact default
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
⊢ p.mulShift v (v * w) = p.config w
have hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
Tactic: have hmem : (v * w) ∈ p.support.image (v * ·) :=
    Finset.mem_image.mpr ⟨w, hw, rfl⟩
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
⊢ p.mulShift v (v * w) = p.config w
have ex : ∃ w' ∈ p.support, v * w' = v * w
Tactic: have ex : ∃ w', w' ∈ p.support ∧ v * w' = v * w := by
    simpa [Finset.mem_image] using hmem
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
⊢ p.mulShift v (v * w) = p.config w
have h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
Tactic: have h1 : p.mulShift v (v * w) = p.config (Classical.choose ex) := by
    simp [Pattern.mulShift, hmem]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
⊢ p.mulShift v (v * w) = p.config w
have hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w
Tactic: have hwv' : v * Classical.choose ex = v * w := (Classical.choose_spec ex).2
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w
⊢ p.mulShift v (v * w) = p.config w
have h_eq : Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = w
Tactic: have h_eq : Classical.choose ex = w := mul_left_cancel hwv'
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w
h_eq : Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = w
⊢ p.mulShift v (v * w) = p.config w
have rw : p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex) = p.config w
Tactic: rw [h1, h_eq]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w
h_eq : Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = w
rw : p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex) = p.config w
⊢ p.mulShift v (v * w) = p.config w
have rw₁ : p.config w = p.config w
Tactic: rw [h1, h_eq]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
⊢ p.mulShift v (v * w) = p.config w
have is : ∀ (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)),
  p.mulShift v (v * w) = p.config w
Tactic: classical
  -- (v * w) is in the translated support
  have hmem : (v * w) ∈ p.support.image (v * ·) :=
    Finset.mem_image.mpr ⟨w, hw, rfl⟩
  -- existential used in the branch
  have ex : ∃ w', w' ∈ p.support ∧ v * w' = v * w := by
    simpa [Finset.mem_image] using hmem
  -- open the `if` branch as returned by the definition
  have h1 : p.mulShift v (v * w) = p.config (Classical.choose ex) := by
    simp [Pattern.mulShift, hmem]
  -- the chosen witness equals w by left-cancellation
  have hwv' : v * Classical.choose ex = v * w := (Classical.choose_spec ex).2
  have h_eq : Classical.choose ex = w := mul_left_cancel hwv'
  rw [h1, h_eq]