-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
theorem coverEntropyInf_image_of_comap (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y}
    (h : Semiconj φ S T) (F : Set X) :
    coverEntropyInf T (φ '' F) = @coverEntropyInf X (comap φ u) S F

Proof state:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
rcases U_uni with ⟨V, V_uni, V_sub⟩

Result:
case a.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Proof state:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
⊢ coverEntropyInf T (φ '' F) = coverEntropyInf S F

Tactic:
apply le_antisymm

Result:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)

Proof state:
case a.h
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ Prod.map φ φ ⁻¹' V

Tactic:
exact ⟨V, V_uni, Subset.rfl⟩

Result:
no goals

Proof state:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
simp only [uniformity_comap φ, mem_comap] at U_uni

Result:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Proof state:
case a.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SymmetricRel W
W_V : W ○ W ⊆ V
⊢ (fun U => coverEntropyInfEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropyInf T (φ '' F)

Tactic:
apply (le_coverEntropyInfEntourage_image h F W_symm).trans

Result:
case a.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SymmetricRel W
W_V : W ○ W ⊆ V
⊢ coverEntropyInfEntourage T (φ '' F) W ≤ coverEntropyInf T (φ '' F)

Proof state:
case a.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
rcases comp_symm_mem_uniformity_sets V_uni with ⟨W, W_uni, W_symm, W_V⟩

Result:
case a.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SymmetricRel W
W_V : W ○ W ⊆ V
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Proof state:
case a.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SymmetricRel W
W_V : W ○ W ⊆ V
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
apply (coverEntropyInfEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans

Result:
case a.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SymmetricRel W
W_V : W ○ W ⊆ V
⊢ (fun U => coverEntropyInfEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropyInf T (φ '' F)

Proof state:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)

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

Result:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Proof state:
case a.h
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ Prod.map φ φ ⁻¹' V ∈ 𝓤 X

Tactic:
rw [uniformity_comap φ, mem_comap]

Result:
case a.h
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ Prod.map φ φ ⁻¹' V

Proof state:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' V) ≤ coverEntropyInf S F

Tactic:
apply @coverEntropyInfEntourage_le_coverEntropyInf X (comap φ u) S F

Result:
case a.h
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ Prod.map φ φ ⁻¹' V ∈ 𝓤 X

Proof state:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
refine iSup₂_le fun V V_uni ↦ (coverEntropyInfEntourage_image_le h F V).trans ?_

Result:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' V) ≤ coverEntropyInf S F

Proof state:
case a.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SymmetricRel W
W_V : W ○ W ⊆ V
⊢ coverEntropyInfEntourage T (φ '' F) W ≤ coverEntropyInf T (φ '' F)

Tactic:
exact coverEntropyInfEntourage_le_coverEntropyInf T (φ '' F) W_uni

Result:
no goals