awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
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 : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)
have obtain : ∀ (i : ι) (h_i : p i) (si_U : s i ⊆ U),
  coverEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)
Tactic: obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
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
have refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage T F U ≤ coverEntropyInf T F
Tactic: refine le_antisymm (coverEntropyInf_le_coverEntropy T F) (iSup₂_le fun U U_uni ↦ ?_)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
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
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F
have 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
Tactic: obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)
⊢ s.card ≤ t.card
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ s.card ≤ t.card
have 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
Tactic: choose! F s_t using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ s.card ≤ t.card
have apply : InjOn F (↑s : Set X)
Tactic: apply Finset.card_le_card_of_injOn F fun x x_s ↦ (s_t x x_s).1
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n < ⊤ ↔ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n
have mp : 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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ netMaxcard T F U n < ⊤ ↔ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n
have mpr : (∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n) → netMaxcard T F U n < ⊤
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n
have 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
Tactic: obtain ⟨k, k_max⟩ := WithTop.ne_top_iff_exists.1 h.ne
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n
have mp : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = (↑k : WithTop ℕ)
Tactic: rw [← k_max]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = (↑k : WithTop ℕ)
have mp : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
Tactic: simp only [ENat.some_eq_coe, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)})
have 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)
Tactic: rw [netMaxcard, ← image_comp, sSup_image]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
have 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)})
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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)})
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
have 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)})
Tactic: rw [this] at k_max
Cleared hypotheses: k_max, this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)})
have refine : ∀ x ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}, x ≤ k
Tactic: refine ⟨k, mem_upperBounds.2 ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)})
⊢ ∀ x ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}, x ≤ k
have simp : ∀ (a : Finset X), IsDynNetIn T F U n (↑a : Set X) → a.card ≤ k
Tactic: simp only [mem_image, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ s.card ≤ k
have 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)})
Tactic: rw [← WithTop.coe_le_coe, k_max]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ (↑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)})
have 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)}
Tactic: apply le_sSup
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ (↑s.card : WithTop ℕ) ∈
    WithTop.some '' image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}
have h₁ : ∃ (x : Finset X), IsDynNetIn T F U n (↑x : Set X) ∧ x.card = s.card
Tactic: simp only [ENat.some_eq_coe, mem_image, mem_setOf_eq, Nat.cast_inj, exists_eq_right]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)})
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
have h_bdda : 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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
have refine : 0 ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}
Tactic: refine ⟨0, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)})
⊢ 0 ∈ image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}
have simp : IsDynNetIn T F U n ∅
Tactic: simp only [mem_image, mem_setOf_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)})
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
have h_nemp : (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty
Tactic: have h_nemp : (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}).Nonempty := by
      refine ⟨0, ?_⟩
      simp only [mem_image, mem_setOf_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]
      exact isDynNetIn_empty
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)})
h_nemp : (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
have k_max₁ : k = sSup (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)})
Tactic: rw [← WithTop.coe_sSup' h_bdda, ENat.some_eq_coe, Nat.cast_inj] at k_max
Cleared hypotheses: k_max, this, h_bdda, h_nemp
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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 = sSup (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)})
h_nemp : (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
have key : sSup (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)}
Tactic: have key := Nat.sSup_mem h_nemp h_bdda
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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 = sSup (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)})
h_nemp : (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty
key :
  sSup (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)}
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k
have key₁ : ∃ (x : Finset X), Membership.mem (γ := Set (Finset X)) {s : Finset X | IsDynNetIn T F U n (↑s : Set X)} x ∧ x.card = k
Tactic: rw [← k_max, mem_image] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ (↑s.card : ℕ∞) = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤
have mpr : ∀ (s : Finset X),
  IsDynNetIn T F U n (↑s : Set X) → ∀ (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n), netMaxcard T F U n < ⊤
