awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
⊢ False
have smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)
Tactic: have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)
⊢ False
have apply : (↑(#(s.erase x)) : ℕ∞) < coverMincard T F U n
Tactic: apply smaller_cover.coverMincard_le_card.not_gt
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)
⊢ (↑(#(s.erase x)) : ℕ∞) < coverMincard T F U n
have rw : LT.lt (α := ℕ∞) (↑(#(s.erase x)) : ℕ∞) (↑(#s) : ℕ∞)
Tactic: rw [← h']
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty
have by_contra! : (¬∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty) → False
Tactic: classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty) → False
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty
have by_contra!₄ : (∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅) → False
Tactic: classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ :
  (∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅) → False
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty
have by_contra!₁₀ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅), False
Tactic: classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ :
  (∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅) → False
by_contra!₁₀ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅), False
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty
have by_contra!₁₁ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
  (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), False
Tactic: classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ :
  (∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅) → False
by_contra!₁₀ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅), False
by_contra!₁₁ :
  ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
    (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), False
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty
have by_contra!₁₂ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
  (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), (↑(#(s.erase x)) : ℕ∞) < coverMincard T F U n
Tactic: classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s
-- 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
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ :
  (∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅) → False
by_contra!₁₀ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅), False
by_contra!₁₁ :
  ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
    (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), False
by_contra!₁₂ :
  ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
    (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), (↑(#(s.erase x)) : ℕ∞) < coverMincard T F U n
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty
have by_contra!₁₃ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
  (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), LT.lt (α := ℕ∞) (↑(#(s.erase x)) : ℕ∞) (↑(#s) : ℕ∞)
Tactic: classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ coverEntropyEntourage T ∅ U = ⊥
have simp : (expGrowthSup fun (n : ℕ) ↦ (↑0 : ℝ≥0∞)) = ⊥
Tactic: simp only [coverEntropyEntourage, coverMincard_empty]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑0 : ℝ≥0∞)) = ⊥
have rw : (expGrowthSup fun (n : ℕ) ↦ 0) = ⊥
Tactic: rw [ENat.toENNReal_zero, ← Pi.zero_def, expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
rw : (expGrowthSup fun (n : ℕ) ↦ 0) = ⊥
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑0 : ℝ≥0∞)) = ⊥
have rw₁ : expGrowthSup 0 = ⊥
Tactic: rw [ENat.toENNReal_zero, ← Pi.zero_def, expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
rw : (expGrowthSup fun (n : ℕ) ↦ 0) = ⊥
rw₁ : expGrowthSup 0 = ⊥
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑0 : ℝ≥0∞)) = ⊥
have rw₂ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [ENat.toENNReal_zero, ← Pi.zero_def, expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ 0 ≤ coverEntropyInfEntourage T F U
have h₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)
Tactic: apply Monotone.expGrowthInf_nonneg
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)
⊢ 0 ≤ coverEntropyInfEntourage T F U
have h' : Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) 0
Tactic: apply Monotone.expGrowthInf_nonneg
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) 0
have h' : ∃ (x : ℕ), ¬(↑(coverMincard T F U x) : ℝ≥0∞) = 0 x
Tactic: rw [ne_eq, funext_iff.not, not_forall]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ∃ (x : ℕ), ¬(↑(coverMincard T F U x) : ℝ≥0∞) = 0 x
have h₁ : ¬(↑(coverMincard T F U 0) : ℝ≥0∞) = 0 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬(↑(coverMincard T F U 0) : ℝ≥0∞) = 0 0
have h₁ : ¬Eq (α := ℝ≥0∞) 1 0
Tactic: rw [coverMincard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyEntourage T F univ = 0
have rw : (expGrowthSup fun (n : ℕ) ↦ (↑(coverMincard T F univ n) : ℝ≥0∞)) = expGrowthSup fun (x : ℕ) ↦ 1
Tactic: rw [← expGrowthSup_const one_ne_zero one_ne_top, coverEntropyEntourage]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyInfEntourage T F univ = 0
have rw : (expGrowthInf fun (n : ℕ) ↦ (↑(coverMincard T F univ n) : ℝ≥0∞)) = expGrowthInf fun (x : ℕ) ↦ 1
Tactic: rw [← expGrowthInf_const one_ne_zero one_ne_top, coverEntropyInfEntourage]
-- 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
n : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n_pos : n ≠ 0
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)
have cv_mono : 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)
-- 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
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∞)
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)
have 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∞)
Tactic: have h := cv_mono.expGrowthSup_comp_mul n_pos
-- 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
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∞)
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)
have 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∞)
Tactic: rw [mul_comm, ← div_eq_iff (natCast_ne_bot n) (natCast_ne_top n) (Nat.cast_ne_zero.2 n_pos)] at h
Cleared hypotheses: h
-- 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
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∞)
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)
have 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)
Tactic: rw [coverEntropyEntourage, ← h]
-- 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
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) ≤
    (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal)
