awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
inst : UniformSpace X
⊢ coverEntropyInf T ∅ = ⊥

Tactic:
simp only [coverEntropyInf, coverEntropyInfEntourage_empty, iSup_bot]

Premises used: Dynamics.coverEntropyInf, Dynamics.coverEntropyInfEntourage_empty, iSup_bot
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
inst : UniformSpace X
T : X → X
h : F.Nonempty
⊢ 0 ≤ coverEntropyInf T F

Tactic:
(coverEntropyInfEntourage_le_coverEntropyInf T F univ_mem).trans_eq'
    (coverEntropyInfEntourage_univ T h)

Premises used: Dynamics.coverEntropyInfEntourage_univ, Dynamics.coverEntropyInfEntourage_le_coverEntropyInf, LE.le.trans_eq', Filter.univ_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
inst : UniformSpace X
T : X → X
h : F.Nonempty
⊢ 0 ≤ coverEntropy T F

Tactic:
(coverEntropyInf_nonneg T h).trans (coverEntropyInf_le_coverEntropy T F)

Premises used: Dynamics.coverEntropyInf_nonneg, LE.le.trans, Dynamics.coverEntropyInf_le_coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
inst : UniformSpace X
T : X → X
h : MapsTo T F F
⊢ coverEntropyInf T F = coverEntropy T F

Tactic:
le_antisymm (coverEntropyInf_le_coverEntropy T F) (iSup₂_le fun U U_uni ↦ ?_)

Premises used: iSup₂_le, le_antisymm, Dynamics.coverEntropyInf_le_coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
inst : UniformSpace X
T : X → X
h : MapsTo T F F
refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage T F U ≤ coverEntropyInf T F
⊢ coverEntropyInf T F = coverEntropy T F

Tactic:
refine le_antisymm (coverEntropyInf_le_coverEntropy T F) (iSup₂_le fun U U_uni ↦ ?_)

Premises used: iSup₂_le, le_antisymm, Dynamics.coverEntropyInf_le_coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
inst : UniformSpace X
T : X → X
h : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
obtain :
  ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_symm : SetRel.IsSymm V) (V_U : V ○ V ⊆ U),
    coverEntropyEntourage T F U ≤ coverEntropyInf T F
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F

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.CoverEntropy
Goal:
X : Type u_1
F : Set X
inst : UniformSpace X
T : X → X
h : MapsTo T F F
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
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F

Tactic:
(coverEntropyEntourage_antitone T F V_U).trans <| le_iSup₂_of_le V V_uni <|
     coverEntropyEntourage_le_coverEntropyInfEntourage h

Premises used: Dynamics.coverEntropyEntourage_le_coverEntropyInfEntourage, Dynamics.coverEntropyEntourage_antitone, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
inst : UniformSpace X
T : X → X
h : MapsTo T F F
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
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F

Tactic:
exact (coverEntropyEntourage_antitone T F V_U).trans <| le_iSup₂_of_le V V_uni <|
     coverEntropyEntourage_le_coverEntropyInfEntourage h

Premises used: Dynamics.coverEntropyEntourage_le_coverEntropyInfEntourage, Dynamics.coverEntropyEntourage_antitone, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
m n : ℕ
F s : Set X
m_n : m ≤ n
h : IsDynNetIn T F U m s
⊢ IsDynNetIn T F U n s

Tactic:
⟨h.1, PairwiseDisjoint.mono h.2 fun x ↦ ball_mono (dynEntourage_antitone T U m_n) x⟩

Premises used: Set.PairwiseDisjoint.mono, UniformSpace.ball_mono, And.right, And.left, And.intro, Dynamics.IsDynNetIn, Dynamics.dynEntourage_antitone
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n : ℕ
F s : Set X
U_V : U ⊆ V
h : IsDynNetIn T F V n s
⊢ IsDynNetIn T F U n s

Tactic:
⟨h.1, PairwiseDisjoint.mono h.2 fun x ↦ ball_mono (dynEntourage_monotone T n U_V) x⟩

