awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact coverEntropyInf_antitone S F (uniformContinuous_iff.1 h')

Premises used: Dynamics.coverEntropyInf_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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
rw : coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

Tactic:
rw [← coverEntropy_restrict_subset hF hG]

Premises used: Dynamics.coverEntropy_restrict_subset
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG x) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
rw₁ : φ (↑(MapsTo.restrict S G G hG x) : X) = T (φ (↑x : X))
rw₂ : φ (S (↑x : X)) = T (φ (↑x : X))
rw₃ rw₄ : T (φ (↑x : X)) = T (φ (↑x : X))
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG x) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)

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

Premises used: Set.restrict_apply, Function.Semiconj.eq, Set.MapsTo.val_restrict_apply, Subtype.val
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T

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]
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
apply :
  coverEntropy T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T (φ '' F)
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)

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

Premises used: uniformContinuousOn_iff_restrict, LE.le.trans_eq', Dynamics.coverEntropy_image_le_of_uniformContinuous, Set.preimage, Iff.mp, Subtype.val
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
rw :
  coverEntropy T
      (φ '' image (α := { x : X // x ∈ G }) (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 T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T (φ '' F)

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

Premises used: Iff.mpr, Subtype.image_preimage_coe, Set.inter_eq_right, Set.image_image_val_eq_restrict_image
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
rw : coverEntropyInf T (φ '' F) ≤ coverEntropyInf (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
rw [← coverEntropyInf_restrict_subset hF hG]

Premises used: Dynamics.coverEntropyInf_restrict_subset
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG a) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
rw₁ : φ (↑(MapsTo.restrict S G G hG a) : X) = T (φ (↑a : X))
rw₂ : φ (S (↑a : X)) = T (φ (↑a : X))
rw₃ rw₄ : T (φ (↑a : X)) = T (φ (↑a : X))
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG a) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)

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

Premises used: Set.restrict_apply, Function.Semiconj.eq, Set.MapsTo.val_restrict_apply, Subtype.val
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T

Tactic:
have hφ : Semiconj (G.restrict φ) (hG.restrict S G G) T := by
    intro a
    rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq a]
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
apply :
  coverEntropyInf T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) =
    coverEntropyInf T (φ '' F)
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)

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

Premises used: uniformContinuousOn_iff_restrict, LE.le.trans_eq', Dynamics.coverEntropyInf_image_le_of_uniformContinuous, Set.preimage, Iff.mp, Subtype.val
-- 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
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
rw :
  coverEntropyInf T
      (φ '' image (α := { x : X // x ∈ G }) (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 T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) =
    coverEntropyInf T (φ '' F)

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

Premises used: Iff.mpr, Subtype.image_preimage_coe, Set.inter_eq_right, Set.image_image_val_eq_restrict_image
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G s : Set X
U : SetRel X X
n : ℕ
F_G : F ⊆ G
h : IsDynCoverOf T G U n s
⊢ IsDynCoverOf T F U n s

Tactic:
F_G.trans h

Premises used: Set.Mem, HasSubset.Subset.trans, Dynamics.IsDynCoverOf, Set.Subset, SetRel.IsCover
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G s : Set X
U : SetRel X X
n : ℕ
F_G : F ⊆ G
h : IsDynNetIn T F U n s
⊢ IsDynNetIn T G U n s

Tactic:
⟨h.1.trans F_G, h.2⟩

Premises used: HasSubset.Subset.trans, And.right, And.left, And.intro, Dynamics.IsDynNetIn
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ Monotone (β := ℕ∞) fun (F : Set X) ↦ coverMincard T F U n

Tactic:
fun _ _ F_G ↦ biInf_mono fun _ h ↦ h.monotone_subset F_G

Premises used: Dynamics.IsDynCoverOf.monotone_subset, Monotone, Dynamics.coverMincard, biInf_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ Monotone (β := ℕ∞) fun (F : Set X) ↦ netMaxcard T F U n

Tactic:
fun _ _ F_G ↦ biSup_mono fun _ h ↦ h.monotone_subset F_G

Premises used: biSup_mono, Monotone, Dynamics.IsDynNetIn.monotone_subset, Dynamics.netMaxcard
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ coverEntropyInfEntourage T F U

Tactic:
fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_

Premises used: Monotone, ExpGrowth.expGrowthInf_monotone, Dynamics.coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
refine :
  ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(coverMincard T F U n) : ENNReal) ≤ (↑(coverMincard T G U n) : ENNReal)
⊢ Monotone (β := EReal) fun (F : Set X) ↦ coverEntropyInfEntourage T F U

Tactic:
refine fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_

Premises used: ExpGrowth.expGrowthInf_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F G : Set X
F_G : F ≤ G
n : ℕ
⊢ (↑(coverMincard T F U n) : ENNReal) ≤ (↑(coverMincard T G U n) : ENNReal)

Tactic:
ENat.toENNReal_mono (coverMincard_monotone_subset T U n F_G)

Premises used: ENat.toENNReal_mono, Dynamics.coverMincard_monotone_subset
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F G : Set X
F_G : F ≤ G
n : ℕ
⊢ (↑(coverMincard T F U n) : ENNReal) ≤ (↑(coverMincard T G U n) : ENNReal)

Tactic:
exact ENat.toENNReal_mono (coverMincard_monotone_subset T U n F_G)

Premises used: ENat.toENNReal_mono, Dynamics.coverMincard_monotone_subset
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
refine :
  ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(coverMincard T F U n) : ENNReal) ≤ (↑(coverMincard T G U n) : ENNReal)
⊢ Monotone (β := EReal) fun (F : Set X) ↦ coverEntropyEntourage T F U

Tactic:
refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_

Premises used: ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ netEntropyInfEntourage T F U

Tactic:
fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_

Premises used: Monotone, ExpGrowth.expGrowthInf_monotone, Dynamics.netEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
refine : ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(netMaxcard T F U n) : ENNReal) ≤ (↑(netMaxcard T G U n) : ENNReal)
⊢ Monotone (β := EReal) fun (F : Set X) ↦ netEntropyInfEntourage T F U

