awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 (↑s : Set X)
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have obtain : ∀ (t : Finset X) (t_dyncover : IsDynCoverOf T F (V ○ V) (1 * n) (↑t : Set X)) (t_card : #t ≤ #s ^ n),
  ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
Tactic: obtain ⟨t, t_dyncover, t_card⟩ := this.iterate_le_pow F_inv n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 (↑s : Set X)
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) (1 * n) (↑t : Set X)
t_card : #t ≤ #s ^ n
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
have t_dyncover₁ : IsDynCoverOf T F (V ○ V) n (↑t : Set X)
Tactic: rw [one_mul n] at t_dyncover
Cleared hypotheses: t_dyncover, t_card
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n < ⊤ ↔ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = coverMincard T F U n
have refine : ∀ (h_fin : coverMincard T F U n < ⊤),
  ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = coverMincard T F U n
Tactic: refine ⟨fun h_fin ↦ ?_, fun ⟨s, _, s_coverMincard⟩ ↦ s_coverMincard ▸ WithTop.coe_lt_top s.card⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = coverMincard T F U n
have obtain : ∀ (k : ℕ) (k_min : (↑k : WithTop ℕ) = coverMincard T F U n),
  ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = coverMincard T F U n
Tactic: obtain ⟨k, k_min⟩ := WithTop.ne_top_iff_exists.1 h_fin.ne
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = coverMincard T F U n
have rw : ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = (↑k : WithTop ℕ)
Tactic: rw [← k_min]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = (↑k : WithTop ℕ)
have simp : ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k
Tactic: simp only [ENat.some_eq_coe, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
have by_contra : ∀ (h : ¬Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
h : ¬Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
⊢ False
have apply : Eq (α := ℕ∞) (↑k : ℕ∞) ⊤
Tactic: apply ENat.coe_ne_top k
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
h : ¬Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
⊢ Eq (α := ℕ∞) (↑k : ℕ∞) ⊤
have rw : ∀ (i : Finset X) (j : IsDynCoverOf T F U n (↑i : Set X)), Eq (α := ℕ∞) (↑(#i) : ℕ∞) ⊤
Tactic: rw [← ENat.some_eq_coe, k_min, coverMincard, iInf₂_eq_top]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
h : ¬Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
⊢ ∀ (i : Finset X) (j : IsDynCoverOf T F U n (↑i : Set X)), Eq (α := ℕ∞) (↑(#i) : ℕ∞) ⊤
have simp : ∀ (i : Finset X), ¬IsDynCoverOf T F U n (↑i : Set X)
Tactic: simp only [ENat.coe_ne_top, imp_false]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k
have this : Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
Tactic: have : Nonempty {s : Finset X // IsDynCoverOf T F U n s} := by
    by_contra h
    apply ENat.coe_ne_top k
    rw [← ENat.some_eq_coe, k_min, coverMincard, iInf₂_eq_top]
    simp only [ENat.coe_ne_top, imp_false]
    rw [nonempty_subtype, not_exists] at h
    exact h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
this : Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k
have key : Membership.mem (γ := Set ℕ∞)
  (range fun (s : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }) ↦ (↑(#(↑s : Finset X)) : ℕ∞))
  (⨅ (s : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), (↑(#(↑s : Finset X)) : ℕ∞))
Tactic: have key := ciInf_mem fun s : {s : Finset X // IsDynCoverOf T F U n s} ↦ (s.val.card : ℕ∞)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = coverMincard T F U n
this : Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
key :
  Membership.mem (γ := Set ℕ∞)
    (range fun (s : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }) ↦ (↑(#(↑s : Finset X)) : ℕ∞))
    (⨅ (s : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), (↑(#(↑s : Finset X)) : ℕ∞))
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k
have k_min₁ : (↑k : WithTop ℕ) = ⨅ (x : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), (↑(#(↑x : Finset X)) : ℕ∞)
Tactic: rw [coverMincard, iInf_subtype'] at k_min
Cleared hypotheses: k_min, this, key
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : (↑k : WithTop ℕ) = ⨅ (x : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), (↑(#(↑x : Finset X)) : ℕ∞)
this : Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }
key :
  Membership.mem (γ := Set ℕ∞)
    (range fun (s : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }) ↦ (↑(#(↑s : Finset X)) : ℕ∞))
    (⨅ (s : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), (↑(#(↑s : Finset X)) : ℕ∞))
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k
have key₁ : ∃ (a : Finset X) (b : IsDynCoverOf T F U n (↑a : Set X)),
  (↑(#(↑(Subtype.mk (p := fun (a : Finset X) ↦ IsDynCoverOf T F U n (↑a : Set X)) a b) : Finset X)) : ℕ∞) =
    (↑k : WithTop ℕ)
Tactic: rw [← k_min, mem_range, Subtype.exists] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ coverMincard T ∅ U n = 0
have rw : coverMincard T ∅ U n ≤ 0
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ 1 ≤ coverMincard T F U n ↔ F.Nonempty
have rw : coverMincard T F U n = 0 ↔ F = ∅
Tactic: rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty, not_iff_not]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ coverMincard T F U 0 = 1
have apply : coverMincard T F U 0 ≤ 1
Tactic: apply le_antisymm _ ((one_le_coverMincard_iff T F U 0).2 h)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ coverMincard T F U 0 ≤ 1
have obtain : ∀ x ∈ F, coverMincard T F U 0 ≤ 1
Tactic: obtain ⟨x, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h : x ∈ F
⊢ coverMincard T F U 0 ≤ 1
have this : IsDynCoverOf T F U 0 {x}
Tactic: have := isDynCoverOf_zero T F U (singleton_nonempty x)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h : x ∈ F
this : IsDynCoverOf T F U 0 {x}
⊢ coverMincard T F U 0 ≤ 1
have this₁ : IsDynCoverOf T F U 0 (↑{x} : Set X)
Tactic: rw [← Finset.coe_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h : x ∈ F
this : IsDynCoverOf T F U 0 (↑{x} : Set X)
⊢ coverMincard T F U 0 ≤ 1
have apply : Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
Tactic: apply this.coverMincard_le_card.trans_eq
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h : x ∈ F
this : IsDynCoverOf T F U 0 (↑{x} : Set X)
⊢ Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
have rw : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
Tactic: rw [Finset.card_singleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h : x ∈ F
this : IsDynCoverOf T F U 0 (↑{x} : Set X)
rw : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
⊢ Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
have rw₁ : Eq (α := ℕ∞) 1 1
Tactic: rw [Finset.card_singleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
⊢ coverMincard T F univ n = 1
have apply : coverMincard T F univ n ≤ 1
Tactic: apply le_antisymm _ ((one_le_coverMincard_iff T F univ n).2 h)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
⊢ coverMincard T F univ n ≤ 1
have obtain : ∀ x ∈ F, coverMincard T F univ n ≤ 1
Tactic: obtain ⟨x, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
⊢ coverMincard T F univ n ≤ 1
have this : IsDynCoverOf T F univ n {x}
Tactic: have := isDynCoverOf_univ T F n (singleton_nonempty x)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
this : IsDynCoverOf T F univ n {x}
⊢ coverMincard T F univ n ≤ 1
have this₁ : IsDynCoverOf T F univ n (↑{x} : Set X)
Tactic: rw [← Finset.coe_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
this : IsDynCoverOf T F univ n (↑{x} : Set X)
⊢ coverMincard T F univ n ≤ 1
have apply : Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
Tactic: apply this.coverMincard_le_card.trans_eq
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
this : IsDynCoverOf T F univ n (↑{x} : Set X)
⊢ Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
have rw : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
Tactic: rw [Finset.card_singleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
this : IsDynCoverOf T F univ n (↑{x} : Set X)
rw : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
⊢ Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
have rw₁ : Eq (α := ℕ∞) 1 1
Tactic: rw [Finset.card_singleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inl : ∀ (F_inv : MapsTo T ∅ ∅), coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ n
Tactic: rcases F.eq_empty_or_nonempty with rfl | F_nonempty
Cleared hypotheses: F, F_inv
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
inl : ∀ (F_inv : MapsTo T ∅ ∅), coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr : ∀ (F_nonempty : F.Nonempty), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Tactic: rcases F.eq_empty_or_nonempty with rfl | F_nonempty
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr : coverMincard T F (U ○ U) (m * 0) ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
inr : coverMincard T F (U ○ U) (m * 0) ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr₁ : ∀ (hn : n ≠ 0), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * 0) ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
have inr : coverMincard T F (U ○ U) 0 ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
Tactic: rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m : ℕ
F_nonempty : F.Nonempty
inr : coverMincard T F (U ○ U) 0 ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
⊢ coverMincard T F (U ○ U) (m * 0) ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
have inr₁ : 1 ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
Tactic: rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m : ℕ
F_nonempty : F.Nonempty
inr : coverMincard T F (U ○ U) 0 ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
inr₁ : 1 ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
⊢ coverMincard T F (U ○ U) (m * 0) ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
have inr₂ : LE.le (α := ℕ∞) 1 1
Tactic: rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr : ∀ (h : coverMincard T F U m = ⊤), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Tactic: rcases eq_top_or_lt_top (coverMincard T F U m) with h | h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
inr : ∀ (h : coverMincard T F U m = ⊤), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr₁ : ∀ (h : coverMincard T F U m < ⊤), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Tactic: rcases eq_top_or_lt_top (coverMincard T F U m) with h | h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U m (↑s : Set X)) (s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m),
  coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Tactic: obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U m).1 h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m (↑s : Set X)
s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr : ∀ (t : Finset X) (t_cover : IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X)) (t_sn : #t ≤ #s ^ n),
  coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Tactic: obtain ⟨t, t_cover, t_sn⟩ := s_cover.iterate_le_pow F_inv n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m (↑s : Set X)
s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X)
t_sn : #t ≤ #s ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
have inr : coverMincard T F (U ○ U) (m * n) ≤ HPow.hPow (α := ℕ∞) (↑(#s) : ℕ∞) n
Tactic: rw [← s_coverMincard]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ coverMincard T F U n < ⊤
have obtain : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U n (↑s : Set X)), coverMincard T F U n < ⊤
Tactic: obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_uniformContinuous F_comp h U_uni n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ coverMincard T F U n < ⊤
have obtain : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U n (↑s : Set X)), coverMincard T F U n < ⊤
Tactic: obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv U_uni n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty
have by_contra! : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅), False
Tactic: by_contra! ⟨x, x_s, ball_empt⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
⊢ ∃ y_1 ∈ (↑(s.erase x) : Set X), (y, y_1) ∈ dynEntourage T U n
have h₁ : ∃ y_1 ∈ (↑s : Set X), (y, y_1) ∈ dynEntourage T U n
Tactic: specialize h y_F
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ y_1 ∈ (↑s : Set X), (y, y_1) ∈ dynEntourage T U n
⊢ ∃ y_1 ∈ (↑(s.erase x) : Set X), (y, y_1) ∈ dynEntourage T U n
have h₁ : ∃ y_1 ∈ s, (y, y_1) ∈ dynEntourage T U n
Tactic: simp only [s.mem_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ y_1 ∈ s, (y, y_1) ∈ dynEntourage T U n
⊢ ∃ y_1 ∈ (↑(s.erase x) : Set X), (y, y_1) ∈ dynEntourage T U n
have simp : ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n
Tactic: simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ y_1 ∈ s, (y, y_1) ∈ dynEntourage T U n
⊢ ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n
have obtain : ∀ (z : X) (z_s : z ∈ s) (hz : (y, z) ∈ dynEntourage T U n),
  ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n
Tactic: obtain ⟨z, z_s, hz⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
⊢ ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n
have refine : ∀ (z_x : z = x), Membership.mem (γ := Set X) ∅ y
Tactic: refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
⊢ Membership.mem (γ := Set X) ∅ y
have rw : y ∈ F ∩ ball x (dynEntourage T U n)
Tactic: rw [← ball_empt]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.CoverEntropy (hypothesis)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T U n)
have hz₁ : (y, x) ∈ dynEntourage T U n
Tactic: rw [z_x] at hz
Cleared hypotheses: hz, z_x