-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma coverEntropy_eq_iSup_basis_netEntropyEntourage {ι : Sort*} {p : ι → Prop}
    {s : ι → Set (X × X)} (h : (𝓤 X).HasBasis p s) (T : X → X) (F : Set X) :
    coverEntropy T F = ⨆ (i : ι) (_ : p i), netEntropyEntourage 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
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ (fun U => netEntropyEntourage T F U) (s i) ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)

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

Result:
no goals

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
⊢ netEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage 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
⊢ netEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage 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, netEntropyEntourage T F U = ⨆ i, ⨆ (_ : p i), netEntropyEntourage 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, netEntropyEntourage T F i ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage 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, netEntropyEntourage T F i ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage 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
⊢ netEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage 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
⊢ coverEntropy T F = ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
rw [coverEntropy_eq_iSup_netEntropyEntourage 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, netEntropyEntourage T F U = ⨆ i, ⨆ (_ : p i), netEntropyEntourage 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
⊢ netEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
apply (netEntropyEntourage_antitone T F si_U).trans _

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
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ (fun U => netEntropyEntourage T F U) (s i) ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)