have a : (expGrowthSup fun (n_1 : ℕ) ↦ (↑(coverMincard T F (U ○ U) (n * n_1)) : ℝ≥0∞)) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log
Tactic: apply monotone_div_right_of_nonneg n.cast_nonneg'
-- 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
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∞)) ≤ (↑(coverMincard T F U n) : ℝ≥0∞).log
have 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
Tactic: rw [← expGrowthSup_pow]
-- 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
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
have a : ∀ (m : ℕ), (↑(coverMincard T F (U ○ U) (n * m)) : ℝ≥0∞) ≤ (↑(coverMincard T F U n) : ℝ≥0∞) ^ m
Tactic: refine expGrowthSup_monotone fun m ↦ ?_
-- 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
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) : ℝ≥0∞) ^ m
have a : (↑(coverMincard T F (U ○ U) (n * m)) : ℝ≥0∞) ≤ (↑(coverMincard T F U n ^ m) : ℝ≥0∞)
Tactic: rw [← ENat.toENNReal_pow]
-- 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
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)
⊢ coverEntropyEntourage T F (U ○ U) ≤ log (↑(#s) : ℝ≥0∞) / (↑n : EReal)
have apply : (↑(coverMincard T F U n) : ℝ≥0∞).log / (↑n : EReal) ≤ log (↑(#s) : ℝ≥0∞) / (↑n : EReal)
Tactic: apply (coverEntropyEntourage_le_log_coverMincard_div F_inv n_pos).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
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∞).log / (↑n : EReal) ≤ log (↑(#s) : ℝ≥0∞) / (↑n : EReal)
have apply : (↑(coverMincard T F U n) : ℝ≥0∞) ≤ (↑(#s) : ℝ≥0∞)
Tactic: apply monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone _)
-- 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
F_inv : MapsTo T F F
inst : U.IsSymm
⊢ coverEntropyEntourage T F (U ○ U) ≤ coverEntropyInfEntourage T F U
have refine : ∀ (m : ℕ) (m_pos : m ≥ 1),
  coverEntropyEntourage T F (U ○ U) ≤ log ((fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) m) / (↑m : EReal)
Tactic: refine (le_liminf_of_le) (eventually_atTop.2 ⟨1, fun m m_pos ↦ ?_⟩)
-- 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
⊢ coverEntropyEntourage T F U < ⊤
have obtain : ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_symm : SetRel.IsSymm V) (V_U : V ○ V ⊆ U), coverEntropyEntourage T F U < ⊤
Tactic: obtain ⟨V, 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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U < ⊤
have obtain : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F V 1 (↑s : Set X)), coverEntropyEntourage T F U < ⊤
Tactic: obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv V_uni 1
-- 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
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)
⊢ coverEntropyEntourage T F U < ⊤
have apply : LT.lt (α := EReal) ((fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V)) ⊤
Tactic: apply (coverEntropyEntourage_antitone T F V_U).trans_lt
-- 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
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)
⊢ LT.lt (α := EReal) ((fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V)) ⊤
have apply : log (↑(#s) : ℝ≥0∞) / (↑1 : EReal) < ⊤
Tactic: apply (s_cover.coverEntropyEntourage_le_log_card_div F_inv one_ne_zero).trans_lt
-- 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
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)
⊢ log (↑(#s) : ℝ≥0∞) / (↑1 : EReal) < ⊤
have rw : (↑(#s) : ℝ≥0∞) < (↑⊤ : ℝ≥0∞)
Tactic: rw [Nat.cast_one, div_one, log_lt_top_iff, ← ENat.toENNReal_top]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
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)
have refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X),
  coverEntropyEntourage T F U ≤ ⨆ (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 _⟩)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
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
⊢ coverEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyEntourage T F (s i)
have obtain : ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
  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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
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)
have refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X),
  coverEntropyInfEntourage T F U ≤ ⨆ (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 _⟩)