awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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
-- 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)})
h_nemp : (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty
⊢ 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

Premises used: ENat.some_eq_coe, WithTop.coe_sSup', 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 ℕ) =
    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
k_max₁ : k = sSup (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 [← WithTop.coe_sSup' h_bdda, ENat.some_eq_coe, Nat.cast_inj] at k_max

Premises used: ENat.some_eq_coe, WithTop.coe_sSup', 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 ℕ) =
    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
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)})
⊢ BddAbove (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

Premises used: ENat.some_eq_coe, WithTop.coe_sSup', 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 ℕ) =
    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
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)})
⊢ (image.{u_1, 0} (α := Finset X) Finset.card {s : Finset X | IsDynNetIn T F U n (↑s : Set X)}).Nonempty

Tactic:
rw [← WithTop.coe_sSup' h_bdda, ENat.some_eq_coe, Nat.cast_inj] at k_max

Premises used: ENat.some_eq_coe, WithTop.coe_sSup', 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 = 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
⊢ 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
-- 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 = 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)}
⊢ ∃ (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

Premises used: Set.mem_image
-- 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 = 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 : ∃ (x : Finset X), IsDynNetIn T F U n (↑x : Set X) ∧ x.card = k
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k

Tactic:
key
-- 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 = 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 : ∃ (x : Finset X), IsDynNetIn T F U n (↑x : Set X) ∧ x.card = k
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ s.card = k

Tactic:
exact key
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
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
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 < ⊤
⊢ netMaxcard T F U n < ⊤

Tactic:
obtain ⟨s, _, s_card⟩ := h
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
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
mpr : LT.lt (α := ℕ∞) (↑s.card : ℕ∞) ⊤
⊢ netMaxcard T F U n < ⊤

Tactic:
rw [← s_card]
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
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
⊢ LT.lt (α := ℕ∞) (↑s.card : ℕ∞) ⊤

Tactic:
WithTop.coe_lt_top s.card

Premises used: WithTop.coe_lt_top, Finset.card
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
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
⊢ LT.lt (α := ℕ∞) (↑s.card : ℕ∞) ⊤

Tactic:
exact WithTop.coe_lt_top s.card

Premises used: WithTop.coe_lt_top, Finset.card
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
rw : ∀ (i : Finset X) (j : IsDynNetIn T ∅ U n (↑i : Set X)), Eq (α := ℕ∞) (↑i.card : ℕ∞) ⊥
⊢ netMaxcard T ∅ U n = 0

Tactic:
rw [netMaxcard, ← bot_eq_zero, iSup₂_eq_bot]

Premises used: iSup₂_eq_bot, bot_eq_zero, Dynamics.netMaxcard
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
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)
⊢ (↑s : Set X) = ∅

Tactic:
replace s_net := subset_empty_iff.1 s_net.1
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : (↑s : Set X) = ∅
⊢ s = ∅

Tactic:
norm_cast at s_net
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
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 ⊥
rw₃ rw₄ : Eq (α := ℕ∞) 0 0
⊢ Eq (α := ℕ∞) (↑s.card : ℕ∞) ⊥

Tactic:
rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']

Premises used: CharP.cast_eq_zero, Finset.card_empty, bot_eq_zero'
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : F = ∅
rw : netMaxcard T ∅ U n = 0
rw₁ rw₂ : Eq (α := ℕ∞) 0 0
⊢ netMaxcard T F U n = 0

Tactic:
rw [h, netMaxcard_empty]

Premises used: Dynamics.netMaxcard_empty
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
refine : ∀ (h : netMaxcard T F U n = 0), F = ∅
⊢ netMaxcard T F U n = 0 ↔ F = ∅

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, netMaxcard_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 = 0
rw : ∀ (x : X), x ∉ F
⊢ F = ∅

Tactic:
rw [eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- 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 = 0
x : X
x_F : x ∈ F
⊢ IsDynNetIn T F U n {x}

Tactic:
have key := isDynNetIn_singleton T U n x_F
-- 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 = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n {x}
⊢ IsDynNetIn T F U n (↑{x} : Set X)

Tactic:
rw [← Finset.coe_singleton] at key

Premises used: Finset.coe_singleton
-- 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 = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n (↑{x} : Set X)
⊢ (↑(Finset.card (α := X) {x}) : ℕ∞) ≤ netMaxcard T F U n

Tactic:
replace key := key.card_le_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 = 0
x : X
x_F : x ∈ F
key : (↑(Finset.card (α := X) {x}) : ℕ∞) ≤ netMaxcard T F U n
⊢ LE.le (α := ℕ∞) 1 0

Tactic:
rw [Finset.card_singleton, Nat.cast_one, h] at key

Premises used: Nat.cast_one, Finset.card_singleton
-- 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 = 0
x : X
x_F : x ∈ F
key : LE.le (α := ℕ∞) 1 0
⊢ False

Tactic:
key.not_gt zero_lt_one

Premises used: zero_lt_one, LE.le.not_gt
-- 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 = 0
x : X
x_F : x ∈ F
key : LE.le (α := ℕ∞) 1 0
⊢ False

Tactic:
exact key.not_gt zero_lt_one

Premises used: zero_lt_one, LE.le.not_gt
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
rw : netMaxcard T F U n ≠ 0 ↔ F ≠ ∅
⊢ 1 ≤ netMaxcard T F U n ↔ F.Nonempty

Tactic:
rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n ≠ 0 ↔ F ≠ ∅

Tactic:
not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)

