awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n (↑(Finset.image φ s) : Set Y)
⊢ coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)

Tactic:
this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)

Premises used: Iff.mpr, Dynamics.IsDynCoverOf.coverMincard_le_card, Finset.card_image_le, LE.le.trans, WithTop.coe_le_coe
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n (↑(Finset.image φ s) : Set Y)
⊢ coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)

Tactic:
exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)

Premises used: Iff.mpr, Dynamics.IsDynCoverOf.coverMincard_le_card, Finset.card_image_le, LE.le.trans, WithTop.coe_le_coe
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr inr₁ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr₂ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n),
    coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr₃ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n), coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
inr₄ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n)
    (this : IsDynCoverOf T (φ '' F) V n (φ '' (↑s : Set X))), coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
inr₅ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n)
    (this : IsDynCoverOf T (φ '' F) V n (↑(Finset.image φ s) : Set Y)), coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)

Premises used: Prod.map, Set.preimage, Dynamics.coverMincard, eq_top_or_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst : V.IsSymm
⊢ coverEntropyEntourage S F (Prod.map φ φ ⁻¹' (V ○ V)) ≤ coverEntropyEntourage T (φ '' F) V

Tactic:
expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (le_coverMincard_image h F n)

Premises used: ENat.toENNReal_mono, Dynamics.coverEntropyEntourage, ExpGrowth.expGrowthSup_monotone, Dynamics.le_coverMincard_image
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst : V.IsSymm
⊢ coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' (V ○ V)) ≤ coverEntropyInfEntourage T (φ '' F) V

Tactic:
expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (le_coverMincard_image h F n)

Premises used: ExpGrowth.expGrowthInf_monotone, ENat.toENNReal_mono, Dynamics.coverEntropyInfEntourage, Dynamics.le_coverMincard_image
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
⊢ coverEntropyEntourage T (φ '' F) V ≤ coverEntropyEntourage S F (Prod.map φ φ ⁻¹' V)

Tactic:
expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_image_le h F V n)

Premises used: Dynamics.coverMincard_image_le, ENat.toENNReal_mono, Dynamics.coverEntropyEntourage, ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
⊢ coverEntropyInfEntourage T (φ '' F) V ≤ coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' V)

Tactic:
expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_image_le h F V n)

Premises used: Dynamics.coverMincard_image_le, ExpGrowth.expGrowthInf_monotone, ENat.toENNReal_mono, Dynamics.coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
a : coverEntropy T (φ '' F) ≤ coverEntropy S F
a₁ : coverEntropy S F ≤ coverEntropy T (φ '' F)
⊢ coverEntropy T (φ '' F) = coverEntropy S F

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

Tactic:
iSup₂_le fun V V_uni ↦
      (coverEntropyEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyEntourage_image_le h F _).trans ?_

Premises used: iSup₂_le, SetRel.symmetrize, Dynamics.coverEntropyEntourage_image_le, Dynamics.coverEntropyEntourage_antitone, SetRel.symmetrize_subset_self, Dynamics.coverEntropy, Set.image, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
a :
  ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y),
    coverEntropyEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropy S F
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

Tactic:
refine iSup₂_le fun V V_uni ↦
      (coverEntropyEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyEntourage_image_le h F _).trans ?_

Premises used: iSup₂_le, SetRel.symmetrize, Dynamics.coverEntropyEntourage_image_le, Dynamics.coverEntropyEntourage_antitone, SetRel.symmetrize_subset_self, Set.image, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
a : Prod.map φ φ ⁻¹' SetRel.symmetrize V ∈ 𝓤 X
⊢ coverEntropyEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropy S F

Tactic:
apply coverEntropyEntourage_le_coverEntropy

Premises used: Dynamics.coverEntropyEntourage_le_coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ Prod.map φ φ ⁻¹' SetRel.symmetrize V

Tactic:
⟨_, symmetrize_mem_uniformity V_uni, .rfl⟩

