awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h₁ : ¬Eq (α := ℝ≥0∞) 1 0
⊢ ¬(↑(netMaxcard T F U 0) : ℝ≥0∞) = 0 0

Tactic:
rw [netMaxcard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]

Premises used: Dynamics.netMaxcard_zero, Pi.zero_apply, ENat.toENNReal_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬Eq (α := ℝ≥0∞) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬Eq (α := ℝ≥0∞) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ 0 ≤ netEntropyEntourage T F U

Tactic:
(netEntropyInfEntourage_nonneg T h U).trans (netEntropyInfEntourage_le_netEntropyEntourage T F U)

Premises used: Dynamics.netEntropyInfEntourage_nonneg, Dynamics.netEntropyInfEntourage_le_netEntropyEntourage, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
rw : (expGrowthInf fun (n : ℕ) ↦ (↑(netMaxcard T F univ n) : ℝ≥0∞)) = expGrowthInf fun (x : ℕ) ↦ 1
⊢ netEntropyInfEntourage T F univ = 0

Tactic:
rw [← expGrowthInf_const one_ne_zero one_ne_top, netEntropyInfEntourage]

Premises used: Dynamics.netEntropyInfEntourage, ExpGrowth.expGrowthInf_const, one_ne_zero, ENNReal.one_ne_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ (expGrowthInf fun (n : ℕ) ↦ (↑(netMaxcard T F univ n) : ℝ≥0∞)) = expGrowthInf fun (x : ℕ) ↦ 1

Tactic:
simp only [netMaxcard_univ T h, ENat.toENNReal_one]

Premises used: ENat.toENNReal_one, Dynamics.netMaxcard_univ
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
rw : (expGrowthSup fun (n : ℕ) ↦ (↑(netMaxcard T F univ n) : ℝ≥0∞)) = expGrowthSup fun (x : ℕ) ↦ 1
⊢ netEntropyEntourage T F univ = 0

Tactic:
rw [← expGrowthSup_const one_ne_zero one_ne_top, netEntropyEntourage]

Premises used: Dynamics.netEntropyEntourage, ExpGrowth.expGrowthSup_const, one_ne_zero, ENNReal.one_ne_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑(netMaxcard T F univ n) : ℝ≥0∞)) = expGrowthSup fun (x : ℕ) ↦ 1

Tactic:
simp only [netMaxcard_univ T h, ENat.toENNReal_one]

Premises used: ENat.toENNReal_one, Dynamics.netMaxcard_univ
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
⊢ netEntropyInfEntourage T F U ≤ coverEntropyInfEntourage T F U

Tactic:
expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (netMaxcard_le_coverMincard T F n)

Premises used: Dynamics.netMaxcard_le_coverMincard, ExpGrowth.expGrowthInf_monotone, ENat.toENNReal_mono, Dynamics.netEntropyInfEntourage, Dynamics.coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst : U.IsRefl
inst_1 : U.IsSymm
⊢ coverEntropyInfEntourage T F (U ○ U) ≤ netEntropyInfEntourage T F U

Tactic:
expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_le_netMaxcard T F n)

Premises used: ExpGrowth.expGrowthInf_monotone, ENat.toENNReal_mono, Dynamics.coverMincard_le_netMaxcard, Dynamics.netEntropyInfEntourage, Dynamics.coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
⊢ netEntropyEntourage T F U ≤ coverEntropyEntourage T F U

Tactic:
expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (netMaxcard_le_coverMincard T F n)

Premises used: Dynamics.netEntropyEntourage, Dynamics.netMaxcard_le_coverMincard, ENat.toENNReal_mono, Dynamics.coverEntropyEntourage, ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst : U.IsRefl
inst_1 : U.IsSymm
⊢ coverEntropyEntourage T F (U ○ U) ≤ netEntropyEntourage T F U

Tactic:
expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_le_netMaxcard T F n)

