awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 : ℕ
V : SetRel X X
hV : V ∈ 𝓤 X
hVsymm : V.IsSymm
hVU : V ⊆ U
uni_ite : dynEntourage T V n ∈ 𝓤 X
openCover : (x : X) → Set X := fun (x : X) ↦ ball x (dynEntourage T V n)
s : Finset X
left : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, openCover x
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)

Tactic:
⟨s, .of_entourage_subset hVU <| .of_subset_iUnion_ball s_cover⟩

Premises used: Dynamics.IsDynCoverOf.of_entourage_subset, SetRel.IsCover.of_subset_iUnion_ball, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 : ℕ
V : SetRel X X
hV : V ∈ 𝓤 X
hVsymm : V.IsSymm
hVU : V ⊆ U
uni_ite : dynEntourage T V n ∈ 𝓤 X
openCover : (x : X) → Set X := fun (x : X) ↦ ball x (dynEntourage T V n)
s : Finset X
left : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, openCover x
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)

Tactic:
exact ⟨s, .of_entourage_subset hVU <| .of_subset_iUnion_ball s_cover⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 : ℕ
obtain :
  ∀ (V : SetRel X X) (V_uni : V ∈ 𝓤 X) (V_symm : V.IsSymm) (V_U : V ○ V ⊆ U),
    ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)

Tactic:
obtain ⟨(V : SetRel X X), V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni

Premises used: SetRel, comp_symm_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
obtain :
  ∀ (s : Finset X),
    (∀ x ∈ s, x ∈ F) → ∀ (s_cover : F ⊆ ⋃ x ∈ s, ball x V), ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)

Tactic:
obtain ⟨s, _, s_cover⟩ := F_comp.elim_nhds_subcover (ball · V)
    fun (x : X) _ ↦ ball_mem_nhds x V_uni

Premises used: UniformSpace.ball_mem_nhds, UniformSpace.ball, IsCompact.elim_nhds_subcover
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
⊢ F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T V 1)

Tactic:
simpa using s_cover
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
⊢ IsDynCoverOf T F V 1 (↑s : Set X)

Tactic:
have : IsDynCoverOf T F V 1 s := .of_subset_iUnion_ball <| by simpa using s_cover
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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)
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)
⊢ ∃ (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

Premises used: Dynamics.IsDynCoverOf.iterate_le_pow
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
⊢ IsDynCoverOf T F (V ○ V) n (↑t : Set X)

Tactic:
rw [one_mul n] at t_dyncover

Premises used: one_mul
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
t_dyncover₁ : IsDynCoverOf T F (V ○ V) n (↑t : Set X)
⊢ #t ≤ #s ^ n

Tactic:
rw [one_mul n] at t_dyncover

Premises used: one_mul
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) n (↑t : Set X)
t_card : #t ≤ #s ^ n
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)

Tactic:
⟨t, t_dyncover.of_entourage_subset V_U⟩

Premises used: Dynamics.IsDynCoverOf.of_entourage_subset, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) n (↑t : Set X)
t_card : #t ≤ #s ^ n
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X)

