awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inl :
  ∀
    (inter_empt :
      Eq.{u_1 + 1} (α := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) ∅),
    ∃ (y : X),
      ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
        ball y (dynEntourage T (U ○ U) (m * n))
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
have inr : ∀
  (inter_nemp :
    Set.Nonempty.{u_1} (α := X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m))),
  ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
Tactic: rcases (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)).eq_empty_or_nonempty
      with inter_empt | inter_nemp
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_nemp : Set.Nonempty.{u_1} (α := X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m))
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
have inr : ∀ (y : X)
  (y_int : Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) y),
  ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
Tactic: obtain ⟨y, y_int⟩ := inter_nemp
Cleared hypotheses: inter_nemp
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y : X
y_int : Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) y
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
have inr : ∀ (z : X)
  (z_int : Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) z),
  z ∈ ball y (dynEntourage T (U ○ U) (m * n))
Tactic: refine ⟨y, fun z z_int ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y : X
y_int : Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) y
z : X
z_int : Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) z
⊢ z ∈ ball y (dynEntourage T (U ○ U) (m * n))
have inr : ∀ (y_int : ∀ (i : Fin n) (i_1 : ℕ) (i_2 : i_1 < m), (T^[i_1] (↑(t i) : X), T^[i_1] (T^[m * (↑i : ℕ)] y)) ∈ U)
  (z_int : ∀ (i : Fin n) (i_1 : ℕ) (i_2 : i_1 < m), (T^[i_1] (↑(t i) : X), T^[i_1] (T^[m * (↑i : ℕ)] z)) ∈ U) (i : ℕ)
  (i_1 : i < m * n), ∃ (b : X), (T^[i] y, b) ∈ U ∧ (b, T^[i] z) ∈ U
Tactic: simp only [ball, dynEntourage, Prod.map_iterate, mem_iInter, Set.mem_preimage, Prod.map_apply,
        mem_comp] at y_int z_int ⊢
Cleared hypotheses: y_int, z_int
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
y_int : ∀ (i : Fin n) (i_1 : ℕ) (i_2 : i_1 < m), (T^[i_1] (↑(t i) : X), T^[i_1] (T^[m * (↑i : ℕ)] y)) ∈ U
z_int : ∀ (i : Fin n) (i_1 : ℕ) (i_2 : i_1 < m), (T^[i_1] (↑(t i) : X), T^[i_1] (T^[m * (↑i : ℕ)] z)) ∈ U
k : ℕ
k_mn : k < m * n
⊢ ∃ (b : X), (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
have k_mn₁ : k / m < n
Tactic: replace k_mn := Nat.div_lt_of_lt_mul k_mn
Cleared hypotheses: k_mn
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
y_int : ∀ (i : Fin n) (i_1 : ℕ) (i_2 : i_1 < m), (T^[i_1] (↑(t i) : X), T^[i_1] (T^[m * (↑i : ℕ)] y)) ∈ U
z_int : ∀ (i : Fin n) (i_1 : ℕ) (i_2 : i_1 < m), (T^[i_1] (↑(t i) : X), T^[i_1] (T^[m * (↑i : ℕ)] z)) ∈ U
k : ℕ
k_mn : k / m < n
⊢ ∃ (b : X), (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
have z_int₁ : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k % m] (T^[m * (↑(⟨k / m, k_mn⟩ : Fin n) : ℕ)] z)) ∈ U
Tactic: specialize z_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
Cleared hypotheses: z_int
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
y_int : ∀ (i : Fin n) (i_1 : ℕ) (i_2 : i_1 < m), (T^[i_1] (↑(t i) : X), T^[i_1] (T^[m * (↑i : ℕ)] y)) ∈ U
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k % m] (T^[m * (↑(⟨k / m, k_mn⟩ : Fin n) : ℕ)] z)) ∈ U
⊢ ∃ (b : X), (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
have y_int₁ : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k % m] (T^[m * (↑(⟨k / m, k_mn⟩ : Fin n) : ℕ)] y)) ∈ U
Tactic: specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
Cleared hypotheses: y_int
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k % m] (T^[m * (↑(⟨k / m, k_mn⟩ : Fin n) : ℕ)] z)) ∈ U
y_int : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k % m] (T^[m * (↑(⟨k / m, k_mn⟩ : Fin n) : ℕ)] y)) ∈ U
⊢ ∃ (b : X), (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
have z_int₁ : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k] z) ∈ U
Tactic: rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int
Cleared hypotheses: z_int, y_int
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y z : X
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k % m] (T^[m * (↑(⟨k / m, k_mn⟩ : Fin n) : ℕ)] z)) ∈ U
y_int : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k % m] (T^[m * (↑(⟨k / m, k_mn⟩ : Fin n) : ℕ)] y)) ∈ U
z_int₁ : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k] z) ∈ U
⊢ ∃ (b : X), (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
have y_int₁ : (T^[k % m] (↑(t (⟨k / m, k_mn⟩ : Fin n)) : X), T^[k] y) ∈ U
Tactic: rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int
Cleared hypotheses: z_int, y_int
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
have this : ∀ (t : Fin n → ↥s),
  ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
Tactic: have (t : Fin n → s) : ∃ y : X, (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)) ⊆
      ball y (dynEntourage T (U ○ U) (m * n)) := by
    rcases (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)).eq_empty_or_nonempty
      with inter_empt | inter_nemp
    · exact inter_empt ▸ ⟨x, empty_subset _⟩
    · obtain ⟨y, y_int⟩ := inter_nemp
      refine ⟨y, fun z z_int ↦ ?_⟩
      simp only [ball, dynEntourage, Prod.map_iterate, mem_iInter, Set.mem_preimage, Prod.map_apply,
        mem_comp] at y_int z_int ⊢
      intro k k_mn
      replace k_mn := Nat.div_lt_of_lt_mul k_mn
      specialize z_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int
      exact mem_comp_of_mem_ball y_int z_int
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
this :
  ∀ (t : Fin n → ↥s),
    ∃ (y : X),
      ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
        ball y (dynEntourage T (U ○ U) (m * n))
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
have inr : ∀ (dyncover : (t : Fin n → ↥s) → X)
  (h_dyncover :
    ∀ (t : Fin n → ↥s),
      ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
        ball (dyncover t) (dynEntourage T (U ○ U) (m * n))),
  ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