Tactic: obtain ⟨s, _, s_card⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
s : Finset X
left : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤
have mpr : LT.lt (α := ℕ∞) (↑s.card : ℕ∞) ⊤
Tactic: rw [← s_card]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ netMaxcard T ∅ U n = 0
have rw : ∀ (i : Finset X) (j : IsDynNetIn T ∅ U n (↑i : Set X)), Eq (α := ℕ∞) (↑i.card : ℕ∞) ⊥
Tactic: rw [netMaxcard, ← bot_eq_zero, iSup₂_eq_bot]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : IsDynNetIn T ∅ U n (↑s : Set X)
⊢ Eq (α := ℕ∞) (↑s.card : ℕ∞) ⊥
have s_net₁ : (↑s : Set X) = ∅
Tactic: replace s_net := subset_empty_iff.1 s_net.1
Cleared hypotheses: s_net
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : (↑s : Set X) = ∅
⊢ Eq (α := ℕ∞) (↑s.card : ℕ∞) ⊥
have s_net₁ : s = ∅
Tactic: norm_cast at s_net
Cleared hypotheses: s_net
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : s = ∅
⊢ Eq (α := ℕ∞) (↑s.card : ℕ∞) ⊥
have rw : Eq (α := ℕ∞) (↑(Finset.card.{u_1} (α := X) ∅) : ℕ∞) ⊥
Tactic: rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : s = ∅
rw : Eq (α := ℕ∞) (↑(Finset.card.{u_1} (α := X) ∅) : ℕ∞) ⊥
⊢ Eq (α := ℕ∞) (↑s.card : ℕ∞) ⊥
have rw₁ : Eq (α := ℕ∞) (↑0 : ℕ∞) ⊥
Tactic: rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : s = ∅
rw : Eq (α := ℕ∞) (↑(Finset.card.{u_1} (α := X) ∅) : ℕ∞) ⊥
rw₁ : Eq (α := ℕ∞) (↑0 : ℕ∞) ⊥
⊢ Eq (α := ℕ∞) (↑s.card : ℕ∞) ⊥
have rw₂ : Eq (α := ℕ∞) 0 ⊥
Tactic: rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : s = ∅
rw : Eq (α := ℕ∞) (↑(Finset.card.{u_1} (α := X) ∅) : ℕ∞) ⊥
rw₁ : Eq (α := ℕ∞) (↑0 : ℕ∞) ⊥
rw₂ : Eq (α := ℕ∞) 0 ⊥
⊢ Eq (α := ℕ∞) (↑s.card : ℕ∞) ⊥
have rw₃ : Eq (α := ℕ∞) 0 0
Tactic: rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : F = ∅
⊢ netMaxcard T F U n = 0
have rw : netMaxcard T ∅ U n = 0
Tactic: rw [h, netMaxcard_empty]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : F = ∅
rw : netMaxcard T ∅ U n = 0
⊢ netMaxcard T F U n = 0
have rw₁ : Eq (α := ℕ∞) 0 0
Tactic: rw [h, netMaxcard_empty]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n = 0 ↔ F = ∅
have refine : ∀ (h : netMaxcard T F U n = 0), F = ∅
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, netMaxcard_empty]⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
⊢ F = ∅
have rw : ∀ (x : X), x ∉ F
Tactic: rw [eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
⊢ False
have key : IsDynNetIn T F U n {x}
Tactic: have key := isDynNetIn_singleton T U n x_F
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n {x}
⊢ False
have key₁ : IsDynNetIn T F U n (↑{x} : Set X)
Tactic: rw [← Finset.coe_singleton] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n (↑{x} : Set X)
⊢ False
have key₁ : (↑(Finset.card (α := X) {x}) : ℕ∞) ≤ netMaxcard T F U n
Tactic: replace key := key.card_le_netMaxcard
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : (↑(Finset.card (α := X) {x}) : ℕ∞) ≤ netMaxcard T F U n
⊢ False
have key₁ : LE.le (α := ℕ∞) 1 0
Tactic: rw [Finset.card_singleton, Nat.cast_one, h] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ 1 ≤ netMaxcard T F U n ↔ F.Nonempty
have rw : netMaxcard T F U n ≠ 0 ↔ F ≠ ∅
Tactic: rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ netMaxcard T F U 0 = 1
have apply : ∀ (i : Finset X) (j : IsDynNetIn T F U 0 (↑i : Set X)), LE.le (α := ℕ∞) (↑i.card : ℕ∞) 1
Tactic: apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F U 0).2 h)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
⊢ ∀ (j : IsDynNetIn T F U 0 (↑s : Set X)), LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
have this : (↑s : Set X) ⊆ F →
  ∀ (s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ ball x (dynEntourage T U 0)),
    LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
Tactic: ⟨_, s_net⟩