awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ 0 ≤ coverEntropyEntourage T F U

Tactic:
(coverEntropyInfEntourage_nonneg T h U).trans
    (coverEntropyInfEntourage_le_coverEntropyEntourage T F U)

Premises used: Dynamics.coverEntropyInfEntourage_le_coverEntropyEntourage, LE.le.trans, Dynamics.coverEntropyInfEntourage_nonneg
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
rw : (expGrowthSup fun (n : ℕ) ↦ (↑(coverMincard T F univ n) : ℝ≥0∞)) = expGrowthSup fun (x : ℕ) ↦ 1
⊢ coverEntropyEntourage T F univ = 0

Tactic:
rw [← expGrowthSup_const one_ne_zero one_ne_top, coverEntropyEntourage]

Premises used: ExpGrowth.expGrowthSup_const, Dynamics.coverEntropyEntourage, one_ne_zero, ENNReal.one_ne_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑(coverMincard T F univ n) : ℝ≥0∞)) = expGrowthSup fun (x : ℕ) ↦ 1

Tactic:
simp only [coverMincard_univ T h, ENat.toENNReal_one]

Premises used: Dynamics.coverMincard_univ, ENat.toENNReal_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
rw : (expGrowthInf fun (n : ℕ) ↦ (↑(coverMincard T F univ n) : ℝ≥0∞)) = expGrowthInf fun (x : ℕ) ↦ 1
⊢ coverEntropyInfEntourage T F univ = 0

Tactic:
rw [← expGrowthInf_const one_ne_zero one_ne_top, coverEntropyInfEntourage]

Premises used: ExpGrowth.expGrowthInf_const, Dynamics.coverEntropyInfEntourage, one_ne_zero, ENNReal.one_ne_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ (expGrowthInf fun (n : ℕ) ↦ (↑(coverMincard T F univ n) : ℝ≥0∞)) = expGrowthInf fun (x : ℕ) ↦ 1

Tactic:
simp only [coverMincard_univ T h, ENat.toENNReal_one]

Premises used: Dynamics.coverMincard_univ, ENat.toENNReal_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
⊢ Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)

Tactic:
have cv_mono : Monotone fun m ↦ (coverMincard T F (U ○ U) m).toENNReal :=
    fun _ _ k_m ↦ ENat.toENNReal_mono (coverMincard_monotone_time T F (U ○ U) k_m)
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
⊢ (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) =
    (↑n : EReal) * expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)

Tactic:
have h := cv_mono.expGrowthSup_comp_mul n_pos
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) =
    (↑n : EReal) * expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
⊢ (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)

Tactic:
rw [mul_comm, ← div_eq_iff (natCast_ne_bot n) (natCast_ne_top n) (Nat.cast_ne_zero.2 n_pos)] at h

Premises used: Iff.mpr, mul_comm, EReal.natCast_ne_top, EReal.div_eq_iff, EReal.natCast_ne_bot, Nat.cast_ne_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
rw :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) ≤
    (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)

Tactic:
rw [coverEntropyEntourage, ← h]

Premises used: Dynamics.coverEntropyEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
a : (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log
⊢ (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) ≤
    (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)

Tactic:
apply monotone_div_right_of_nonneg n.cast_nonneg'

Premises used: Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
a :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) ≤
    expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞) ^ n_1
⊢ (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log

Tactic:
rw [← expGrowthSup_pow]

Premises used: ExpGrowth.expGrowthSup_pow
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
⊢ (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) ≤
    expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞) ^ n_1

Tactic:
expGrowthSup_monotone fun m ↦ ?_

Premises used: ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
a : ∀ (m : ℕ), (↑(coverMincard T F (U ○ U) (n * m)) : ℝ≥0∞) ≤ (↑(coverMincard T F U n) : ℝ≥0∞) ^ m
⊢ (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) ≤
    expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞) ^ n_1

Tactic:
refine expGrowthSup_monotone fun m ↦ ?_

Premises used: ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
m : ℕ
a : (↑(coverMincard T F (U ○ U) (n * m)) : ℝ≥0∞) ≤ (↑(coverMincard T F U n ^ m) : ℝ≥0∞)
⊢ (↑(coverMincard T F (U ○ U) (n * m)) : ℝ≥0∞) ≤ (↑(coverMincard T F U n) : ℝ≥0∞) ^ m

Tactic:
rw [← ENat.toENNReal_pow]

Premises used: ENat.toENNReal_pow
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
m : ℕ
⊢ (↑(coverMincard T F (U ○ U) (n * m)) : ℝ≥0∞) ≤ (↑(coverMincard T F U n ^ m) : ℝ≥0∞)

Tactic:
ENat.toENNReal_mono (coverMincard_mul_le_pow F_inv n m)