Premises used: Dynamics.netEntropyEntourage, ENat.toENNReal_mono, Dynamics.coverMincard_le_netMaxcard, Dynamics.coverEntropyEntourage, ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
a₁ : ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U ≤ coverEntropyInf T F
⊢ coverEntropyInf T F = ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le, Dynamics.coverEntropyInf
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
⊢ coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U ≤ coverEntropyInf T F

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), netEntropyInfEntourage T F U ≤ coverEntropyInf T F
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U ≤ coverEntropyInf T F

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
a :
  ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_symm : SetRel.IsSymm V) (V_U : V ○ V ⊆ U),
    coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

Tactic:
obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
⊢ SetRel.IsRefl V

Tactic:
have := isRefl_of_mem_uniformity V_uni
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
this : SetRel.IsRefl V
apply : (fun (U : SetRel X X) ↦ coverEntropyInfEntourage T F U) (V ○ V) ≤ netEntropyInfEntourage T F V
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U

Tactic:
apply (coverEntropyInfEntourage_antitone T F V_U).trans (le_iSup₂_of_le V V_uni _)

Premises used: Dynamics.coverEntropyInfEntourage_antitone, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
this : SetRel.IsRefl V
⊢ (fun (U : SetRel X X) ↦ coverEntropyInfEntourage T F U) (V ○ V) ≤ netEntropyInfEntourage T F V

Tactic:
coverEntropyInfEntourage_le_netEntropyInfEntourage T F

Premises used: Dynamics.coverEntropyInfEntourage_le_netEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
this : SetRel.IsRefl V
⊢ (fun (U : SetRel X X) ↦ coverEntropyInfEntourage T F U) (V ○ V) ≤ netEntropyInfEntourage T F V

Tactic:
exact coverEntropyInfEntourage_le_netEntropyInfEntourage T F

