awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 h₂ h₃ h₄ h₅ : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x ∣ p ^ (k + 1)

Tactic:
rwa [← isPeriodicPt_iff_minimalPeriod_dvd]

Premises used: Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ minimalPeriod (f ∘ g) x ∣ minimalPeriod f x * minimalPeriod g x

Tactic:
dvd_trans h.minimalPeriod_of_comp_dvd_lcm (Nat.lcm_dvd_mul _ _)

Premises used: dvd_trans, Function.Commute.minimalPeriod_of_comp_dvd_lcm, Nat.lcm_dvd_mul
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
apply : minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

Tactic:
apply h.minimalPeriod_of_comp_dvd_mul.antisymm

Premises used: Function.Commute.minimalPeriod_of_comp_dvd_mul, Dvd.dvd.antisymm
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
suffices :
  ∀ {f g : α → α},
    Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
⊢ minimalPeriod f x * minimalPeriod g 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)
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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

Tactic:
hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd

Premises used: Function.IsPeriodicPt.minimalPeriod_dvd, Function.IsPeriodicPt.left_of_comp, Nat.Coprime.dvd_of_dvd_mul_left
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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
refine_2 : IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Tactic:
refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd

Premises used: Function.IsPeriodicPt.minimalPeriod_dvd, Function.IsPeriodicPt.left_of_comp, Nat.Coprime.dvd_of_dvd_mul_left
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
(isPeriodicPt_minimalPeriod _ _).const_mul _

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.const_mul
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
exact (isPeriodicPt_minimalPeriod _ _).const_mul _

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.const_mul
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
(isPeriodicPt_minimalPeriod _ _).mul_const _

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.mul_const
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
exact (isPeriodicPt_minimalPeriod _ _).mul_const _

Premises used: Function.isPeriodicPt_minimalPeriod, Function.IsPeriodicPt.mul_const
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
inst : Fintype α
rw : (periodicOrbit f x).length ≤ card α
⊢ minimalPeriod f x ≤ card α

Tactic:
rw [← periodicOrbit_length]

Premises used: Function.periodicOrbit_length
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
inst : Fintype α
⊢ (periodicOrbit f x).length ≤ card α

Tactic:
List.Nodup.length_le_card nodup_periodicOrbit

Premises used: List.Nodup.length_le_card, Cycle.length, Function.nodup_periodicOrbit
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
inst : Fintype α
⊢ (periodicOrbit f x).length ≤ card α

Tactic:
exact List.Nodup.length_le_card nodup_periodicOrbit

Premises used: List.Nodup.length_le_card, Function.nodup_periodicOrbit
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
x : α
inst : Fintype α
h : x ∈ periodicPts f
⊢ IsPeriodicPt f (card α)! x

Tactic:
isPeriodicPt_iff_minimalPeriod_dvd.mpr
    (Nat.dvd_factorial (minimalPeriod_pos_of_mem_periodicPts h) minimalPeriod_le_card)

Premises used: Iff.mpr, Function.minimalPeriod_le_card, Nat.dvd_factorial, Function.minimalPeriod_pos_of_mem_periodicPts, Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
⊢ ∃ (m : ℕ) (n : ℕ), f^[m] x = f^[n] x ∧ m ≠ n

Tactic:
simpa [Injective] using not_injective_infinite_finite (f^[·] x)

Premises used: not_injective_infinite_finite, Nat.iterate, Function.Injective
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
obtain : ∀ (m n : ℕ) (heq : f^[m] x = f^[n] x) (hne : m ≠ n), x ∈ periodicPts f
⊢ 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)
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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
inr : ∀ (hlt : n < m), x ∈ periodicPts f
⊢ x ∈ periodicPts f

Tactic:
rcases lt_or_gt_of_ne hne with hlt | hlt

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : m < n
⊢ 0 < n - m

Tactic:
lia
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : m < n
⊢ x ∈ periodicPts f

Tactic:
exact mk_mem_periodicPts (by lia) (iterate_cancel h heq.symm)

Premises used: Function.iterate_cancel, Eq.symm, Function.mk_mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : n < m
⊢ 0 < m - n

Tactic:
lia
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : n < m
⊢ x ∈ periodicPts f

Tactic:
exact mk_mem_periodicPts (by lia) (iterate_cancel h heq)

Premises used: Function.iterate_cancel, Function.mk_mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
⊢ Injective f ↔ periodicPts f = univ

Tactic:
⟨fun h ↦ eq_univ_iff_forall.mpr h.mem_periodicPts, fun h ↦ ?_⟩

Premises used: Iff.mpr, Set.eq_univ_iff_forall, Iff.intro, Function.Injective.mem_periodicPts
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
refine : ∀ (h : periodicPts f = univ), Injective f
⊢ Injective f ↔ periodicPts f = univ