Premises used: symmetrize_mem_uniformity, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ Prod.map φ φ ⁻¹' SetRel.symmetrize V

Tactic:
exact ⟨_, symmetrize_mem_uniformity V_uni, .rfl⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropy S F ≤ coverEntropy T (φ '' F)

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le, Dynamics.coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
⊢ coverEntropy S F ≤ coverEntropy T (φ '' F)

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U

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

Premises used: Filter.mem_comap, uniformity_comap
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
a :
  ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y) (V_sub : Prod.map φ φ ⁻¹' V ⊆ U),
    coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)

Tactic:
obtain ⟨V, V_uni, V_sub⟩ := U_uni
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
a :
  ∀ (W : Set (Y × Y)) (W_uni : W ∈ 𝓤 Y) (W_symm : SetRel.IsSymm W) (W_V : W ○ W ⊆ V),
    coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)

Tactic:
obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
a : (fun (U : SetRel X X) ↦ coverEntropyEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropy T (φ '' F)
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)

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

Premises used: HasSubset.Subset.trans, Set.preimage_mono, Dynamics.coverEntropyEntourage_antitone, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
a : coverEntropyEntourage T (φ '' F) W ≤ coverEntropy T (φ '' F)
⊢ (fun (U : SetRel X X) ↦ coverEntropyEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropy T (φ '' F)

Tactic:
apply (le_coverEntropyEntourage_image h F).trans

Premises used: Dynamics.le_coverEntropyEntourage_image, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ coverEntropyEntourage T (φ '' F) W ≤ coverEntropy T (φ '' F)

Tactic:
coverEntropyEntourage_le_coverEntropy T (φ '' F) W_uni

Premises used: Set.image, Dynamics.coverEntropyEntourage_le_coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ coverEntropyEntourage T (φ '' F) W ≤ coverEntropy T (φ '' F)

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

Premises used: Set.image, Dynamics.coverEntropyEntourage_le_coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
a : coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F
a₁ : coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)
⊢ coverEntropyInf T (φ '' F) = coverEntropyInf S F

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
iSup₂_le fun V V_uni ↦
      (coverEntropyInfEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyInfEntourage_image_le h F _).trans ?_

Premises used: Dynamics.coverEntropyInfEntourage_antitone, iSup₂_le, SetRel.symmetrize, Dynamics.coverEntropyInf, Dynamics.coverEntropyInfEntourage_image_le, SetRel.symmetrize_subset_self, Set.image, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
a :
  ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y),
    coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropyInf S F
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
refine iSup₂_le fun V V_uni ↦
      (coverEntropyInfEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyInfEntourage_image_le h F _).trans ?_

Premises used: Dynamics.coverEntropyInfEntourage_antitone, iSup₂_le, SetRel.symmetrize, Dynamics.coverEntropyInfEntourage_image_le, SetRel.symmetrize_subset_self, Set.image, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
a : Prod.map φ φ ⁻¹' SetRel.symmetrize V ∈ 𝓤 X
⊢ coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropyInf S F

Tactic:
apply coverEntropyInfEntourage_le_coverEntropyInf

