awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
val : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
a : (fun (g : G) ↦ if h : g ∈ dom then cfg g else default) = cfg
⊢ (↑((fun (f : ↥dom → A) ↦
            (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
                {
                  config := fun (g : G) ↦
                    if h : g ∈ dom then f (Subtype.mk (p := fun (x : G) ↦ x ∈ dom) g h) else default,
                  support := dom, condition := ⋯ }
                ⋯ :
              { p : Pattern A G // p.support = dom }))
          ((fun (p : { p : Pattern A G // p.support = dom }) (i : ↥dom) ↦ (↑p : Pattern A G).config (↑i : G))
            (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
              { config := cfg, support := dom, condition := cond } ⋯))) :
      Pattern A G) =
    (↑(Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
          { config := cfg, support := dom, condition := cond : Pattern A G } ⋯) :
      Pattern A G)

Tactic:
simp only [Pattern.mk.injEq, and_true]

Premises used: and_true, SymbolicDynamics.FullShift.Pattern.mk.injEq
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
val : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
a : ∀ (g : G), (if h : g ∈ dom then cfg g else default) = cfg g
⊢ (fun (g : G) ↦ if h : g ∈ dom then cfg g else default) = cfg

Tactic:
funext g
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
val : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
pos : ∀ (hg : g ∈ dom), (if h : g ∈ dom then cfg g else default) = cfg g
neg : ∀ (hg : g ∉ dom), (if h : g ∈ dom then cfg g else default) = cfg g
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
by_cases hg : g ∈ dom
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
val : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∈ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
simp [hg]
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
val : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∉ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
simp [hg, cond g hg]
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
val : Fintype A
f : ↥U → A
h :
  ∀ (i : ↥U),
    (fun (p : { p : Pattern A G // p.support = U }) (i : ↥U) ↦ (↑p : Pattern A G).config (↑i : G))
        ((fun (f : ↥U → A) ↦
            (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = U)
                { config := fun (g : G) ↦ if h : g ∈ U then f (Subtype.mk (p := fun (x : G) ↦ x ∈ U) g h) else default,
                  support := U, condition := ⋯ }
                ⋯ :
              { p : Pattern A G // p.support = U }))
          f)
        i =
      f i
⊢ (fun (p : { p : Pattern A G // p.support = U }) (i : ↥U) ↦ (↑p : Pattern A G).config (↑i : G))
      ((fun (f : ↥U → A) ↦
          (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = U)
              { config := fun (g : G) ↦ if h : g ∈ U then f (Subtype.mk (p := fun (x : G) ↦ x ∈ U) g h) else default,
                support := U, condition := ⋯ }
              ⋯ :
            { p : Pattern A G // p.support = U }))
        f) =
    f

Tactic:
ext i
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
val : Fintype A
f : ↥U → A
i : ↥U
⊢ (fun (p : { p : Pattern A G // p.support = U }) (i : ↥U) ↦ (↑p : Pattern A G).config (↑i : G))
      ((fun (f : ↥U → A) ↦
          (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = U)
              { config := fun (g : G) ↦ if h : g ∈ U then f (Subtype.mk (p := fun (x : G) ↦ x ∈ U) g h) else default,
                support := U, condition := ⋯ }
              ⋯ :
            { p : Pattern A G // p.support = U }))
        f)
      i =
    f i

Tactic:
simp [i.2]

Premises used: Subtype.property
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
val : Fintype A
e : { p : Pattern A G // p.support = U } ≃ (↥U → A) :=
  { toFun := fun (p : { p : Pattern A G // p.support = U }) (i : ↥U) ↦ (↑p : Pattern A G).config (↑i : G),
    invFun := fun (f : ↥U → A) ↦
      Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = U)
        { config := fun (g : G) ↦ if h : g ∈ U then f (Subtype.mk (p := fun (x : G) ↦ x ∈ U) g h) else default,
          support := U, condition := ⋯ }
        ⋯,
    left_inv := ⋯, right_inv := ⋯ }
this : Fintype (↑{p : Pattern A G | p.support = U} : Type (max u_3 u_4)) := Fintype.ofEquiv (↥U → A) e.symm
⊢ Set.Finite (α := Pattern A G) {p : Pattern A G | p.support = U}

Tactic:
apply toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
val : Fintype A
intro intro₁ intro₂ intro₃ : Set.Finite (α := Pattern A G) {p : Pattern A G | p.support = U}
⊢ Set.Finite (α := Pattern A G) {p : Pattern A G | p.support = U}

Tactic:
classical
  -- Patterns with support U biject with (U → A) via restriction/extension
  let e : { p : Pattern A G // p.support = U } ≃ (U → A) :=
  { toFun := fun p i => p.1.config i.1
    invFun := fun f => ⟨{ config := fun g => if h : g ∈ U then f ⟨g, h⟩ else default,
                           support := U,
                           condition := fun g hg => by simp [hg] }, rfl⟩
    left_inv := by
      rintro ⟨⟨cfg, dom, cond⟩, hU⟩
      simp only at hU; subst hU
      apply Subtype.ext
      simp only [Pattern.mk.injEq, and_true]
      funext g
      by_cases hg : g ∈ dom
      · simp [hg]
      · simp [hg, cond g hg]
    right_inv := fun f => by ext i; simp [i.2] }
  let : Fintype { p : Pattern A G | p.support = U } := Fintype.ofEquiv (U → A) e.symm
  apply toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ dynEntourage T U n = ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U

Tactic:
simp [dynEntourage]

Premises used: Dynamics.dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
x y : X
⊢ (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U

Tactic:
simp [dynEntourage]

Premises used: Dynamics.dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
x y : X
⊢ y ∈ ball x (dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ ball (T^[k] x) U

Tactic:
simp only [ball, mem_preimage, mem_dynEntourage]

Premises used: Dynamics.mem_dynEntourage, UniformSpace.ball, Set.mem_preimage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
rw : ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
⊢ dynEntourage T U n ∈ 𝓤 X

Tactic:
rw [dynEntourage_eq_inter_Ico T U n]

Premises used: Dynamics.dynEntourage_eq_inter_Ico
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
⊢ ⋂ (k : (↑(Ico 0 0) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X

Tactic:
simp
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
succ :
  ∀ (ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X), ⋂ (i : ℕ), ⋂ (_ : i < n + 1), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ (k : (↑(Ico 0 (n + 1)) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X

Tactic:
simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢

Premises used: Nat.zero_le, Set.mem_Ico, Set.iInter_coe_set, true_and
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
succ : (⋂ (k : ℕ), ⋂ (_ : k < n), (map T T)^[k] ⁻¹' U) ∩ (map T T)^[n] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ (i : ℕ), ⋂ (_ : i < n + 1), (map T T)^[i] ⁻¹' U ∈ 𝓤 X

Tactic:
rw [Set.biInter_lt_succ]

Premises used: Set.biInter_lt_succ
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
succ : (map T T)^[n] ⁻¹' U ∈ 𝓤 X
⊢ (⋂ (k : ℕ), ⋂ (_ : k < n), (map T T)^[k] ⁻¹' U) ∩ (map T T)^[n] ⁻¹' U ∈ 𝓤 X

Tactic:
apply Filter.inter_mem ih

Premises used: Filter.inter_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
succ : map T^[n] T^[n] ⁻¹' U ∈ 𝓤 X
⊢ (map T T)^[n] ⁻¹' U ∈ 𝓤 X

Tactic:
rw [map_iterate T T n]

Premises used: Prod.map_iterate
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ map T^[n] T^[n] ⁻¹' U ∈ 𝓤 X

Tactic:
uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni

Premises used: uniformContinuous_def, Set.Mem, setOf, Prod.map, UniformContinuous.iterate, Set.preimage, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ map T^[n] T^[n] ⁻¹' U ∈ 𝓤 X

Tactic:
exact uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni

Premises used: uniformContinuous_def, UniformContinuous.iterate, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
zero : ⋂ (k : (↑(Ico 0 0) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
succ :
  ∀ (n : ℕ) (ih : ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X),
    ⋂ (k : (↑(Ico 0 (n + 1)) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢
    rw [Set.biInter_lt_succ]
    apply Filter.inter_mem ih
    rw [map_iterate T T n]
    exact uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni

Premises used: Nat.zero_le, uniformContinuous_def, Set.mem_Ico, UniformContinuous.iterate, Iff.mp, Set.biInter_lt_succ, Set.iInter_coe_set, Prod.map_iterate, true_and
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : Continuous[inst.toTopologicalSpace, inst.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
rw :
  ∀ (a : ℕ) (b : a ∈ Ico 0 n), ball x ((map T T)^[(↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ico 0 n) a b) : ℕ)] ⁻¹' U) ∈ 𝓝 x
⊢ ball x (dynEntourage T U n) ∈ 𝓝 x

Tactic:
rw [dynEntourage_eq_inter_Ico T U n, ball_iInter, Filter.iInter_mem, Subtype.forall]

Premises used: Subtype.forall, UniformSpace.ball_iInter, Filter.iInter_mem, Dynamics.dynEntourage_eq_inter_Ico
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : Continuous[inst.toTopologicalSpace, inst.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
k : ℕ
_ : ∀ (b : k ∈ Ico 0 n), ball x ((map T T)^[(↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ico 0 n) k b) : ℕ)] ⁻¹' U) ∈ 𝓝 x
⊢ ∀ (b : k ∈ Ico 0 n), ball x ((map T T)^[(↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ico 0 n) k b) : ℕ)] ⁻¹' U) ∈ 𝓝 x

Tactic:
_
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : Continuous[inst.toTopologicalSpace, inst.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
k : ℕ
b : k ∈ Ico 0 n
simp : T^[k] ⁻¹' ball (T^[k] x) U ∈ 𝓝 x
⊢ ball x ((map T T)^[(↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ico 0 n) k b) : ℕ)] ⁻¹' U) ∈ 𝓝 x

Tactic:
simp only [map_iterate, _root_.ball_preimage]

Premises used: ball_preimage, Prod.map_iterate
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : Continuous[inst.toTopologicalSpace, inst.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
k : ℕ
b : k ∈ Ico 0 n
⊢ T^[k] ⁻¹' ball (T^[k] x) U ∈ 𝓝 x

Tactic:
(h.iterate k).continuousAt.preimage_mem_nhds (ball_mem_nhds (T^[k] x) U_uni)

Premises used: UniformSpace.ball_mem_nhds, ContinuousAt.preimage_mem_nhds, Nat.iterate, Continuous.continuousAt, Continuous.iterate
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : Continuous[inst.toTopologicalSpace, inst.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
k : ℕ
b : k ∈ Ico 0 n
⊢ T^[k] ⁻¹' ball (T^[k] x) U ∈ 𝓝 x

Tactic:
exact (h.iterate k).continuousAt.preimage_mem_nhds (ball_mem_nhds (T^[k] x) U_uni)

Premises used: UniformSpace.ball_mem_nhds, ContinuousAt.preimage_mem_nhds, Nat.iterate, Continuous.continuousAt, Continuous.iterate
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst : U.IsRefl
simp : SetRel.IsRefl.{u_1} (α := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
⊢ (dynEntourage T U n).IsRefl

Tactic:
simp [dynEntourage]

Premises used: Dynamics.dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst : U.IsRefl
⊢ SetRel.IsRefl.{u_1} (α := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)

Tactic:
infer_instance
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst : U.IsSymm
simp : SetRel.IsSymm.{u_1} (α := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
⊢ (dynEntourage T U n).IsSymm

Tactic:
simp [dynEntourage]

Premises used: Dynamics.dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst : U.IsSymm
⊢ SetRel.IsSymm.{u_1} (α := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)

Tactic:
infer_instance
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n : ℕ
simp :
  ∀ (i : ℕ) (i_1 : i < n),
    SetRel.comp (β := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
        (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V) ⊆
      map T^[i] T^[i] ⁻¹' (U ○ V)
⊢ dynEntourage T U n ○ dynEntourage T V n ⊆ dynEntourage T (U ○ V) n

Tactic:
simp only [dynEntourage, map_iterate, subset_iInter_iff]

Premises used: Set.subset_iInter_iff, Dynamics.dynEntourage, Prod.map_iterate
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
xy_comp :
  Membership.mem (γ := Set (X × X))
    (SetRel.comp (β := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
      (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V))
    xy
simp :
  ∀
    (xy_comp :
      ∃ (b : X),
        (∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] b) ∈ U) ∧ ∀ (i : ℕ) (i_1 : i < n), (T^[i] b, T^[i] xy.2) ∈ V),
    ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V
⊢ xy ∈ map T^[k] T^[k] ⁻¹' (U ○ V)

Tactic:
simp only [SetRel.comp, mem_iInter, mem_preimage, map_apply, mem_setOf_eq] at xy_comp ⊢

Premises used: Set.mem_setOf_eq, Set.mem_iInter, SetRel.comp, Prod.map_apply, Set.mem_preimage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
xy_comp :
  ∃ (b : X), (∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] b) ∈ U) ∧ ∀ (i : ℕ) (i_1 : i < n), (T^[i] b, T^[i] xy.2) ∈ V
rcases :
  ∀ (z : X) (hz1 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] z) ∈ U)
    (hz2 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] z, T^[i] xy.2) ∈ V),
    ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V
⊢ ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V

Tactic:
rcases xy_comp with ⟨z, hz1, hz2⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
z : X
hz1 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] z) ∈ U
hz2 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] z, T^[i] xy.2) ∈ V
⊢ ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V

Tactic:
mem_ball_comp (hz1 k k_n) (hz2 k k_n)

Premises used: UniformSpace.mem_ball_comp, Set.Mem, setOf, UniformSpace.ball, SetRel.comp, Set.preimage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
z : X
hz1 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] z) ∈ U
hz2 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] z, T^[i] xy.2) ∈ V
⊢ ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V

Tactic:
exact mem_ball_comp (hz1 k k_n) (hz2 k k_n)

Premises used: UniformSpace.mem_ball_comp
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
U : SetRel X X
inst : TopologicalSpace X
T : X → X
T_cont : Continuous[inst, inst] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
rw : IsOpen[instTopologicalSpaceProd] (⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U)
⊢ IsOpen[instTopologicalSpaceProd] (Dynamics.dynEntourage T U n)

Tactic:
rw [dynEntourage_eq_inter_Ico T U n]

Premises used: Dynamics.dynEntourage_eq_inter_Ico
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
U : SetRel X X
inst : TopologicalSpace X
T : X → X
T_cont : Continuous[inst, inst] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
⊢ IsOpen[instTopologicalSpaceProd] (⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U)

Tactic:
isOpen_iInter_of_finite fun k ↦ ?_

Premises used: isOpen_iInter_of_finite
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
U : SetRel X X
inst : TopologicalSpace X
T : X → X
T_cont : Continuous[inst, inst] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
refine : ∀ (k : (↑(Ico 0 n) : Type)), IsOpen[instTopologicalSpaceProd] ((map T T)^[(↑k : ℕ)] ⁻¹' U)
⊢ IsOpen[instTopologicalSpaceProd] (⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U)

Tactic:
refine isOpen_iInter_of_finite fun k ↦ ?_

Premises used: isOpen_iInter_of_finite
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
U : SetRel X X
inst : TopologicalSpace X
T : X → X
T_cont : Continuous[inst, inst] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
k : (↑(Ico 0 n) : Type)
⊢ IsOpen[instTopologicalSpaceProd] ((map T T)^[(↑k : ℕ)] ⁻¹' U)

Tactic:
U_open.preimage ((T_cont.prodMap T_cont).iterate k)

Premises used: Continuous.prodMap, Continuous.iterate, IsOpen.preimage, Subtype.val
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
U : SetRel X X
inst : TopologicalSpace X
T : X → X
T_cont : Continuous[inst, inst] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
k : (↑(Ico 0 n) : Type)
⊢ IsOpen[instTopologicalSpaceProd] ((map T T)^[(↑k : ℕ)] ⁻¹' U)

Tactic:
exact U_open.preimage ((T_cont.prodMap T_cont).iterate k)

Premises used: Continuous.prodMap, Continuous.iterate, IsOpen.preimage, Subtype.val
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
n : ℕ
⊢ Monotone (β := SetRel X X) fun (U : SetRel X X) ↦ dynEntourage T U n

Tactic:
fun _ _ h ↦ iInter₂_mono fun _ _ ↦ preimage_mono h

Premises used: Set.iInter₂_mono, Monotone, Dynamics.dynEntourage, Set.preimage_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
m n : ℕ
m_n : m ≤ n
k : ℕ
k_m : k < m
w : ℕ
w₁ : k < n
h : (map T T)^[k] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U
⊢ ∃ (i : ℕ) (_ : i < n), (map T T)^[i] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U

Tactic:
use k, lt_of_lt_of_le k_m m_n

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
hUV : U ⊆ V
hmn : m ≤ n
⊢ dynEntourage T U n ⊆ dynEntourage T V m

Tactic:
(dynEntourage_monotone _ _ hUV).trans (dynEntourage_antitone _ _ hmn)

Premises used: LE.le.trans, Dynamics.dynEntourage_antitone, Dynamics.dynEntourage_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ dynEntourage T U 0 = univ

Tactic:
simp [dynEntourage]

Premises used: Dynamics.dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ dynEntourage T U 1 = U

Tactic:
simp [dynEntourage]

Premises used: Dynamics.dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
n : ℕ
⊢ dynEntourage T univ n = univ

Tactic:
simp [dynEntourage]

Premises used: Dynamics.dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst : U.IsSymm
x y : X
h : (ball x (dynEntourage T U n) ∩ ball y (dynEntourage T U n)).Nonempty
rcases :
  ∀ (z : X) (z_Bx : z ∈ ball x (dynEntourage T U n)) (z_By : z ∈ ball y (dynEntourage T U n)),
    x ∈ ball y (dynEntourage T (U ○ U) n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
rcases h with ⟨z, z_Bx, z_By⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst : U.IsSymm
x y z : X
z_Bx : z ∈ ball x (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball z (dynEntourage T U n)

Tactic:
rw [mem_ball_symmetry] at z_Bx

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst : U.IsSymm
x y z : X
z_Bx : z ∈ ball x (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
z_Bx₁ : x ∈ ball z (dynEntourage T U n)
⊢ z ∈ ball y (dynEntourage T U n)

Tactic:
rw [mem_ball_symmetry] at z_Bx

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst : U.IsSymm
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
dynEntourage_comp_subset T U U n (mem_ball_comp z_By z_Bx)

Premises used: iInf, UniformSpace.mem_ball_comp, Set.Mem, Set.iInter, setOf, Dynamics.dynEntourage, UniformSpace.ball, Dynamics.dynEntourage_comp_subset, Set.preimage
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst : U.IsSymm
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
exact dynEntourage_comp_subset T U U n (mem_ball_comp z_By z_Bx)

Premises used: UniformSpace.mem_ball_comp, Dynamics.dynEntourage_comp_subset
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
rw : ⋂ (i : ℕ), ⋂ (_ : i < n), map φ φ ⁻¹' (map T T)^[i] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n
⊢ map φ φ ⁻¹' dynEntourage T U n = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
rw [dynEntourage, preimage_iInter₂]

Premises used: Dynamics.dynEntourage, Set.preimage_iInter₂