-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage {ι : Sort*} {p : ι → Prop}
    {s : ι → Set (X × X)} (h : (𝓤 X).HasBasis p s) (T : X → X) (F : Set X) :
    coverEntropyInf T F = ⨆ (i : ι) (_ : p i), netEntropyInfEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
rw [coverEntropyInf_eq_iSup_netEntropyInfEntourage T F]

Result:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U = ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U = ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

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

Result:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ ⨆ i ∈ 𝓤 X, netEntropyInfEntourage T F i ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

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

Result:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (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
⊢ netEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Proof state:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (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
⊢ netEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
apply (netEntropyInfEntourage_antitone T F si_U).trans

Result:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (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
⊢ (fun U => netEntropyInfEntourage T F U) (s i) ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ ⨆ i ∈ 𝓤 X, netEntropyInfEntourage T F i ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
refine iSup₂_le fun U U_uni ↦ ?_

Result:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Proof state:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (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
⊢ (fun U => netEntropyInfEntourage T F U) (s i) ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyInfEntourage T F (s i)) i h_i

Result:
no goals