Tactic:
refine ⟨fun h ↦ eq_univ_iff_forall.mpr h.mem_periodicPts, fun h ↦ ?_⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : periodicPts f = univ
rw : periodicPts f ⊆ range f
⊢ Injective f

Tactic:
rw [Finite.injective_iff_surjective, ← range_eq_univ, ← univ_subset_iff, ← h]

Premises used: Set.range_eq_univ, Set.univ_subset_iff, Finite.injective_iff_surjective
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Finite α
h : periodicPts f = univ
⊢ periodicPts f ⊆ range f

Tactic:
apply periodicPts_subset_range

Premises used: Function.periodicPts_subset_range
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
f : α → α
inst : Fintype α
⊢ Injective f ↔ f^[(card α)!] = id

Tactic:
simp only [injective_iff_periodicPts_eq_univ, mem_periodicPts_iff_isPeriodicPt_factorial_card,
    funext_iff, eq_univ_iff_forall, IsPeriodicPt, id, IsFixedPt]

Premises used: Set.eq_univ_iff_forall, funext_iff, id, Function.IsPeriodicPt, Function.mem_periodicPts_iff_isPeriodicPt_factorial_card, Function.injective_iff_periodicPts_eq_univ, Function.IsFixedPt
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ ∀ (c : ℕ), minimalPeriod (Prod.map f g) x ∣ c ↔ (minimalPeriod f x.1).lcm (minimalPeriod g x.2) ∣ c

Tactic:
simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]

Premises used: Nat.lcm_dvd_iff, Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
rw : minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
⊢ minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x

Tactic:
rw [minimalPeriod_prodMap]

Premises used: Function.minimalPeriod_prodMap
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Tactic:
Nat.dvd_lcm_left _ _

Premises used: Nat.dvd_lcm_left
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Tactic:
exact Nat.dvd_lcm_left _ _

Premises used: Nat.dvd_lcm_left
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
rw : minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
⊢ minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x

Tactic:
rw [minimalPeriod_prodMap]

Premises used: Function.minimalPeriod_prodMap
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Tactic:
Nat.dvd_lcm_right _ _

Premises used: Nat.dvd_lcm_right
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Tactic:
exact Nat.dvd_lcm_right _ _

Premises used: Nat.dvd_lcm_right
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
simp : sInf {n : ℕ | 0 < n ∧ ∀ (i : ι), IsPeriodicPt (f i) n (x i)}
| minimalPeriod (Pi.map (α := α) (β := α) f) x

Tactic:
simp [minimalPeriod_eq_sInf_n_pos_IsPeriodicPt]

Premises used: Function.minimalPeriod_eq_sInf_n_pos_IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
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})
⊢ minimalPeriod (Pi.map (α := α) (β := α) f) x = sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}

Tactic:
conv_lhs => simp [minimalPeriod_eq_sInf_n_pos_IsPeriodicPt]

Premises used: Function.minimalPeriod_eq_sInf_n_pos_IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
⊢ Eq (α := ℕ) (sInf {n : ℕ | 0 < n ∧ ∀ (i : ι), IsPeriodicPt (f i) n (x i)})
    (sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n})

Tactic:
simp [← isPeriodicPt_iff_minimalPeriod_dvd]

Premises used: Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
inst : Fintype ι
⊢ ∀ (c : ℕ),
    minimalPeriod (Pi.map (α := α) (β := α) f) x ∣ c ↔
      (Finset.lcm Finset.univ fun (i : ι) ↦ minimalPeriod (f i) (x i)) ∣ c

Tactic:
simp [← isPeriodicPt_iff_minimalPeriod_dvd]

Premises used: Function.isPeriodicPt_iff_minimalPeriod_dvd
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
simp : minimalPeriod (f i) (x i) ∣ sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
⊢ minimalPeriod (f i) (x i) ∣ minimalPeriod (Pi.map (α := α) (β := α) f) x

Tactic:
simp only [minimalPeriod_piMap]

Premises used: Function.minimalPeriod_piMap
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
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}
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}
⊢ 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

Premises used: setOf, And, Set.Nonempty, LT.lt, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
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:
(Nat.sInf_mem h).2 i

Premises used: Set.Mem, setOf, Nat.sInf_mem, And.right
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
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:
exact (Nat.sInf_mem h).2 i

Premises used: Nat.sInf_mem, And.right
-- Module: Mathlib.Dynamics.PeriodicPts.Lemmas
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
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:
simp [not_nonempty_iff_eq_empty.mp h]

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
g : G
x : G → A
h : G
⊢ mulShift g x h = x (g * h)

Tactic:
rfl

Premises used: SymbolicDynamics.FullShift.mulShift, rfl
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
x : G → A
h : ∀ (h : G), mulShift 1 x h = x h
⊢ mulShift 1 x = x

Tactic:
ext h
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
x : G → A
h : G
⊢ mulShift 1 x h = x h