Tactic:
refine fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_

Premises used: ExpGrowth.expGrowthInf_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F G : Set X
F_G : F ≤ G
n : ℕ
⊢ (↑(netMaxcard T F U n) : ENNReal) ≤ (↑(netMaxcard T G U n) : ENNReal)

Tactic:
ENat.toENNReal_mono (netMaxcard_monotone_subset T U n F_G)

Premises used: Dynamics.netMaxcard_monotone_subset, ENat.toENNReal_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F G : Set X
F_G : F ≤ G
n : ℕ
⊢ (↑(netMaxcard T F U n) : ENNReal) ≤ (↑(netMaxcard T G U n) : ENNReal)

Tactic:
exact ENat.toENNReal_mono (netMaxcard_monotone_subset T U n F_G)

Premises used: Dynamics.netMaxcard_monotone_subset, ENat.toENNReal_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ netEntropyEntourage T F U

Tactic:
fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_

Premises used: Dynamics.netEntropyEntourage, Monotone, ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
U : SetRel X X
refine : ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(netMaxcard T F U n) : ENNReal) ≤ (↑(netMaxcard T G U n) : ENNReal)
⊢ Monotone (β := EReal) fun (F : Set X) ↦ netEntropyEntourage T F U

Tactic:
refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_

Premises used: ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ coverEntropyInf T F

Tactic:
fun _ _ F_G ↦ iSup₂_mono fun U _ ↦ coverEntropyInfEntourage_monotone T U F_G

Premises used: iSup₂_mono, Monotone, Dynamics.coverEntropyInf, Dynamics.coverEntropyInfEntourage_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ coverEntropy T F

Tactic:
fun _ _ F_G ↦ iSup₂_mono fun U _ ↦ coverEntropyEntourage_monotone T U F_G

Premises used: iSup₂_mono, Monotone, Dynamics.coverEntropyEntourage_monotone, Dynamics.coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
rcases :
  ∀ (W : SetRel X X) (W_V : id W ⊆ V) (W_uni : W ∈ 𝓤 X) (W_symm : W.IsSymm),
    IsDynCoverOf T (_root_.closure F) (V ○ U) n s
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s

