awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 ≤ (↑s.card : ℕ∞)
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
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
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 ≤ (↑s.card : ℕ∞)
⊢ 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), IsDynCoverOf T F (U ○ U) n (↑s : Set X)
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
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
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 ≤ (↑s.card : ℕ∞)
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), IsDynCoverOf T F (U ○ U) n (↑s : Set X)
⊢ 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), F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ 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
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
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 ≤ (↑s.card : ℕ∞)
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), IsDynCoverOf T F (U ○ U) n (↑s : Set X)
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), F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ 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) (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)), False
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
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
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 ≤ (↑s.card : ℕ∞)
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), IsDynCoverOf T F (U ○ U) n (↑s : Set X)
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), F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
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) (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)),
    False
⊢ 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) (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
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
T : X → X
U : SetRel X X
⊢ netEntropyEntourage T ∅ U = ⊥
have rw : (expGrowthSup fun (n : ℕ) ↦ (↑(netMaxcard T ∅ U n) : ℝ≥0∞)) = expGrowthSup 0
Tactic: rw [netEntropyEntourage, ← expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑(netMaxcard T ∅ U n) : ℝ≥0∞)) = expGrowthSup 0
have e_u : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(netMaxcard T ∅ U n) : ℝ≥0∞)) 0
Tactic: congr
-- 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
⊢ 0 ≤ netEntropyInfEntourage T F U
have h₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)
Tactic: apply Monotone.expGrowthInf_nonneg
-- 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
h₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)
⊢ 0 ≤ netEntropyInfEntourage T F U
have h' : Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)) 0
Tactic: apply Monotone.expGrowthInf_nonneg
-- 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
⊢ Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(netMaxcard T F U n) : ℝ≥0∞)) 0
have h' : ∃ (x : ℕ), ¬(↑(netMaxcard T F U x) : ℝ≥0∞) = 0 x
Tactic: rw [ne_eq, funext_iff.not, not_forall]
-- 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
⊢ ∃ (x : ℕ), ¬(↑(netMaxcard T F U x) : ℝ≥0∞) = 0 x
have h₁ : ¬(↑(netMaxcard T F U 0) : ℝ≥0∞) = 0 0
Tactic: use 0
-- 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) : ℝ≥0∞) = 0 0
have h₁ : ¬Eq (α := ℝ≥0∞) 1 0
Tactic: rw [netMaxcard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyInfEntourage T F univ = 0
have rw : (expGrowthInf fun (n : ℕ) ↦ (↑(netMaxcard T F univ n) : ℝ≥0∞)) = expGrowthInf fun (x : ℕ) ↦ 1
Tactic: rw [← expGrowthInf_const one_ne_zero one_ne_top, netEntropyInfEntourage]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyEntourage T F univ = 0
have rw : (expGrowthSup fun (n : ℕ) ↦ (↑(netMaxcard T F univ n) : ℝ≥0∞)) = expGrowthSup fun (x : ℕ) ↦ 1
Tactic: rw [← expGrowthSup_const one_ne_zero one_ne_top, netEntropyEntourage]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
have a : coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
⊢ coverEntropyInf T F = ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
have a₁ : ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U ≤ coverEntropyInf T F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropyInf T F ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
have a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
Tactic: refine iSup₂_le fun U U_uni ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U ≤ coverEntropyInf T F
have a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), netEntropyInfEntourage T F U ≤ coverEntropyInf T F
Tactic: refine iSup₂_le fun U U_uni ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
have a : ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_symm : SetRel.IsSymm V) (V_U : V ○ V ⊆ U),
  coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
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
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
have this : SetRel.IsRefl V
Tactic: have := isRefl_of_mem_uniformity V_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_U : V ○ V ⊆ U
this : SetRel.IsRefl V
⊢ coverEntropyInfEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U
have apply : (fun (U : SetRel X X) ↦ coverEntropyInfEntourage T F U) (V ○ V) ≤ netEntropyInfEntourage T F V
Tactic: apply (coverEntropyInfEntourage_antitone T F V_U).trans (le_iSup₂_of_le V V_uni _)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyInfEntourage T F U ≤ coverEntropyInf T F
have a : (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropyInf T F
Tactic: apply (netEntropyInfEntourage_antitone T F SetRel.symmetrize_subset_self).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropyInf T F
have a : (fun (U : SetRel X X) ↦ netEntropyInfEntourage T F U) (SetRel.symmetrize U) ≤
  coverEntropyInfEntourage T F (SetRel.symmetrize U)
Tactic: apply (le_iSup₂ (SetRel.symmetrize U) (symmetrize_mem_uniformity U_uni)).trans'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropy T F = ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
have a : coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
a : coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
⊢ coverEntropy T F = ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
have a₁ : ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U ≤ coverEntropy T F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ coverEntropy T F ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
have a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
Tactic: refine iSup₂_le fun U U_uni ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U ≤ coverEntropy T F
have a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), netEntropyEntourage T F U ≤ coverEntropy T F
Tactic: refine iSup₂_le fun U U_uni ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
have a : ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_symm : SetRel.IsSymm V) (V_comp_U : V ○ V ⊆ U),
  coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
Tactic: obtain ⟨V, V_uni, V_symm, V_comp_U⟩ := comp_symm_mem_uniformity_sets U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_comp_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U
have apply : (fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V) ≤ netEntropyEntourage T F V
Tactic: apply (coverEntropyEntourage_antitone T F V_comp_U).trans (le_iSup₂_of_le V V_uni _)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SetRel.IsSymm V
V_comp_U : V ○ V ⊆ U
⊢ (fun (U : SetRel X X) ↦ coverEntropyEntourage T F U) (V ○ V) ≤ netEntropyEntourage T F V
have this : SetRel.IsRefl V
Tactic: have := isRefl_of_mem_uniformity V_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F
have a : (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropy T F
Tactic: apply (netEntropyEntourage_antitone T F SetRel.symmetrize_subset_self).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropy T F
have a : (fun (U : SetRel X X) ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤
  coverEntropyEntourage T F (SetRel.symmetrize U)
Tactic: apply (le_iSup₂ (SetRel.symmetrize U) (symmetrize_mem_uniformity U_uni)).trans'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (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
⊢ coverEntropyInf T F = ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
have rw : Eq (α := EReal) (⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U) (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
Tactic: rw [coverEntropyInf_eq_iSup_netEntropyInfEntourage T F]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (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
⊢ Eq (α := EReal) (⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U) (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
have apply : LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyInfEntourage T F i) (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
Tactic: apply (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩).antisymm'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (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
⊢ LE.le (α := EReal) (⨆ i ∈ 𝓤 X, netEntropyInfEntourage T F i)
    (⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i))
have refine : ∀ (U : SetRel X X) (U_uni : U ∈ 𝓤 X),
  netEntropyInfEntourage T F U ≤ ⨆ (i : ι), ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
Tactic: refine iSup₂_le fun U U_uni ↦ ?_