Premises used: not_iff_not, Iff.mpr, Dynamics.netMaxcard_eq_zero_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n ≠ 0 ↔ F ≠ ∅

Tactic:
exact not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)

Premises used: not_iff_not, Iff.mpr, Dynamics.netMaxcard_eq_zero_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
apply : ∀ (i : Finset X) (j : IsDynNetIn T F U 0 (↑i : Set X)), LE.le (α := ℕ∞) (↑i.card : ℕ∞) 1
⊢ netMaxcard T F U 0 = 1

Tactic:
apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F U 0).2 h)

Premises used: Iff.mpr, iSup₂_le, LE.le.antisymm, OfNat.ofNat, Dynamics.one_le_netMaxcard_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
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
⊢ ∀ (j : IsDynNetIn T F U 0 (↑s : Set X)), LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1

Tactic:
⟨_, s_net⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ ball x (dynEntourage T U 0)
⊢ (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ

Tactic:
simp only [ball, dynEntourage_zero, preimage_univ] at s_net

Premises used: UniformSpace.ball, Set.preimage_univ, Dynamics.dynEntourage_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
norm_cast : s.card ≤ 1
⊢ LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1

Tactic:
norm_cast
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
⊢ s.card ≤ 1

Tactic:
Finset.card_le_one.2 fun x x_s y y_s ↦ ?_

Premises used: Iff.mpr, Finset.card_le_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
refine : ∀ (x : X) (x_s : x ∈ s) (y : X) (y_s : y ∈ s), x = y
⊢ s.card ≤ 1

Tactic:
refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_

Premises used: Iff.mpr, Finset.card_le_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Tactic:
PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

Premises used: Set.mem_univ, Set.PairwiseDisjoint.elim_set
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Tactic:
exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

Premises used: Set.mem_univ, Set.PairwiseDisjoint.elim_set
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
apply : ∀ (i : Finset X) (j : IsDynNetIn T F univ n (↑i : Set X)), LE.le (α := ℕ∞) (↑i.card : ℕ∞) 1
⊢ netMaxcard T F univ n = 1

Tactic:
apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F univ n).2 h)

Premises used: Iff.mpr, iSup₂_le, Set.univ, LE.le.antisymm, Dynamics.one_le_netMaxcard_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
this :
  (↑s : Set X) ⊆ F →
    ∀ (s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ ball x (dynEntourage T univ n)),
      LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
⊢ ∀ (j : IsDynNetIn T F univ n (↑s : Set X)), LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1

Tactic:
⟨_, s_net⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ ball x (dynEntourage T univ n)
⊢ (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ

Tactic:
simp only [ball, dynEntourage_univ, preimage_univ] at s_net

Premises used: UniformSpace.ball, Set.preimage_univ, Dynamics.dynEntourage_univ
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
norm_cast : s.card ≤ 1
⊢ LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1

Tactic:
norm_cast
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
⊢ s.card ≤ 1

Tactic:
Finset.card_le_one.2 fun x x_s y y_s ↦ ?_

Premises used: Iff.mpr, Finset.card_le_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
refine : ∀ (x : X) (x_s : x ∈ s) (y : X) (y_s : y ∈ s), x = y
⊢ s.card ≤ 1

Tactic:
refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_

Premises used: Iff.mpr, Finset.card_le_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Tactic:
PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

Premises used: Set.mem_univ, Set.PairwiseDisjoint.elim_set
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Tactic:
exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

Premises used: Set.mem_univ, Set.PairwiseDisjoint.elim_set
-- 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 = ⊤ → ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
mpr : (∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card) → netMaxcard T F U n = ⊤
⊢ netMaxcard T F U n = ⊤ ↔ ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card

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 = ⊤
k : ℕ
mp :
  ∀ (h : ∀ b < ⊤, ∃ (i : { s : Finset X // IsDynNetIn T F U n (↑s : Set X) }), b < (↑(↑i : Finset X).card : ℕ∞))
    (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card

Tactic:
rw [netMaxcard, iSup_subtype', iSup_eq_top] at h

Premises used: iSup_subtype', iSup_eq_top, Dynamics.netMaxcard
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∀ b < ⊤, ∃ (i : { s : Finset X // IsDynNetIn T F U n (↑s : Set X) }), b < (↑(↑i : Finset X).card : ℕ∞)
k : ℕ
⊢ ∃ (i : { s : Finset X // IsDynNetIn T F U n (↑s : Set X) }), LT.lt (α := ℕ∞) (↑k : ℕ∞) (↑(↑i : Finset X).card : ℕ∞)

Tactic:
specialize h k (ENat.coe_lt_top k)

Premises used: Nat.cast, ENat.coe_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
h : ∃ (i : { s : Finset X // IsDynNetIn T F U n (↑s : Set X) }), LT.lt (α := ℕ∞) (↑k : ℕ∞) (↑(↑i : Finset X).card : ℕ∞)
⊢ ∃ (a : Finset X), IsDynNetIn T F U n (↑a : Set X) ∧ k < a.card

Tactic:
simp only [Nat.cast_lt, Subtype.exists, exists_prop] at h

Premises used: Subtype.exists, exists_prop, Nat.cast_lt
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
h : ∃ (a : Finset X), IsDynNetIn T F U n (↑a : Set X) ∧ k < a.card
mp :
  ∀ (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X)) (s_k : k < s.card),
    ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card

Tactic:
obtain ⟨s, s_net, s_k⟩ := h
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_k : k < s.card
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card

Tactic:
⟨s, s_net, s_k.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_k : k < s.card
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card

Tactic:
exact ⟨s, s_net, s_k.le⟩