-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
theorem coverEntropy_eq_iSup_netEntropyEntourage :
    coverEntropy T F = ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Proof state:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
apply (netEntropyEntourage_antitone T F (symmetrizeRel_subset_self U)).trans

Result:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun U => netEntropyEntourage T F U) (symmetrizeRel U) ≤ coverEntropy T F

Proof state:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun U => netEntropyEntourage T F U) (symmetrizeRel U) ≤ coverEntropy T F

Tactic:
apply (le_iSup₂ (symmetrizeRel U) (symmetrize_mem_uniformity U_uni)).trans'

Result:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun U => netEntropyEntourage T F U) (symmetrizeRel U) ≤ coverEntropyEntourage T F (symmetrizeRel U)

Proof state:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
rcases (comp_symm_mem_uniformity_sets U_uni) with ⟨V, V_uni, V_symm, V_comp_U⟩

Result:
case a.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_comp_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Proof state:
case a.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_comp_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
apply (coverEntropyEntourage_antitone T F V_comp_U).trans (le_iSup₂_of_le V V_uni _)

Result:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_comp_U : V ○ V ⊆ U
⊢ (fun U => coverEntropyEntourage T F U) (V ○ V) ≤ netEntropyEntourage T F V

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_comp_U : V ○ V ⊆ U
⊢ (fun U => coverEntropyEntourage T F U) (V ○ V) ≤ netEntropyEntourage T F V

Tactic:
exact coverEntropyEntourage_le_netEntropyEntourage T F (refl_le_uniformity V_uni) V_symm

Result:
no goals

Proof state:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun U => netEntropyEntourage T F U) (symmetrizeRel U) ≤ coverEntropyEntourage T F (symmetrizeRel U)

Tactic:
exact netEntropyEntourage_le_coverEntropyEntourage T F (symmetric_symmetrizeRel U)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropy T F = ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
apply le_antisymm <;> refine iSup₂_le fun U U_uni ↦ ?_

Result:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F