Premises used: Dynamics.coverEntropyInfEntourage_le_coverEntropyInf
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le, Dynamics.coverEntropyInf
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
⊢ coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
a :
  ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y) (V_sub : Prod.map φ φ ⁻¹' V ⊆ U),
    coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
obtain ⟨V, V_uni, V_sub⟩ := U_uni
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
a :
  ∀ (W : Set (Y × Y)) (W_uni : W ∈ 𝓤 Y) (W_symm : SetRel.IsSymm W) (W_V : W ○ W ⊆ V),
    coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
a : (fun (U : SetRel X X) ↦ coverEntropyInfEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropyInf T (φ '' F)
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

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

Premises used: Dynamics.coverEntropyInfEntourage_antitone, HasSubset.Subset.trans, Set.preimage_mono, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
a : coverEntropyInfEntourage T (φ '' F) W ≤ coverEntropyInf T (φ '' F)
⊢ (fun (U : SetRel X X) ↦ coverEntropyInfEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropyInf T (φ '' F)

Tactic:
apply (le_coverEntropyInfEntourage_image h F).trans

Premises used: LE.le.trans, Dynamics.le_coverEntropyInfEntourage_image
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ coverEntropyInfEntourage T (φ '' F) W ≤ coverEntropyInf T (φ '' F)

Tactic:
coverEntropyInfEntourage_le_coverEntropyInf T (φ '' F) W_uni

Premises used: Dynamics.coverEntropyInfEntourage_le_coverEntropyInf, Set.image
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
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
this : UniformSpace X := UniformSpace.comap φ u
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 : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ coverEntropyInfEntourage T (φ '' F) W ≤ coverEntropyInf T (φ '' F)

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

Premises used: Dynamics.coverEntropyInfEntourage_le_coverEntropyInf, Set.image
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
rw :
  coverEntropy T
      (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropy T F
rw₁ : coverEntropy T (G ∩ F) = coverEntropy T F
rw₂ rw₃ : coverEntropy T F = coverEntropy T F
⊢ coverEntropy (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T F

Tactic:
rw [← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]

Premises used: Iff.mpr, Set.MapsTo.val_restrict_apply, Subtype.image_preimage_coe, Set.inter_eq_right, Set.preimage, Dynamics.coverEntropy_image_of_comap, Subtype.val
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
rw :
  coverEntropyInf T
      (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropyInf T F
rw₁ : coverEntropyInf T (G ∩ F) = coverEntropyInf T F
rw₂ rw₃ : coverEntropyInf T F = coverEntropyInf T F
⊢ coverEntropyInf (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropyInf T F

Tactic:
rw [← coverEntropyInf_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]

Premises used: Dynamics.coverEntropyInf_image_of_comap, Iff.mpr, Set.MapsTo.val_restrict_apply, Subtype.image_preimage_coe, Set.inter_eq_right, Set.preimage, Subtype.val
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
rw :
  coverEntropy (MapsTo.restrict T F F h) univ =
    coverEntropy (MapsTo.restrict T F F h) (val (p := fun (x : X) ↦ x ∈ F) ⁻¹' F)
rw₁ rw₂ : coverEntropy (MapsTo.restrict T F F h) univ = coverEntropy (MapsTo.restrict T F F h) univ
⊢ coverEntropy (MapsTo.restrict T F F h) univ = coverEntropy T F

Tactic:
rw [← coverEntropy_restrict_subset Subset.rfl h, coe_preimage_self F]

Premises used: Subtype.coe_preimage_self, Dynamics.coverEntropy_restrict_subset, Set.Subset.rfl
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
rw : coverEntropy S F ≤ coverEntropy S F
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

Tactic:
rw [coverEntropy_image_of_comap _ h F]

Premises used: Dynamics.coverEntropy_image_of_comap
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropy S F ≤ coverEntropy S F

Tactic:
coverEntropy_antitone S F (uniformContinuous_iff.1 h')

Premises used: Dynamics.coverEntropy_antitone, uniformContinuous_iff, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropy S F ≤ coverEntropy S F

Tactic:
exact coverEntropy_antitone S F (uniformContinuous_iff.1 h')

Premises used: Dynamics.coverEntropy_antitone, uniformContinuous_iff, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
rw : coverEntropyInf S F ≤ coverEntropyInf S F
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
rw [coverEntropyInf_image_of_comap _ h F]

Premises used: Dynamics.coverEntropyInf_image_of_comap
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf S F

Tactic:
coverEntropyInf_antitone S F (uniformContinuous_iff.1 h')

Premises used: Dynamics.coverEntropyInf_antitone, uniformContinuous_iff, Iff.mp