Tactic:
rcases (hasBasis_symmetric.mem_iff' V).1 V_uni with ⟨W, ⟨W_uni, W_symm⟩, W_V⟩

Premises used: Iff.mp, Filter.HasBasis.mem_iff', UniformSpace.hasBasis_symmetric
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s

Tactic:
IsDynCoverOf.of_entourage_subset (SetRel.comp_subset_comp_left W_V) fun x hx ↦ ?_

Premises used: SetRel.comp_subset_comp_left, Dynamics.IsDynCoverOf.of_entourage_subset
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
refine : ∀ (x : X) (hx : x ∈ _root_.closure F), ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s

Tactic:
refine IsDynCoverOf.of_entourage_subset (SetRel.comp_subset_comp_left W_V) fun x hx ↦ ?_

Premises used: SetRel.comp_subset_comp_left, Dynamics.IsDynCoverOf.of_entourage_subset
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
obtain : ∀ (y : X) (hxy : y ∈ ball x (dynEntourage T W n)) (hy : y ∈ F), ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n

Tactic:
obtain ⟨y, hxy, hy⟩ := mem_closure_iff_nhds.1 hx _ (ball_dynEntourage_mem_nhds h W_uni n x)

Premises used: mem_closure_iff_nhds, Dynamics.ball_dynEntourage_mem_nhds, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
y : X
hxy : y ∈ ball x (dynEntourage T W n)
hy : y ∈ F
obtain : ∀ (z : X) (hz : z ∈ s) (hyz : (y, z) ∈ dynEntourage T U n), ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n

Tactic:
obtain ⟨z, hz, hyz⟩ := s_cover hy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
y : X
hxy : y ∈ ball x (dynEntourage T W n)
hy : y ∈ F
z : X
hz : z ∈ s
hyz : (y, z) ∈ dynEntourage T U n
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n

Tactic:
⟨z, hz, dynEntourage_comp_subset _ _ _ _ ⟨y, hxy, hyz⟩⟩

Premises used: Dynamics.dynEntourage_comp_subset, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
y : X
hxy : y ∈ ball x (dynEntourage T W n)
hy : y ∈ F
z : X
hz : z ∈ s
hyz : (y, z) ∈ dynEntourage T U n
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n

Tactic:
exact ⟨z, hz, dynEntourage_comp_subset _ _ _ _ ⟨y, hxy, hyz⟩⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
inl : ∀ (h' : coverMincard T F U n = ⊤), coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
inr : ∀ (h' : coverMincard T F U n < ⊤), coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U n) with h' | h'

Premises used: Dynamics.coverMincard, eq_top_or_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n = ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
h' ▸ le_top

Premises used: Eq.rec, le_top, Eq.symm
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n = ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
exact h' ▸ le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n < ⊤
inr :
  ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U n (↑s : Set X))
    (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
    coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 h'

Premises used: Iff.mp, Dynamics.coverMincard_finite_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
s_coverMincard ▸ (s_cover.closure h V_uni).coverMincard_le_card

Premises used: Eq.rec, Dynamics.IsDynCoverOf.coverMincard_le_card, Dynamics.IsDynCoverOf.closure
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
⊢ coverEntropyInfEntourage T (closure F) (V ○ U) ≤ coverEntropyInfEntourage T F U

Tactic:
expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_closure_le h F U V_uni n)

Premises used: Dynamics.coverMincard_closure_le, ExpGrowth.expGrowthInf_monotone, ENat.toENNReal_mono, Dynamics.coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
⊢ coverEntropyEntourage T (closure F) (V ○ U) ≤ coverEntropyEntourage T F U

Tactic:
expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_closure_le h F U V_uni n)

Premises used: Dynamics.coverMincard_closure_le, ENat.toENNReal_mono, Dynamics.coverEntropyEntourage, ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
⊢ coverEntropyInf T (closure F) = coverEntropyInf T F

Tactic:
(iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropyInf_monotone T subset_closure)

Premises used: iSup₂_le, subset_closure, LE.le.antisymm, Dynamics.coverEntropyInf_monotone, Dynamics.coverEntropyInf
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F
⊢ coverEntropyInf T (closure F) = coverEntropyInf T F

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropyInf_monotone T subset_closure)

Premises used: iSup₂_le, subset_closure, LE.le.antisymm, Dynamics.coverEntropyInf_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
obtain :
  ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_U : V ○ V ⊆ U),
    coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F

Tactic:
obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_U : V ○ V ⊆ U
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F

Tactic:
le_iSup₂_of_le V V_uni ((coverEntropyInfEntourage_antitone T (closure F) V_U).trans
    (coverEntropyInfEntourage_closure h F V V_uni))

Premises used: Dynamics.coverEntropyInfEntourage_antitone, Dynamics.coverEntropyInf, closure, Dynamics.coverEntropyInfEntourage_closure, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_U : V ○ V ⊆ U
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F

Tactic:
exact le_iSup₂_of_le V V_uni ((coverEntropyInfEntourage_antitone T (closure F) V_U).trans
    (coverEntropyInfEntourage_closure h F V V_uni))

Premises used: Dynamics.coverEntropyInfEntourage_antitone, closure, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
⊢ coverEntropy T (closure F) = coverEntropy T F

Tactic:
(iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropy_monotone T subset_closure)

Premises used: iSup₂_le, subset_closure, Dynamics.coverEntropy_monotone, LE.le.antisymm, Dynamics.coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage T (closure F) U ≤ coverEntropy T F
⊢ coverEntropy T (closure F) = coverEntropy T F

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropy_monotone T subset_closure)

Premises used: iSup₂_le, subset_closure, Dynamics.coverEntropy_monotone, LE.le.antisymm