-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyEntourage_finite_of_isCompact_invariant [UniformSpace X] {T : X → X} {F : Set X}
    (F_comp : IsCompact F) (F_inv : MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) :
    coverEntropyEntourage T F U < ⊤

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ coverEntropyEntourage T F U < ⊤

Tactic:
apply (coverEntropyEntourage_antitone T F V_U).trans_lt

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ (fun U => coverEntropyEntourage T F U) (V ○ V) < ⊤

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ ↑s.card < ↑⊤

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

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ (fun U => coverEntropyEntourage T F U) (V ○ V) < ⊤

Tactic:
apply (s_cover.coverEntropyEntourage_le_log_card_div F_inv V_symm zero_lt_one).trans_lt

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ (↑s.card).log / ↑1 < ⊤

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U < ⊤

Tactic:
rcases comp_symm_mem_uniformity_sets U_uni with ⟨V, V_uni, V_symm, V_U⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U < ⊤

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ (↑s.card).log / ↑1 < ⊤

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

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ ↑s.card < ↑⊤

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U < ⊤

Tactic:
rcases exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv V_uni 1 with ⟨s, s_cover⟩

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
s_cover : IsDynCoverOf T F V 1 ↑s
⊢ coverEntropyEntourage T F U < ⊤