Tactic: choose! dyncover h_dyncover using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
have inr : IsDynCoverOf T F (U ○ U) (m * n) (↑sn.toFinset : Set X)
Tactic: refine ⟨sn.toFinset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
inr : IsDynCoverOf T F (U ○ U) (m * n) (↑sn.toFinset : Set X)
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
have inr₁ : #sn.toFinset ≤ #s ^ n
Tactic: refine ⟨sn.toFinset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ IsDynCoverOf T F (U ○ U) (m * n) (↑sn.toFinset : Set X)
have inr : ∀ (s_nemp : s.Nonempty) (x : X) (x_F : x ∈ F) (m_pos : m > 0) (dyncover : (t : Fin n → ↥s) → X)
  (h_dyncover :
    ∀ (t : Fin n → ↥s),
      ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
        ball (dyncover t) (dynEntourage T (U ○ U) (m * n))),
  let sn := range dyncover;
  IsDynCoverOf T F (U ○ U) (m * n) (↑sn.toFinset : Set X)
Tactic: rw [Finset.coe_nonempty] at s_nemp
Cleared hypotheses: s_nemp, x, x_F, m_pos, dyncover, h_dyncover, sn
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ IsDynCoverOf T F (U ○ U) (m * n) (↑sn.toFinset : Set X)
have x₁ : Nonempty.{u_1 + 1} ↥s
Tactic: have _ : Nonempty s := Finset.Nonempty.coe_sort s_nemp
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
h_2 : Nonempty.{u_1 + 1} ↥s
y : X
y_F : y ∈ F
k : Fin n
⊢ ∃ (z : ↥s), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑z : X) (dynEntourage T U m)
have this : ∃ y_1 ∈ (↑s : Set X), (T^[m * (↑k : ℕ)] y, y_1) ∈ dynEntourage T U m
Tactic: have := h (MapsTo.iterate F_inv (m * k) y_F)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
h_2 : Nonempty.{u_1 + 1} ↥s
y : X
y_F : y ∈ F
k : Fin n
this : ∃ y_1 ∈ (↑s : Set X), (T^[m * (↑k : ℕ)] y, y_1) ∈ dynEntourage T U m
⊢ ∃ (z : ↥s), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑z : X) (dynEntourage T U m)
have this₁ : ∃ y_1 ∈ s, (T^[m * (↑k : ℕ)] y, y_1) ∈ dynEntourage T U m
Tactic: simp only [Finset.mem_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
h_2 : Nonempty.{u_1 + 1} ↥s
y : X
y_F : y ∈ F
k : Fin n
this : ∃ y_1 ∈ s, (T^[m * (↑k : ℕ)] y, y_1) ∈ dynEntourage T U m
⊢ ∃ (z : ↥s), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑z : X) (dynEntourage T U m)
have obtain : ∀ (z : X) (z_s : z ∈ s) (hz : (T^[m * (↑k : ℕ)] y, z) ∈ dynEntourage T U m),
  ∃ (z : ↥s), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑z : X) (dynEntourage T U m)
