awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)
⊢ LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
have s_net₁ : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
Tactic: simp only [ball, dynEntourage_zero, preimage_univ] at s_net
Cleared hypotheses: s_net
-- 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
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
⊢ LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
have norm_cast : s.card ≤ 1
Tactic: norm_cast
-- 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
left : (↑s : Set X) ⊆ F
s_net : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
⊢ s.card ≤ 1
have refine : ∀ (x : X) (x_s : x ∈ s) (y : X) (y_s : y ∈ s), x = y
Tactic: refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
⊢ netMaxcard T F univ n = 1
have apply : ∀ (i : Finset X) (j : IsDynNetIn T F univ n (↑i : Set X)), LE.le (α := ℕ∞) (↑i.card : ℕ∞) 1
Tactic: apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F univ n).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
n : ℕ
s : Finset X
⊢ ∀ (j : IsDynNetIn T F univ n (↑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 univ n)),
    LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
Tactic: ⟨_, s_net⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)
⊢ LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
have s_net₁ : (↑s : Set X).PairwiseDisjoint (α := Set X) fun (x : X) ↦ univ
Tactic: simp only [ball, dynEntourage_univ, preimage_univ] at s_net
Cleared hypotheses: s_net
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ LE.le (α := ℕ∞) (↑s.card : ℕ∞) 1
have norm_cast : s.card ≤ 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
have refine : ∀ (x : X) (x_s : x ∈ s) (y : X) (y_s : y ∈ s), x = y
Tactic: refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_
-- 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 = ⊤ ↔ ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
have mp : netMaxcard T F U n = ⊤ → ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
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 = ⊤ → ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
⊢ netMaxcard T F U n = ⊤ ↔ ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
have mpr : (∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ 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 : ℕ
h : netMaxcard T F U n = ⊤
k : ℕ
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
have 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
Tactic: rw [netMaxcard, iSup_subtype', iSup_eq_top] at h
Cleared hypotheses: h, k
-- 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 : ∀ 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
have h₁ : ∃ (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)
Cleared hypotheses: h
-- 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 k : ℕ
h : ∃ (i : { s : Finset X // IsDynNetIn T F U n (↑s : Set X) }), LT.lt (α := ℕ∞) (↑k : ℕ∞) (↑(↑i : Finset X).card : ℕ∞)
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
have h₁ : ∃ (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
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 k : ℕ
h : ∃ (a : Finset X), IsDynNetIn T F U n (↑a : Set X) ∧ k < a.card
⊢ ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
have 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
Tactic: obtain ⟨s, s_net, s_k⟩ := 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 : ℕ
h : ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
⊢ netMaxcard T F U n = ⊤
have mpr : ∀ (k : ℕ), (↑k : WithTop ℕ) < netMaxcard T F U n
Tactic: refine WithTop.eq_top_iff_forall_gt.2 fun k ↦ ?_
-- 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 : ∀ (k : ℕ), ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k ≤ s.card
k : ℕ
⊢ (↑k : WithTop ℕ) < netMaxcard T F U n
have h₁ : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k + 1 ≤ s.card
Tactic: specialize h (k + 1)
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 k : ℕ
h : ∃ (s : Finset X), IsDynNetIn T F U n (↑s : Set X) ∧ k + 1 ≤ s.card
⊢ (↑k : WithTop ℕ) < netMaxcard T F U n
have 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
Tactic: obtain ⟨s, s_net, 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 k : ℕ
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
have mpr : (↑k : WithTop ℕ) < (↑s.card : ℕ∞)
Tactic: apply s_net.card_le_netMaxcard.trans_lt'
-- 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 k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n (↑s : Set X)
s_card : k + 1 ≤ s.card
⊢ (↑k : WithTop ℕ) < (↑s.card : ℕ∞)
have mpr : k < s.card
Tactic: rw [ENat.some_eq_coe, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
⊢ netMaxcard T F U n ≤ coverMincard T F U n
have inl : ∀ (h : 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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ netMaxcard T F U n ≤ coverMincard T F U n
have inr : ∀ (h : 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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
have 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
Tactic: obtain ⟨t, t_cover, t_mincard⟩ := (coverMincard_finite_iff T F U n).1 h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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 ≤ coverMincard T F U n
have inr : netMaxcard T F U n ≤ (↑t.card : ℕ∞)
Tactic: rw [← t_mincard]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst : U.IsRefl
inst_1 : U.IsSymm
n : ℕ
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
have inl : ∀ (h : 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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
have inr : ∀ (h : 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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
have 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
Tactic: obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
have inr : coverMincard T F (U ○ U) n ≤ (↑s.card : ℕ∞)
Tactic: rw [← s_card]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ coverMincard T F (U ○ U) n ≤ (↑s.card : ℕ∞)
have inr : IsDynCoverOf T F (U ○ U) n (↑s : Set X)
Tactic: apply IsDynCoverOf.coverMincard_le_card
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ IsDynCoverOf T F (U ○ U) n (↑s : Set X)
have inr : F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
Tactic: rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
have inr : ∀ (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ False
have inr : ∀ (x : X) (x_F : x ∈ F) (x_uncov : x ∉ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)), False
Tactic: obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)
⊢ False
have x_uncov₁ : ∀ 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
Cleared hypotheses: x_uncov
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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))
have refine : ∀ j ∈ (↑s : Set X), x ≠ j → Disjoint (ball x (dynEntourage T U n)) (ball j (dynEntourage T U n))
Tactic: refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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))
have 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)
Tactic: refine fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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)
⊢ False
have larger_net : 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⟩)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
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))
⊢ False
have larger_net₁ : IsDynNetIn T F U n (↑(insert x s) : Set X)
Tactic: rw [← s.coe_insert x] at larger_net
Cleared hypotheses: larger_net
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ False
have inr : netMaxcard T F U n < (↑(insert x s).card : ℕ∞)
Tactic: apply larger_net.card_le_netMaxcard.not_gt
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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)
⊢ netMaxcard T F U n < (↑(insert x s).card : ℕ∞)
have inr : s.card < (insert x s).card
Tactic: rw [← s_card, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
have inr : ∀ (x_s : x ∈ s), False
Tactic: refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst : U.IsRefl
inst_1 : U.IsSymm
n : ℕ
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
have inl : ∀ (h : netMaxcard T F U n = ⊤), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
Tactic: classical
  -- WLOG, there exists a maximal dynamical net `s`.
  rcases eq_top_or_lt_top (netMaxcard T F U n) with h | h
  · exact h ▸ le_top
  obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
  rw [← s_card]
  apply IsDynCoverOf.coverMincard_le_card
  --  We have to check that `s` is a cover for `dynEntourage T F (U ○ U) n`.
  -- If `s` is not a cover, then we can add to `s` a point `x` which is not covered
  -- and get a new net. This contradicts the maximality of `s`.
  rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]
  by_contra h
  obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
  simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov
  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⟩)
  rw [← s.coe_insert x] at larger_net
  apply larger_net.card_le_netMaxcard.not_gt
  rw [← s_card, Nat.cast_lt]
  refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
  exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