Premises used: Set.PairwiseDisjoint.mono, UniformSpace.ball_mono, And.right, And.left, And.intro, Dynamics.IsDynNetIn, Dynamics.dynEntourage_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
⊢ IsDynNetIn T F U n ∅

Tactic:
⟨empty_subset F, pairwise_empty _⟩

Premises used: Set.pairwise_empty, And.intro, Set.empty_subset, Dynamics.IsDynNetIn
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
x : X
T : X → X
U : SetRel X X
n : ℕ
h : x ∈ F
⊢ IsDynNetIn T F U n {x}

Tactic:
⟨singleton_subset_iff.2 h, pairwise_singleton x _⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.pairwise_singleton, And.intro, Dynamics.IsDynNetIn
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s t : Finset X
hs : IsDynNetIn T F U n (↑s : Set X)
ht : IsDynCoverOf T F U n (↑t : Set X)
x : X
x_s : x ∈ s
⊢ ∃ z ∈ t, z ∈ ball x (dynEntourage T U n)

Tactic:
simpa using ht (hs.1 x_s)

Premises used: And.left
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s t : Finset X
hs : IsDynNetIn T F U n (↑s : Set X)
ht : IsDynCoverOf T F U n (↑t : Set X)
⊢ ∀ (x : X) (x_s : x ∈ s), ∃ z ∈ t, z ∈ ball x (dynEntourage T U n)

Tactic:
have (x : X) (x_s : x ∈ s) : ∃ z ∈ t, z ∈ ball x (dynEntourage T U n) := by
    simpa using ht (hs.1 x_s)
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s t : Finset X
hs : IsDynNetIn T F U n (↑s : Set X)
ht : IsDynCoverOf T F U n (↑t : Set X)
this : ∀ (x : X) (x_s : x ∈ s), ∃ z ∈ t, z ∈ ball x (dynEntourage T U n)
choose! :
  ∀ (F : (x : X) → X) (s_t : ∀ (x : X) (x_s : x ∈ s), F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)), s.card ≤ t.card
⊢ s.card ≤ t.card

Tactic:
choose! F s_t using this
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F_1 : Set X
s t : Finset X
hs : IsDynNetIn T F_1 U n (↑s : Set X)
ht : IsDynCoverOf T F_1 U n (↑t : Set X)
F : (x : X) → X
s_t : ∀ (x : X) (x_s : x ∈ s), F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)
apply : InjOn F (↑s : Set X)
⊢ s.card ≤ t.card

Tactic:
apply Finset.card_le_card_of_injOn F fun x x_s ↦ (s_t x x_s).1

Premises used: Finset.card_le_card_of_injOn, And.left
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F_1 : Set X
s t : Finset X
hs : IsDynNetIn T F_1 U n (↑s : Set X)
ht : IsDynCoverOf T F_1 U n (↑t : Set X)
F : (x : X) → X
s_t : ∀ (x : X) (x_s : x ∈ s), F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)
⊢ InjOn F (↑s : Set X)

Tactic:
fun x x_s y y_s Fx_Fy ↦
    PairwiseDisjoint.elim_set hs.2 x_s y_s (F x) (s_t x x_s).2 (Fx_Fy ▸ (s_t y y_s).2)

Premises used: Eq.rec, And.right, Set.InjOn, Eq.symm, Set.PairwiseDisjoint.elim_set
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F_1 : Set X
s t : Finset X
hs : IsDynNetIn T F_1 U n (↑s : Set X)
ht : IsDynCoverOf T F_1 U n (↑t : Set X)
F : (x : X) → X
s_t : ∀ (x : X) (x_s : x ∈ s), F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)
⊢ InjOn F (↑s : Set X)

Tactic:
exact fun x x_s y y_s Fx_Fy ↦
    PairwiseDisjoint.elim_set hs.2 x_s y_s (F x) (s_t x x_s).2 (Fx_Fy ▸ (s_t y y_s).2)