Tactic:
exact ⟨t, t_dyncover.of_entourage_subset V_U⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
⊢ coverMincard T F U n ≤ (↑(#s) : ℕ∞)

Tactic:
iInf₂_le s h

Premises used: iInf₂_le, Dynamics.coverMincard
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
⊢ Monotone (β := ℕ∞) fun (n : ℕ) ↦ coverMincard T F U n

Tactic:
fun _ _ m_n ↦ biInf_mono fun _ h ↦ h.of_le m_n

Premises used: Monotone, Dynamics.coverMincard, biInf_mono, Dynamics.IsDynCoverOf.of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
n : ℕ
⊢ Antitone (β := ℕ∞) fun (U : SetRel X X) ↦ coverMincard T F U n

Tactic:
fun _ _ U_V ↦ biInf_mono fun _ h ↦ h.of_entourage_subset U_V

Premises used: Dynamics.IsDynCoverOf.of_entourage_subset, Antitone, Dynamics.coverMincard, biInf_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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

Tactic:
⟨fun h_fin ↦ ?_, fun ⟨s, _, s_coverMincard⟩ ↦ s_coverMincard ▸ WithTop.coe_lt_top s.card⟩

Premises used: WithTop.coe_lt_top, Eq.rec, Dynamics.coverMincard, LT.lt, Iff.intro, Finset.card, Top.top, _private.0.Dynamics.coverMincard_finite_iff.match_1
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
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
⊢ 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⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
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
⊢ ∃ (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

Premises used: WithTop.ne_top_iff_exists, Iff.mp, LT.lt.ne
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
rw : ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = (↑k : WithTop ℕ)
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = coverMincard T F U n

Tactic:
rw [← k_min]
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
simp : ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ (↑(#s) : ℕ∞) = (↑k : WithTop ℕ)

Tactic:
simp only [ENat.some_eq_coe, Nat.cast_inj]

Premises used: ENat.some_eq_coe, Nat.cast_inj
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
by_contra : ∀ (h : ¬Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), False
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }

Tactic:
by_contra h
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) }
apply : Eq (α := ℕ∞) (↑k : ℕ∞) ⊤
⊢ False

Tactic:
apply ENat.coe_ne_top k

Premises used: ENat.coe_ne_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) }
rw : ∀ (i : Finset X) (j : IsDynCoverOf T F U n (↑i : Set X)), Eq (α := ℕ∞) (↑(#i) : ℕ∞) ⊤
⊢ Eq (α := ℕ∞) (↑k : ℕ∞) ⊤

Tactic:
rw [← ENat.some_eq_coe, k_min, coverMincard, iInf₂_eq_top]

Premises used: ENat.some_eq_coe, iInf₂_eq_top, Dynamics.coverMincard
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) }
simp : ∀ (i : Finset X), ¬IsDynCoverOf T F U n (↑i : Set X)
⊢ ∀ (i : Finset X) (j : IsDynCoverOf T F U n (↑i : Set X)), Eq (α := ℕ∞) (↑(#i) : ℕ∞) ⊤

Tactic:
simp only [ENat.coe_ne_top, imp_false]

Premises used: imp_false, ENat.coe_ne_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) }
⊢ ∀ (x : Finset X), ¬IsDynCoverOf T F U n (↑x : Set X)

Tactic:
rw [nonempty_subtype, not_exists] at h

Premises used: not_exists, nonempty_subtype
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 : ∀ (x : Finset X), ¬IsDynCoverOf T F U n (↑x : Set X)
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n (↑i : Set X)

Tactic:
h
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 : ∀ (x : Finset X), ¬IsDynCoverOf T F U n (↑x : Set X)
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n (↑i : Set X)