Tactic: obtain ⟨z, z_s, hz⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
h_2 : Nonempty.{u_1 + 1} ↥s
y : X
y_F : y ∈ F
⊢ ∃ y_1 ∈ (↑sn.toFinset : Set X), (y, y_1) ∈ dynEntourage T (U ○ U) (m * n)
have key : ∀ (k : Fin n), ∃ (z : ↥s), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑z : X) (dynEntourage T U m)
Tactic: have key : ∀ k : Fin n, ∃ z : s, y ∈ T^[m * k] ⁻¹' ball z (dynEntourage T U m) := by
      intro k
      have := h (MapsTo.iterate F_inv (m * k) y_F)
      simp only [Finset.mem_coe] at this
      obtain ⟨z, z_s, hz⟩ := this
      exact ⟨⟨z, z_s⟩, (dynEntourage T U m).symm hz⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
h_2 : Nonempty.{u_1 + 1} ↥s
y : X
y_F : y ∈ F
key : ∀ (k : Fin n), ∃ (z : ↥s), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑z : X) (dynEntourage T U m)
⊢ ∃ y_1 ∈ (↑sn.toFinset : Set X), (y, y_1) ∈ dynEntourage T (U ○ U) (m * n)
have inr : ∀ (t : (k : Fin n) → ↥s) (ht : ∀ (k : Fin n), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)),
  ∃ y_1 ∈ (↑sn.toFinset : Set X), (y, y_1) ∈ dynEntourage T (U ○ U) (m * n)
Tactic: choose! t ht using key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
h_2 : Nonempty.{u_1 + 1} ↥s
y : X
y_F : y ∈ F
t : (k : Fin n) → ↥s
ht : ∀ (k : Fin n), y ∈ T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)
⊢ ∃ y_1 ∈ (↑sn.toFinset : Set X), (y, y_1) ∈ dynEntourage T (U ○ U) (m * n)
have inr : ∃ (a : Fin n → ↥s), (y, dyncover a) ∈ dynEntourage T (U ○ U) (m * n)
Tactic: simp only [toFinset_range, Finset.coe_image, Finset.coe_univ, image_univ, mem_range,
      exists_exists_eq_and, sn]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ #sn.toFinset ≤ #s ^ n
have inr : Fintype.card.{u_1} (↑sn : Type u_1) ≤ #s ^ n
Tactic: rw [toFinset_card]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (t : Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
      ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ Fintype.card.{u_1} (↑sn : Type u_1) ≤ #s ^ n
have inr : Fintype.card.{u_1} (Fin n → ↥s) ≤ #s ^ n
Tactic: apply (Fintype.card_range_le dyncover).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have obtain : ∀ (V : SetRel X X) (hV : V ∈ 𝓤 X) (hVsymm : V.IsSymm) (hVU : V ⊆ U), ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
Tactic: obtain ⟨(V : SetRel X X), hV, hVsymm, hVU⟩ := symm_of_uniformity U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
hV : V ∈ 𝓤 X
hVsymm : V.IsSymm
hVU : V ⊆ U
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have uni_ite : dynEntourage T V n ∈ 𝓤 X
Tactic: have uni_ite := dynEntourage_mem_uniformity h hV n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
hV : V ∈ 𝓤 X
hVsymm : V.IsSymm
hVU : V ⊆ U
uni_ite : dynEntourage T V n ∈ 𝓤 X
openCover : (x : X) → Set X := fun (x : X) ↦ ball x (dynEntourage T V n)
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have obtain : ∀ (s : Finset X),
  (∀ x ∈ s, x ∈ F) → ∀ (s_cover : F ⊆ ⋃ x ∈ s, openCover x), ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
Tactic: obtain ⟨s, _, s_cover⟩ := F_comp.elim_nhds_subcover openCover fun x _ ↦ ball_mem_nhds x uni_ite
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have obtain : ∀ (V : SetRel X X) (V_uni : V ∈ 𝓤 X) (V_symm : V.IsSymm) (V_U : V ○ V ⊆ U),
  ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
Tactic: obtain ⟨(V : SetRel X X), V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have obtain : ∀ (s : Finset X),
  (∀ x ∈ s, x ∈ F) → ∀ (s_cover : F ⊆ ⋃ x ∈ s, ball x V), ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
Tactic: obtain ⟨s, _, s_cover⟩ := F_comp.elim_nhds_subcover (ball · V)
    fun (x : X) _ ↦ ball_mem_nhds x V_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have this : IsDynCoverOf T F V 1 (↑s : Set X)
Tactic: have : IsDynCoverOf T F V 1 s := .of_subset_iUnion_ball <| by simpa using s_cover