-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
theorem coverEntropyInf_eq_iSup_netEntropyInfEntourage :
    coverEntropyInf T F = ⨆ U ∈ 𝓤 X, netEntropyInfEntourage 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
⊢ netEntropyInfEntourage T F U ≤ coverEntropyInf T F

Tactic:
apply (netEntropyInfEntourage_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 => netEntropyInfEntourage T F U) (symmetrizeRel U) ≤ coverEntropyInf 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 => netEntropyInfEntourage T F U) (symmetrizeRel U) ≤ coverEntropyInfEntourage T F (symmetrizeRel U)

Tactic:
exact netEntropyInfEntourage_le_coverEntropyInfEntourage T F (symmetric_symmetrizeRel U)

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 => netEntropyInfEntourage T F U) (symmetrizeRel U) ≤ coverEntropyInf 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 => netEntropyInfEntourage T F U) (symmetrizeRel U) ≤ coverEntropyInfEntourage T F (symmetrizeRel U)

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 => coverEntropyInfEntourage T F U) (V ○ V) ≤ netEntropyInfEntourage T F V

Tactic:
exact coverEntropyInfEntourage_le_netEntropyInfEntourage T F (refl_le_uniformity V_uni) V_symm

Result:
no goals

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
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

Tactic:
apply (coverEntropyInfEntourage_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 => coverEntropyInfEntourage T F U) (V ○ V) ≤ netEntropyInfEntourage T F V

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
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage 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
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ U ∈ 𝓤 X, netEntropyInfEntourage 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
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage 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
⊢ netEntropyInfEntourage T F U ≤ coverEntropyInf T F