Premises used: And.right, Set.PairwiseDisjoint.elim_set
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
F : Set X
s : Finset X
h : IsDynNetIn T F U n (↑s : Set X)
⊢ (↑s.card : ℕ∞) ≤ netMaxcard T F U n

Tactic:
le_iSup₂ (α := ℕ∞) s h

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

Tactic:
fun _ _ m_n ↦ biSup_mono fun _ h ↦ h.of_le m_n

Premises used: Dynamics.IsDynNetIn.of_le, biSup_mono, Monotone, Dynamics.netMaxcard
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
n : ℕ
⊢ Antitone (β := ℕ∞) fun (U : SetRel X X) ↦ netMaxcard T F U n

Tactic:
fun _ _ U_V ↦ biSup_mono fun _ h ↦ h.of_entourage_subset U_V

Premises used: biSup_mono, Antitone, Dynamics.IsDynNetIn.of_entourage_subset, Dynamics.netMaxcard
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
mp : netMaxcard T F U n < ⊤ → ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n
mpr : (∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n) → netMaxcard T F U n < ⊤
⊢ netMaxcard T F U n < ⊤ ↔ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
mp :
  ∀ (k : ℕ) (k_max : (↑k : WithTop ℕ) = netMaxcard T F U n),
    ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n

Tactic:
obtain ⟨k, k_max⟩ := WithTop.ne_top_iff_exists.1 h.ne

Premises used: WithTop.ne_top_iff_exists, Iff.mp, LT.lt.ne
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : (↑k : WithTop ℕ) = netMaxcard T F U n
mp : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = (↑k : WithTop ℕ)
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n

Tactic:
rw [← k_max]
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : (↑k : WithTop ℕ) = netMaxcard T F U n
mp : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = (↑k : WithTop ℕ)

Tactic:
simp only [ENat.some_eq_coe, Nat.cast_inj]

Premises used: ENat.some_eq_coe, Nat.cast_inj
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : (↑k : WithTop ℕ) = netMaxcard T F U n
rw :
  Eq (α := ℕ∞) (⨆ (s : Finset X), ⨆ (_ : IsDynNetIn T F U n (↑s : Set X)), (↑s.card : ℕ∞))
    (⨆ (a : Finset X),
      ⨆ (_ : Membership.mem (γ := Set (Finset X)) {s : Finset X | IsDynNetIn T F U n (↑s : Set X)} a),
        (WithTop.some ∘ Finset.card) a)
⊢ netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
rw [netMaxcard, ← image_comp, sSup_image]

Premises used: sSup_image, Set.image_comp, Dynamics.netMaxcard
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : (↑k : WithTop ℕ) = netMaxcard T F U n
⊢ Eq (α := ℕ∞) (⨆ (s : Finset X), ⨆ (_ : IsDynNetIn T F U n (↑s : Set X)), (↑s.card : ℕ∞))
    (⨆ (a : Finset X),
      ⨆ (_ : Membership.mem (γ := Set (Finset X)) {s : Finset X | IsDynNetIn T F U n (↑s : Set X)} a),
        (WithTop.some ∘ Finset.card) a)

Tactic:
simp only [mem_setOf_eq, ENat.some_eq_coe, Function.comp_apply]

Premises used: ENat.some_eq_coe, Set.mem_setOf_eq, Function.comp_apply
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : (↑k : WithTop ℕ) = netMaxcard T F U n
⊢ netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
have : netMaxcard T F U n
      = sSup (WithTop.some '' Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
      rw [netMaxcard, ← image_comp, sSup_image]
      simp only [mem_setOf_eq, ENat.some_eq_coe, Function.comp_apply]
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : (↑k : WithTop ℕ) = netMaxcard T F U n
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
rw [this] at k_max
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : (↑k : WithTop ℕ) = netMaxcard T F U n
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
k_max₁ :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
rw [this] at k_max
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
⟨k, mem_upperBounds.2 ?_⟩

Premises used: Iff.mpr, BddAbove, Set.Nonempty, Exists.intro, mem_upperBounds
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
refine : ∀ x ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}, x ≤ k
⊢ BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
refine ⟨k, mem_upperBounds.2 ?_⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
simp : ∀ (a : Finset X), IsDynNetIn T F U n (↑a : Set X) → a.card ≤ k
⊢ ∀ x ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}, x ≤ k