Tactic:
simp [mulShift]

Premises used: SymbolicDynamics.FullShift.mulShift
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
g₁ g₂ : G
x : G → A
h : ∀ (h : G), mulShift (g₁ * g₂) x h = mulShift g₂ (mulShift g₁ x) h
⊢ mulShift (g₁ * g₂) x = mulShift g₂ (mulShift g₁ x)

Tactic:
ext h
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
g₁ g₂ : G
x : G → A
h : G
⊢ mulShift (g₁ * g₂) x h = mulShift g₂ (mulShift g₁ x) h

Tactic:
simp [mulShift, mul_assoc]

Premises used: SymbolicDynamics.FullShift.mulShift, mul_assoc
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : TopologicalSpace A
g : G
unfold : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : G → A) (h : G) ↦ x (g * h)
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] (mulShift g)

Tactic:
unfold mulShift

Premises used: SymbolicDynamics.FullShift.mulShift
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : TopologicalSpace A
g : G
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : G → A) (h : G) ↦ x (g * h)

Tactic:
fun_prop
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
U : Finset G
x : G → A
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
⊢ cylinder U x = (↑U : Set G).pi (α := fun (i : G) ↦ A) fun (i : G) ↦ {x i}

Tactic:
ext y
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
U : Finset G
x 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:
simp [cylinder, Set.pi]

Premises used: Set.pi, SymbolicDynamics.FullShift.cylinder
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
U : Finset G
x y : G → A
⊢ y ∈ cylinder U x ↔ ∀ i ∈ U, y i = x i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SymbolicDynamics.FullShift.cylinder
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : TopologicalSpace A
inst_1 : DiscreteTopology A
U : Finset G
x : G → A
⊢ ∀ a ∈ (↑U : Set G), IsOpen[inst] {x a}

Tactic:
simp
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : TopologicalSpace A
inst_1 : DiscreteTopology A
U : Finset G
x : G → A
⊢ IsOpen[Pi.topologicalSpace] (cylinder U x)

Tactic:
simpa [cylinder_eq_set_pi U x] using isOpen_set_pi (U.finite_toSet) (by simp)

Premises used: isOpen_set_pi, Finset.finite_toSet, SymbolicDynamics.FullShift.cylinder_eq_set_pi
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : TopologicalSpace A
inst_1 : T1Space A
U : Finset G
x : G → A
⊢ ∀ a ∈ (↑U : Set G), IsClosed[inst] {x a}

Tactic:
simp
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
G : Type u_2
inst : TopologicalSpace A
inst_1 : T1Space A
U : Finset G
x : G → A
⊢ IsClosed[Pi.topologicalSpace] (cylinder U x)

Tactic:
simpa [cylinder_eq_set_pi U x] using isClosed_set_pi (by simp)

Premises used: isClosed_set_pi, SymbolicDynamics.FullShift.cylinder_eq_set_pi
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) h
⊢ ∃ w ∈ p.support, v * w = h

Tactic:
simpa [Finset.mem_image] using hmem

Premises used: Finset.mem_image
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) h
let : A
⊢ A

Tactic:
let ex : ∃ w, w ∈ p.support ∧ v * w = h := by
      simpa [Finset.mem_image] using hmem
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) h
ex : ∃ w ∈ p.support, v * w = h := ⋯
⊢ A

Tactic:
exact p.config (Classical.choose ex)

Premises used: SymbolicDynamics.FullShift.Pattern.config, Classical.choose
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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
hmem : h ∉ Finset.image (fun (x : G) ↦ v * x) p.support
⊢ A

Tactic:
exact default

Premises used: Inhabited.default
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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
if₁ : (hmem : h ∉ Finset.image (fun (x : G) ↦ v * x) p.support) → A
if₂ : (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) h) → A
if₃ if₄ : (hmem : h ∉ Finset.image (fun (x : G) ↦ v * x) p.support) → A
⊢ 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

Premises used: Inhabited.default, HMul.hMul, SymbolicDynamics.FullShift.Pattern.support, Finset.image
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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 : G
intro : (h : G) → A
⊢ G → A

Tactic:
classical
  intro h
  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

Premises used: Inhabited.default
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
x : G → A
U : Finset G
⊢ Pattern A G

Tactic:
exact { config := fun g => if g ∈ U then x g else default,
          support := U,
          condition := fun g hg => if_neg hg }
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
x : G → A
U : Finset G
⊢ Pattern A G

Tactic:
classical
  exact { config := fun g => if g ∈ U then x g else default,
          support := U,
          condition := fun g hg => if_neg hg }
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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
⊢ 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⟩
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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)
⊢ ∃ w' ∈ p.support, v * w' = v * w

Tactic:
simpa [Finset.mem_image] using hmem

Premises used: Finset.mem_image
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
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)
⊢ ∃ 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