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

Tactic:
WithTop.eq_top_iff_forall_gt.2 fun k ↦ ?_

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

Tactic:
refine WithTop.eq_top_iff_forall_gt.2 fun k ↦ ?_

Premises used: Iff.mpr, WithTop.eq_top_iff_forall_gt
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
k : ℕ
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k + 1 ≤ s.card

Tactic:
specialize h (k + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
h : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k + 1 ≤ s.card
mpr :
  ∀ (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X)) (s_card : k + 1 ≤ s.card),
    (↑k : WithTop ℕ) < netMaxcard T F U n
⊢ (↑k : WithTop ℕ) < netMaxcard T F U n

Tactic:
obtain ⟨s, s_net, s_card⟩ := 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_card : k + 1 ≤ s.card
mpr : (↑k : WithTop ℕ) < (↑s.card : ℕ∞)
⊢ (↑k : WithTop ℕ) < netMaxcard T F U n

Tactic:
apply s_net.card_le_netMaxcard.trans_lt'

Premises used: Dynamics.IsDynNetIn.card_le_netMaxcard, LE.le.trans_lt'
-- 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_card : k + 1 ≤ s.card
mpr : k < s.card
⊢ (↑k : WithTop ℕ) < (↑s.card : ℕ∞)

Tactic:
rw [ENat.some_eq_coe, Nat.cast_lt]

Premises used: ENat.some_eq_coe, 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 : ℕ
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : k + 1 ≤ s.card
⊢ k < s.card

Tactic:
(lt_add_one k).trans_le s_card

Premises used: lt_add_one, LT.lt.trans_le
-- 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_card : k + 1 ≤ s.card
⊢ k < s.card

Tactic:
exact (lt_add_one k).trans_le s_card

Premises used: lt_add_one, LT.lt.trans_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
inl : ∀ (h : coverMincard T F U n = ⊤), netMaxcard T F U n ≤ coverMincard T F U n
inr : ∀ (h : coverMincard T F U n < ⊤), netMaxcard T F U n ≤ coverMincard T F U n
⊢ netMaxcard T F U n ≤ coverMincard T F U n

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

Premises used: Dynamics.coverMincard, eq_top_or_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n = ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
h ▸ le_top

Premises used: Eq.rec, le_top, Eq.symm
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n = ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
exact h ▸ le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
inr :
  ∀ (t : Finset X) (t_cover : IsDynCoverOf T F U n (↑t : Set X)) (t_mincard : (↑t.card : ℕ∞) = coverMincard T F U n),
    netMaxcard T F U n ≤ coverMincard T F U n
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
obtain ⟨t, t_cover, t_mincard⟩ := (coverMincard_finite_iff T F U n).1 h

Premises used: Iff.mp, Dynamics.coverMincard_finite_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n (↑t : Set X)
t_mincard : (↑t.card : ℕ∞) = coverMincard T F U n
inr : netMaxcard T F U n ≤ (↑t.card : ℕ∞)
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
rw [← t_mincard]
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n (↑t : Set X)
t_mincard : (↑t.card : ℕ∞) = coverMincard T F U n
⊢ netMaxcard T F U n ≤ (↑t.card : ℕ∞)

Tactic:
iSup₂_le fun s s_net ↦ Nat.cast_le.2 (s_net.card_le_card_of_isDynCoverOf t_cover)

Premises used: Iff.mpr, iSup₂_le, Dynamics.IsDynNetIn.card_le_card_of_isDynCoverOf, Nat.cast_le, Dynamics.netMaxcard
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n (↑t : Set X)
t_mincard : (↑t.card : ℕ∞) = coverMincard T F U n
⊢ netMaxcard T F U n ≤ (↑t.card : ℕ∞)

Tactic:
exact iSup₂_le fun s s_net ↦ Nat.cast_le.2 (s_net.card_le_card_of_isDynCoverOf t_cover)

Premises used: Iff.mpr, iSup₂_le, Nat.cast_le
-- 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
n : ℕ
inl : ∀ (h : netMaxcard T F U n = ⊤), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
inr : ∀ (h : netMaxcard T F U n < ⊤), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

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

Premises used: eq_top_or_lt_top, Dynamics.netMaxcard
-- 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
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
h ▸ le_top

Premises used: Eq.rec, le_top, Eq.symm
-- 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
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
exact h ▸ le_top
-- 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
n : ℕ
h : netMaxcard T F U n < ⊤
inr :
  ∀ (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X)) (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n),
    coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h