Premises used: Dynamics.coverEntropyInfEntourage_le_netEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
a : (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropyInf T F
⊢ netEntropyInfEntourage T F U ≤ coverEntropyInf T F

Tactic:
apply (netEntropyInfEntourage_antitone T F SetRel.symmetrize_subset_self).trans

Premises used: SetRel.symmetrize_subset_self, LE.le.trans, Dynamics.netEntropyInfEntourage_antitone
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
a :
  (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤
    coverEntropyInfEntourage T F (SetRel.symmetrize U)
⊢ (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropyInf T F

Tactic:
apply (le_iSup₂ (SetRel.symmetrize U) (symmetrize_mem_uniformity U_uni)).trans'

Premises used: SetRel.symmetrize, le_iSup₂, symmetrize_mem_uniformity, LE.le.trans'
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤
    coverEntropyInfEntourage T F (SetRel.symmetrize U)

Tactic:
netEntropyInfEntourage_le_coverEntropyInfEntourage T F

Premises used: Dynamics.netEntropyInfEntourage_le_coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤
    coverEntropyInfEntourage T F (SetRel.symmetrize U)

Tactic:
exact netEntropyInfEntourage_le_coverEntropyInfEntourage T F

Premises used: Dynamics.netEntropyInfEntourage_le_coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
a₁ : ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U ≤ coverEntropy T F
⊢ coverEntropy T F = ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le, Dynamics.coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
⊢ coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), netEntropyEntourage T F U ≤ coverEntropy T F
⊢ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U ≤ coverEntropy T F

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
a :
  ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_symm : SetRel.IsSymm V) (V_comp_U : V ○ V ⊆ U),
    coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
obtain ⟨V, V_uni, V_symm, V_comp_U⟩ := comp_symm_mem_uniformity_sets U_uni

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_comp_U : V ○ V ⊆ U
apply : (fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V) ≤ netEntropyEntourage T F V
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
apply (coverEntropyEntourage_antitone T F V_comp_U).trans (le_iSup₂_of_le V V_uni _)

Premises used: Dynamics.coverEntropyEntourage_antitone, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_comp_U : V ○ V ⊆ U
⊢ SetRel.IsRefl V

Tactic:
have := isRefl_of_mem_uniformity V_uni
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_comp_U : V ○ V ⊆ U
this : SetRel.IsRefl V
⊢ (fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V) ≤ netEntropyEntourage T F V

Tactic:
coverEntropyEntourage_le_netEntropyEntourage T F

Premises used: Dynamics.coverEntropyEntourage_le_netEntropyEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_comp_U : V ○ V ⊆ U
this : SetRel.IsRefl V
⊢ (fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V) ≤ netEntropyEntourage T F V

Tactic:
exact coverEntropyEntourage_le_netEntropyEntourage T F

Premises used: Dynamics.coverEntropyEntourage_le_netEntropyEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
a : (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropy T F
⊢ netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
apply (netEntropyEntourage_antitone T F SetRel.symmetrize_subset_self).trans

Premises used: Dynamics.netEntropyEntourage_antitone, SetRel.symmetrize_subset_self, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
a :
  (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤
    coverEntropyEntourage T F (SetRel.symmetrize U)
⊢ (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropy T F

Tactic:
apply (le_iSup₂ (SetRel.symmetrize U) (symmetrize_mem_uniformity U_uni)).trans'

Premises used: SetRel.symmetrize, le_iSup₂, symmetrize_mem_uniformity, LE.le.trans'
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤
    coverEntropyEntourage T F (SetRel.symmetrize U)

Tactic:
netEntropyEntourage_le_coverEntropyEntourage T F

Premises used: Dynamics.netEntropyEntourage_le_coverEntropyEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤
    coverEntropyEntourage T F (SetRel.symmetrize U)

Tactic:
exact netEntropyEntourage_le_coverEntropyEntourage T F

Premises used: Dynamics.netEntropyEntourage_le_coverEntropyEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
rw :
  Eq (α := EReal) (⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U) (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
⊢ coverEntropyInf T F = ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
rw [coverEntropyInf_eq_iSup_netEntropyInfEntourage T F]

Premises used: Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
apply :
  LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyInfEntourage T F i)
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
⊢ Eq (α := EReal) (⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U) (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))

Tactic:
apply (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩).antisymm'

Premises used: le_refl, LE.le.antisymm', iSup₂_mono', Exists.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyInfEntourage T F i)
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
refine :
  ∀ (U : SetRel X X) (U_uni : U ∈ 𝓤 X),
    netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
⊢ LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyInfEntourage T F i)
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
obtain :
  ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
    netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
⊢ netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
apply :
  LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (s i))
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
⊢ netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
apply (netEntropyInfEntourage_antitone T F si_U).trans

Premises used: LE.le.trans, Dynamics.netEntropyInfEntourage_antitone
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (s i))
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))

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

Premises used: le_iSup₂
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (s i))
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))

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

Premises used: le_iSup₂
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
rw : Eq (α := EReal) (⨆ U ∈ 𝓤 X, netEntropyEntourage T F U) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
⊢ coverEntropy T F = ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
rw [coverEntropy_eq_iSup_netEntropyEntourage T F]

Premises used: Dynamics.coverEntropy_eq_iSup_netEntropyEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
apply :
  LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyEntourage T F i) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
⊢ Eq (α := EReal) (⨆ 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'

Premises used: le_refl, LE.le.antisymm', iSup₂_mono', Exists.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyEntourage T F i) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))

Tactic:
iSup₂_le fun U U_uni ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
refine :
  ∀ (U : SetRel X X) (U_uni : U ∈ 𝓤 X),
    netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)
⊢ LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyEntourage T F i) (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))

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

Premises used: iSup₂_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
obtain :
  ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
    netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)
⊢ netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
apply :
  LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (s i))
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))
⊢ netEntropyEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i)

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

Premises used: Dynamics.netEntropyEntourage_antitone, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
inst : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ LE.le (α := EReal) ((fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (s i))
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyEntourage T F (s i))

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

Premises used: le_iSup₂