Tactic:
exact h
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) }

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
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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) }
⊢ 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 : ℕ∞)
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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)) : ℕ∞))
⊢ (↑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

Premises used: iInf_subtype', Dynamics.coverMincard
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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)) : ℕ∞))
k_min₁ : (↑k : WithTop ℕ) = ⨅ (x : { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }), (↑(#(↑x : Finset X)) : ℕ∞)
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Finset X // IsDynCoverOf T F U n (↑s : Set X) }

Tactic:
rw [coverMincard, iInf_subtype'] at k_min

Premises used: iInf_subtype', Dynamics.coverMincard
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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)) : ℕ∞))
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) }
⊢ 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:
rw [coverMincard, iInf_subtype'] at k_min

Premises used: iInf_subtype', Dynamics.coverMincard
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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)) : ℕ∞))
⊢ ∃ (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

Premises used: Set.mem_range, Subtype.exists
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 :
  ∃ (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 ℕ)
⊢ ∃ (a : Finset X), IsDynCoverOf T F U n (↑a : Set X) ∧ #a = k

Tactic:
simp only [ENat.some_eq_coe, Nat.cast_inj, exists_prop] at key

Premises used: ENat.some_eq_coe, Nat.cast_inj, exists_prop
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 : ∃ (a : Finset X), IsDynCoverOf T F U n (↑a : Set X) ∧ #a = k
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k

Tactic:
key
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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 : ∃ (a : Finset X), IsDynCoverOf T F U n (↑a : Set X) ∧ #a = k
⊢ ∃ (s : Finset X), IsDynCoverOf T F U n (↑s : Set X) ∧ #s = k

Tactic:
exact key
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
rw : coverMincard T ∅ U n ≤ 0
⊢ coverMincard T ∅ U n = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ Membership.mem (γ := Set ℕ∞) (range fun (s : Finset X) ↦ ⨅ (_ : IsDynCoverOf T ∅ U n (↑s : Set X)), (↑(#s) : ℕ∞)) 0

Tactic:
simp [IsDynCoverOf]

Premises used: Dynamics.IsDynCoverOf
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ coverMincard T ∅ U n ≤ 0

Tactic:
exact sInf_le (by simp [IsDynCoverOf])

Premises used: sInf_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n = 0 ↔ F = ∅

Tactic:
simp [coverMincard, ENat.iInf_eq_zero]

Premises used: Dynamics.coverMincard, ENat.iInf_eq_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
rw : coverMincard T F U n = 0 ↔ F = ∅
⊢ 1 ≤ coverMincard T F U n ↔ F.Nonempty

Tactic:
rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty, not_iff_not]

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

Tactic:
coverMincard_eq_zero_iff T F U n

Premises used: Dynamics.coverMincard_eq_zero_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n = 0 ↔ F = ∅

Tactic:
exact coverMincard_eq_zero_iff T F U n

Premises used: Dynamics.coverMincard_eq_zero_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
apply : coverMincard T F U 0 ≤ 1
⊢ coverMincard T F U 0 = 1

Tactic:
apply le_antisymm _ ((one_le_coverMincard_iff T F U 0).2 h)

Premises used: Iff.mpr, Dynamics.one_le_coverMincard_iff, le_antisymm, OfNat.ofNat
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
obtain : ∀ x ∈ F, coverMincard T F U 0 ≤ 1
⊢ coverMincard T F U 0 ≤ 1

Tactic:
obtain ⟨x, _⟩ := h
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h : x ∈ F
⊢ IsDynCoverOf T F U 0 {x}

Tactic:
have := isDynCoverOf_zero T F U (singleton_nonempty x)
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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}
⊢ IsDynCoverOf T F U 0 (↑{x} : Set X)

Tactic:
rw [← Finset.coe_singleton] at this

Premises used: Finset.coe_singleton
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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)
apply : Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
⊢ coverMincard T F U 0 ≤ 1

Tactic:
apply this.coverMincard_le_card.trans_eq

Premises used: LE.le.trans_eq, Dynamics.IsDynCoverOf.coverMincard_le_card
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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
rw₁ rw₂ : Eq (α := ℕ∞) 1 1
⊢ Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1

Tactic:
rw [Finset.card_singleton, Nat.cast_one]

Premises used: Nat.cast_one, Finset.card_singleton
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
apply : coverMincard T F univ n ≤ 1
⊢ coverMincard T F univ n = 1

Tactic:
apply le_antisymm _ ((one_le_coverMincard_iff T F univ n).2 h)

Premises used: Iff.mpr, Dynamics.one_le_coverMincard_iff, Set.univ, le_antisymm
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
obtain : ∀ x ∈ F, coverMincard T F univ n ≤ 1
⊢ coverMincard T F univ n ≤ 1

Tactic:
obtain ⟨x, _⟩ := h
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
⊢ IsDynCoverOf T F univ n {x}

Tactic:
have := isDynCoverOf_univ T F n (singleton_nonempty x)
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
this : IsDynCoverOf T F univ n {x}
⊢ IsDynCoverOf T F univ n (↑{x} : Set X)

Tactic:
rw [← Finset.coe_singleton] at this

Premises used: Finset.coe_singleton
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
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)
apply : Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1
⊢ coverMincard T F univ n ≤ 1

Tactic:
apply this.coverMincard_le_card.trans_eq

Premises used: LE.le.trans_eq, Dynamics.IsDynCoverOf.coverMincard_le_card