Premises used: Dynamics.netMaxcard_finite_iff, Iff.mp
-- 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
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
inr : coverMincard T F (U ○ U) n ≤ (↑s.card : ℕ∞)
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
rw [← s_card]
-- 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
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
inr : IsDynCoverOf T F (U ○ U) n (↑s : Set X)
⊢ coverMincard T F (U ○ U) n ≤ (↑s.card : ℕ∞)

Tactic:
apply IsDynCoverOf.coverMincard_le_card

Premises used: Dynamics.IsDynCoverOf.coverMincard_le_card
-- 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
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
inr : F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
⊢ IsDynCoverOf T F (U ○ U) n (↑s : Set X)

Tactic:
rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]

Premises used: UniformSpace.isCover_iff_subset_iUnion_ball, Dynamics.IsDynCoverOf
-- 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
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
inr : ∀ (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)), False
⊢ F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)

Tactic:
by_contra h
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
inr : ∀ (x : X) (x_F : x ∈ F) (x_uncov : x ∉ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)), False
⊢ False

Tactic:
obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h

Premises used: Set.not_subset, Iff.mp
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : x ∉ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
⊢ ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)

Tactic:
simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov

Premises used: Set.mem_iUnion, not_exists, exists_prop, not_and, Finset.mem_coe
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
⊢ IsDynNetIn T F U n (insert x (↑s : Set X))

Tactic:
⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Dynamics.IsDynNetIn, Set.pairwiseDisjoint_insert, Set.insert_subset
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
refine : ∀ j ∈ (↑s : Set X), x ≠ j → Disjoint (ball x (dynEntourage T U n)) (ball j (dynEntourage T U n))
⊢ IsDynNetIn T F U n (insert x (↑s : Set X))

Tactic:
refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
⊢ ∀ j ∈ (↑s : Set X), x ≠ j → Disjoint (ball x (dynEntourage T U n)) (ball j (dynEntourage T U n))

Tactic:
fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_

Premises used: Iff.mpr, Set.disjoint_left
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
refine :
  ∀ (y : X) (y_s : y ∈ (↑s : Set X)),
    x ≠ y →
      ∀ (z : X) (z_x : z ∈ ball x (dynEntourage T U n)) (z_y : z ∈ ball y (dynEntourage T U n)),
        x ∈ ball y (dynEntourage T (U ○ U) n)
⊢ ∀ j ∈ (↑s : Set X), x ≠ j → Disjoint (ball x (dynEntourage T U n)) (ball j (dynEntourage T U n))

Tactic:
refine fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_

Premises used: Iff.mpr, Set.disjoint_left
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
y : X
y_s : y ∈ (↑s : Set X)
h_2 : x ≠ y
z : X
z_x : z ∈ ball x (dynEntourage T U n)
z_y : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
mem_ball_dynEntourage_comp T n x y (nonempty_of_mem ⟨z_x, z_y⟩)

Premises used: And.intro, Set.nonempty_of_mem, Dynamics.mem_ball_dynEntourage_comp
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
y : X
y_s : y ∈ (↑s : Set X)
h_2 : x ≠ y
z : X
z_x : z ∈ ball x (dynEntourage T U n)
z_y : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
exact mem_ball_dynEntourage_comp T n x y (nonempty_of_mem ⟨z_x, z_y⟩)

Premises used: And.intro, Set.nonempty_of_mem, Dynamics.mem_ball_dynEntourage_comp
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
⊢ IsDynNetIn T F U n (insert x (↑s : Set X))

Tactic:
have larger_net : IsDynNetIn T F U n (insert x s) := by
    refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩
    refine fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_
    exact mem_ball_dynEntourage_comp T n x y (nonempty_of_mem ⟨z_x, z_y⟩)
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (insert x (↑s : Set X))
⊢ IsDynNetIn T F U n (↑(insert x s) : Set X)

Tactic:
rw [← s.coe_insert x] at larger_net

Premises used: Finset.coe_insert
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (↑(insert x s) : Set X)
inr : netMaxcard T F U n < (↑(insert x s).card : ℕ∞)
⊢ False

Tactic:
apply larger_net.card_le_netMaxcard.not_gt

Premises used: Dynamics.IsDynNetIn.card_le_netMaxcard, LE.le.not_gt
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (↑(insert x s) : Set X)
inr : s.card < (insert x s).card
⊢ netMaxcard T F U n < (↑(insert x s).card : ℕ∞)

Tactic:
rw [← s_card, Nat.cast_lt]