have inr : ∀ (h : netMaxcard T F U n < ⊤), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
Tactic: classical
  -- WLOG, there exists a maximal dynamical net `s`.
  rcases eq_top_or_lt_top (netMaxcard T F U n) with h | h
  · exact h ▸ le_top
  obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
  rw [← s_card]
  apply IsDynCoverOf.coverMincard_le_card
  --  We have to check that `s` is a cover for `dynEntourage T F (U ○ U) n`.
  -- If `s` is not a cover, then we can add to `s` a point `x` which is not covered
  -- and get a new net. This contradicts the maximality of `s`.
  rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]
  by_contra h
  obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
  simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov
  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⟩)
  rw [← s.coe_insert x] at larger_net
  apply larger_net.card_le_netMaxcard.not_gt
  rw [← s_card, Nat.cast_lt]
  refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
  exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
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 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
have inr₂ : ∀ (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), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
Tactic: classical
  -- WLOG, there exists a maximal dynamical net `s`.
  rcases eq_top_or_lt_top (netMaxcard T F U n) with h | h
  · exact h ▸ le_top
  obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
  rw [← s_card]
  apply IsDynCoverOf.coverMincard_le_card
  --  We have to check that `s` is a cover for `dynEntourage T F (U ○ U) n`.
  -- If `s` is not a cover, then we can add to `s` a point `x` which is not covered
  -- and get a new net. This contradicts the maximality of `s`.
  rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]
  by_contra h
  obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
  simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov
  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⟩)
  rw [← s.coe_insert x] at larger_net
  apply larger_net.card_le_netMaxcard.not_gt
  rw [← s_card, Nat.cast_lt]
  refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
  exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))