Premises used: ENat.toENNReal_mono, Dynamics.coverMincard_mul_le_pow
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone (β := ℝ≥0∞) fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
h :
  (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) / (↑n : EReal) =
    expGrowthSup fun (m : ℕ) ↦ (↑(coverMincard T F (U ○ U) m) : ℝ≥0∞)
m : ℕ
⊢ (↑(coverMincard T F (U ○ U) (n * m)) : ℝ≥0∞) ≤ (↑(coverMincard T F U n ^ m) : ℝ≥0∞)

Tactic:
exact ENat.toENNReal_mono (coverMincard_mul_le_pow F_inv n m)

Premises used: ENat.toENNReal_mono, Dynamics.coverMincard_mul_le_pow
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
apply : (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal) ≤ log (↑(#s) : ℝ≥0∞) / (↑n : EReal)
⊢ coverEntropyEntourage T F (U ○ U) ≤ log (↑(#s) : ℝ≥0∞) / (↑n : EReal)

Tactic:
apply (coverEntropyEntourage_le_log_coverMincard_div F_inv n_pos).trans

Premises used: Dynamics.coverEntropyEntourage_le_log_coverMincard_div, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
apply : (↑(coverMincard T F U n) : ℝ≥0∞) ≤ (↑(#s) : ℝ≥0∞)
⊢ (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal) ≤ log (↑(#s) : ℝ≥0∞) / (↑n : EReal)

Tactic:
apply monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone _)

Premises used: ENNReal.log_monotone, Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
⊢ (↑(coverMincard T F U n) : ℝ≥0∞) ≤ (↑(#s) : ℝ≥0∞)

Tactic:
exact_mod_cast coverMincard_le_card h

Premises used: Dynamics.IsDynCoverOf.coverMincard_le_card
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
⊢ coverEntropyEntourage T F (U ○ U) ≤ coverEntropyInfEntourage T F U

Tactic:
(le_liminf_of_le) (eventually_atTop.2 ⟨1, fun m m_pos ↦ ?_⟩)

Premises used: Iff.mpr, ExpGrowth.expGrowthInf, Exists.intro, Dynamics.coverEntropyInfEntourage, Filter.eventually_atTop, OfNat.ofNat, Filter.le_liminf_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
refine :
  ∀ (m : ℕ) (m_pos : m ≥ 1),
    coverEntropyEntourage T F (U ○ U) ≤ log ((fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) m) / (↑m : EReal)
⊢ coverEntropyEntourage T F (U ○ U) ≤ coverEntropyInfEntourage T F U

Tactic:
refine (le_liminf_of_le) (eventually_atTop.2 ⟨1, fun m m_pos ↦ ?_⟩)

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat, Filter.le_liminf_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m : ℕ
m_pos : m ≥ 1
⊢ coverEntropyEntourage T F (U ○ U) ≤ log ((fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) m) / (↑m : EReal)

Tactic:
coverEntropyEntourage_le_log_coverMincard_div F_inv (Nat.one_le_iff_ne_zero.1 m_pos)

Premises used: Dynamics.coverEntropyEntourage_le_log_coverMincard_div, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m : ℕ
m_pos : m ≥ 1
⊢ coverEntropyEntourage T F (U ○ U) ≤ log ((fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) m) / (↑m : EReal)

Tactic:
exact coverEntropyEntourage_le_log_coverMincard_div F_inv (Nat.one_le_iff_ne_zero.1 m_pos)

Premises used: Dynamics.coverEntropyEntourage_le_log_coverMincard_div, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
obtain :
  ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_symm : SetRel.IsSymm V) (V_U : V ○ V ⊆ U), coverEntropyEntourage T F U < ⊤
⊢ coverEntropyEntourage T F U < ⊤

Tactic:
obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
obtain : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F V 1 (↑s : Set X)), coverEntropyEntourage T F U < ⊤
⊢ coverEntropyEntourage T F U < ⊤

Tactic:
obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv V_uni 1

Premises used: OfNat.ofNat, Dynamics.exists_isDynCoverOf_of_isCompact_invariant
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 (↑s : Set X)
apply : LT.lt (α := EReal) ((fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V)) ⊤
⊢ coverEntropyEntourage T F U < ⊤

Tactic:
apply (coverEntropyEntourage_antitone T F V_U).trans_lt

Premises used: Dynamics.coverEntropyEntourage_antitone, LE.le.trans_lt
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 (↑s : Set X)
apply : log (↑(#s) : ℝ≥0∞) / (↑1 : EReal) < ⊤
⊢ LT.lt (α := EReal) ((fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V)) ⊤

Tactic:
apply (s_cover.coverEntropyEntourage_le_log_card_div F_inv one_ne_zero).trans_lt

Premises used: Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div, one_ne_zero, LE.le.trans_lt
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 (↑s : Set X)
rw : (↑(#s) : ℝ≥0∞) < (↑⊤ : ℝ≥0∞)
⊢ log (↑(#s) : ℝ≥0∞) / (↑1 : EReal) < ⊤

Tactic:
rw [Nat.cast_one, div_one, log_lt_top_iff, ← ENat.toENNReal_top]

Premises used: ENat.toENNReal_top, ENNReal.log_lt_top_iff, div_one, Nat.cast_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 (↑s : Set X)
⊢ (↑(#s) : ℝ≥0∞) < (↑⊤ : ℝ≥0∞)

Tactic:
exact_mod_cast (ENat.coe_ne_top (Finset.card s)).lt_top

Premises used: Ne.lt_top, Finset.card, ENat.coe_ne_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
⊢ Antitone (β := EReal) fun (u : UniformSpace X) ↦ coverEntropyInf T F

Tactic:
fun _ _ h ↦ iSup₂_mono' fun U U_uni ↦ ⟨U, (le_def.1 h) U U_uni, le_refl _⟩

Premises used: le_refl, Dynamics.coverEntropyInf, iSup₂_mono', Antitone, Exists.intro, Iff.mp, Dynamics.coverEntropyInfEntourage, Filter.le_def
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
⊢ Antitone (β := EReal) fun (u : UniformSpace X) ↦ coverEntropy T F

Tactic:
fun _ _ h ↦ iSup₂_mono' fun U U_uni ↦ ⟨U, (le_def.1 h) U U_uni, le_refl _⟩

Premises used: le_refl, iSup₂_mono', Antitone, Exists.intro, Iff.mp, Dynamics.coverEntropy, Dynamics.coverEntropyEntourage, Filter.le_def
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
U : SetRel X X
inst : UniformSpace X
T : X → X
F : Set X
h : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
le_iSup₂ (f := fun (U : SetRel X X) (_ : U ∈ 𝓤 X) ↦ coverEntropyEntourage T F U) U h

Premises used: le_iSup₂, Dynamics.coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
U : SetRel X X
inst : UniformSpace X
T : X → X
F : Set X
h : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T F U ≤ coverEntropyInf T F

Tactic:
le_iSup₂ (f := fun (U : SetRel X X) (_ : U ∈ 𝓤 X) ↦ coverEntropyInfEntourage T F U) U h

Premises used: le_iSup₂, Dynamics.coverEntropyInf
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropy T F = ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
(iSup₂_le fun U U_uni ↦ ?_).antisymm
    (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)

Premises used: iSup₂_le, le_refl, LE.le.antisymm, iSup₂_mono', Exists.intro, Dynamics.coverEntropy, Dynamics.coverEntropyEntourage, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
refine :
  ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X),
    coverEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)
⊢ coverEntropy T F = ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm
    (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)

Premises used: iSup₂_le, le_refl, LE.le.antisymm, iSup₂_mono', Exists.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
obtain :
  ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
    coverEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)
⊢ coverEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
(coverEntropyEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyEntourage T F (s i)) i h_i)

Premises used: le_iSup₂, Dynamics.coverEntropyEntourage_antitone, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
exact (coverEntropyEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyEntourage T F (s i)) i h_i)

Premises used: le_iSup₂, Dynamics.coverEntropyEntourage_antitone, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
(iSup₂_le fun U U_uni ↦ ?_).antisymm
    (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)

Premises used: iSup₂_le, le_refl, LE.le.antisymm, Dynamics.coverEntropyInf, iSup₂_mono', Exists.intro, Dynamics.coverEntropyInfEntourage, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
refine :
  ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X),
    coverEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)
⊢ coverEntropyInf T F = ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm
    (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)

Premises used: iSup₂_le, le_refl, LE.le.antisymm, iSup₂_mono', Exists.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
obtain :
  ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
    coverEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)
⊢ coverEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
(coverEntropyInfEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyInfEntourage T F (s i)) i h_i)

Premises used: Dynamics.coverEntropyInfEntourage_antitone, le_iSup₂, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
exact (coverEntropyInfEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyInfEntourage T F (s i)) i h_i)

Premises used: Dynamics.coverEntropyInfEntourage_antitone, le_iSup₂, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropyInf T F ≤ coverEntropy T F

Tactic:
iSup₂_mono fun (U : SetRel X X) (_ : U ∈ 𝓤 X) ↦
    coverEntropyInfEntourage_le_coverEntropyEntourage T F U

Premises used: iSup₂_mono, Dynamics.coverEntropyInfEntourage_le_coverEntropyEntourage, Dynamics.coverEntropyInf, Dynamics.coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
inst : UniformSpace X
⊢ coverEntropy T ∅ = ⊥

Tactic:
simp only [coverEntropy, coverEntropyEntourage_empty, iSup_bot]

Premises used: Dynamics.coverEntropy, Dynamics.coverEntropyEntourage_empty, iSup_bot