Premises used: Nat.cast_lt
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (↑(insert x s) : Set X)
⊢ s.card < (insert x s).card

Tactic:
(lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm

Premises used: lt_add_one, Finset.card_insert_of_notMem, LT.lt.trans_eq, Finset.card, Eq.symm
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (↑(insert x s) : Set X)
inr : ∀ (x_s : x ∈ s), False
⊢ s.card < (insert x s).card

Tactic:
refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm

Premises used: lt_add_one, Finset.card_insert_of_notMem, LT.lt.trans_eq, Finset.card, Eq.symm
-- 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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (↑(insert x s) : Set X)
x_s : x ∈ s
⊢ False

Tactic:
x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))

Premises used: UniformSpace.ball_mono, SetRel.left_subset_comp, Dynamics.dynEntourage, SetRel.rfl, Dynamics.dynEntourage_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
n : ℕ
h_1 : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (↑(insert x s) : Set X)
x_s : x ∈ s
⊢ False

Tactic:
exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))

Premises used: UniformSpace.ball_mono, SetRel.left_subset_comp, Dynamics.dynEntourage, SetRel.rfl, Dynamics.dynEntourage_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
⊢ Antitone (β := EReal) fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U

Tactic:
fun _ _ U_V ↦ expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (netMaxcard_antitone T F n U_V)

Premises used: ExpGrowth.expGrowthInf_monotone, Dynamics.netMaxcard_antitone, ENat.toENNReal_mono, Antitone, Dynamics.netEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
⊢ Antitone (β := EReal) fun (U : SetRel X X) ↦ netEntropyEntourage T F U

Tactic:
fun _ _ U_V ↦ expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (netMaxcard_antitone T F n U_V)

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

Tactic:
expGrowthInf_le_expGrowthSup

Premises used: Dynamics.netEntropyEntourage, Dynamics.netEntropyInfEntourage, ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
rw : (expGrowthSup fun (n : ℕ) ↦ (↑(netMaxcard T ∅ U n) : ℝ≥0∞)) = expGrowthSup 0
⊢ netEntropyEntourage T ∅ U = ⊥

Tactic:
rw [netEntropyEntourage, ← expGrowthSup_zero]

Premises used: Dynamics.netEntropyEntourage, ExpGrowth.expGrowthSup_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
e_u : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(netMaxcard T ∅ U n) : ℝ≥0∞)) 0
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑(netMaxcard T ∅ U n) : ℝ≥0∞)) = expGrowthSup 0

Tactic:
congr
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(netMaxcard T ∅ U n) : ℝ≥0∞)) 0

Tactic:
simp only [netMaxcard_empty, ENat.toENNReal_zero, Pi.zero_def]

Premises used: Dynamics.netMaxcard_empty, ENat.toENNReal_zero, Pi.zero_def
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ netEntropyInfEntourage T ∅ U = ⊥

Tactic:
eq_bot_mono (netEntropyInfEntourage_le_netEntropyEntourage T ∅ U) netEntropyEntourage_empty

Premises used: Dynamics.netEntropyEntourage_empty, Dynamics.netEntropyInfEntourage_le_netEntropyEntourage, eq_bot_mono, EmptyCollection.emptyCollection
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)
h' : Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)) 0
⊢ 0 ≤ netEntropyInfEntourage T F U

Tactic:
apply Monotone.expGrowthInf_nonneg

Premises used: Monotone.expGrowthInf_nonneg
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)

Tactic:
fun _ _ m_n ↦ ENat.toENNReal_mono (netMaxcard_monotone_time T F U m_n)

Premises used: Monotone, ENat.toENNReal_mono, Dynamics.netMaxcard_monotone_time
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)

Tactic:
exact fun _ _ m_n ↦ ENat.toENNReal_mono (netMaxcard_monotone_time T F U m_n)

Premises used: ENat.toENNReal_mono, Dynamics.netMaxcard_monotone_time
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h' : ∃ (x : ℕ), ¬(↑(netMaxcard T F U x) : ℝ≥0∞) = 0 x
⊢ Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)) 0

Tactic:
rw [ne_eq, funext_iff.not, not_forall]

Premises used: funext_iff, Iff.not, ne_eq, Classical.not_forall
-- Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h₁ : ¬(↑(netMaxcard T F U 0) : ℝ≥0∞) = 0 0
⊢ ∃ (x : ℕ), ¬(↑(netMaxcard T F U x) : ℝ≥0∞) = 0 x

Tactic:
use 0