Tactic:
simp only [mem_image, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_1 : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
s : Finset X
h : IsDynNetIn T F U n (↑s : Set X)
rw :
  (↑s.card : WithTop ℕ) ≤
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ s.card ≤ k

Tactic:
rw [← WithTop.coe_le_coe, k_max]

Premises used: WithTop.coe_le_coe
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_1 : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
s : Finset X
h : IsDynNetIn T F U n (↑s : Set X)
h₁ :
  (↑s.card : WithTop ℕ) ∈
    WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}
⊢ (↑s.card : WithTop ℕ) ≤
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
apply le_sSup

Premises used: le_sSup
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_1 : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
s : Finset X
h : IsDynNetIn T F U n (↑s : Set X)
h₁ : ∃ (x : Finset X), IsDynNetIn T F U n (↑x : Set X) ∧ x.card = s.card
⊢ (↑s.card : WithTop ℕ) ∈
    WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}

Tactic:
simp only [ENat.some_eq_coe, mem_image, mem_setOf_eq, Nat.cast_inj, exists_eq_right]

Premises used: ENat.some_eq_coe, Set.mem_image, exists_eq_right, Set.mem_setOf_eq, Nat.cast_inj
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_1 : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
s : Finset X
h : IsDynNetIn T F U n (↑s : Set X)
⊢ ∃ (x : Finset X), IsDynNetIn T F U n (↑x : Set X) ∧ x.card = s.card

Tactic:
Filter.frequently_principal.mp fun a ↦ a h rfl

Premises used: Set.Mem, Dynamics.IsDynNetIn, Iff.mp, Filter.frequently_principal, rfl
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_1 : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
s : Finset X
h : IsDynNetIn T F U n (↑s : Set X)
⊢ ∃ (x : Finset X), IsDynNetIn T F U n (↑x : Set X) ∧ x.card = s.card

Tactic:
exact Filter.frequently_principal.mp fun a ↦ a h rfl

Premises used: Iff.mp, Filter.frequently_principal, rfl
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})

Tactic:
have h_bdda : BddAbove (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
      refine ⟨k, mem_upperBounds.2 ?_⟩
      simp only [mem_image, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
      intro s h
      rw [← WithTop.coe_le_coe, k_max]
      apply le_sSup
      simp only [ENat.some_eq_coe, mem_image, mem_setOf_eq, Nat.cast_inj, exists_eq_right]
      exact Filter.frequently_principal.mp fun a ↦ a h rfl
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
h_bdda : BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty

Tactic:
⟨0, ?_⟩

Premises used: Set.Nonempty, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
h_bdda : BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
refine : 0 ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}
⊢ (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty

Tactic:
refine ⟨0, ?_⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
h_bdda : BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
simp : IsDynNetIn T F U n ∅
⊢ 0 ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}

Tactic:
simp only [mem_image, mem_setOf_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]

Premises used: Finset.coe_empty, Set.mem_image, exists_eq_right, Set.mem_setOf_eq, Finset.card_eq_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
h_bdda : BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ IsDynNetIn T F U n ∅

Tactic:
isDynNetIn_empty

Premises used: Dynamics.isDynNetIn_empty
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max :
  (↑k : WithTop ℕ) =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
this :
  netMaxcard T F U n =
    sSup (WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
h_bdda : BddAbove (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
⊢ IsDynNetIn T F U n ∅

Tactic:
exact isDynNetIn_empty

Premises used: Dynamics.isDynNetIn_empty