-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
lemma coverEntropy_image_le_of_uniformContinuousOn_invariant [UniformSpace X] [UniformSpace Y]
    {S : X → X} {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) {F G : Set X}
    (h' : UniformContinuousOn φ G) (hF : F ⊆ G) (hG : MapsTo S G G) :
    coverEntropy T (φ '' F) ≤ coverEntropy S F

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val ⁻¹' F)

Tactic:
have hφ : Semiconj (G.restrict φ) (hG.restrict S G G) T := by
  intro x
  rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val ⁻¹' F)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

Tactic:
rw [← coverEntropy_restrict_subset hF hG]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val ⁻¹' F)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' F) = coverEntropy T (G.restrict φ '' (val ⁻¹' F))

Tactic:
rw [← image_image_val_eq_restrict_image, image_preimage_coe G F, inter_eq_right.2 hF]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ G.restrict φ (MapsTo.restrict S G G hG x) = T (G.restrict φ x)

Tactic:
rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val ⁻¹' F)

Tactic:
apply (coverEntropy_image_le_of_uniformContinuous hφ
  (uniformContinuousOn_iff_restrict.1 h') (val ⁻¹' F)).trans_eq'

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' F) = coverEntropy T (G.restrict φ '' (val ⁻¹' F))

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ Semiconj (G.restrict φ) (MapsTo.restrict S G G hG) T

Tactic:
intro x

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ G.restrict φ (MapsTo.restrict S G G hG x) = T (G.restrict φ x)