-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma exists_isDynCoverOf_of_isCompact_invariant [UniformSpace X] {T : X → X} {F : Set X}
    (F_comp : IsCompact F) (F_inv : MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) (n : ℕ) :
    ∃ s : Finset X, IsDynCoverOf T F U n s

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
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
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) n ↑t
t_card : t.card ≤ s.card ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
exact ⟨t, t_dyncover.of_entourage_subset V_U⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
rcases comp_symm_mem_uniformity_sets U_uni with ⟨V, V_uni, V_symm, V_U⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
⊢ ∃ s, IsDynCoverOf T F U n ↑s

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

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
have : IsDynCoverOf T F V 1 s := by
  simp only [IsDynCoverOf, Finset.mem_coe, dynEntourage_one, s_cover]

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
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
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
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

Tactic:
simp only [IsDynCoverOf, Finset.mem_coe, dynEntourage_one, s_cover]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
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
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
rcases this.iterate_le_pow F_inv V_symm n with ⟨t, t_dyncover, t_card⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
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
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) (1 * n) ↑t
t_card : t.card ≤ s.card ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
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
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) (1 * n) ↑t
t_card : t.card ≤ s.card ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
rw [one_mul n] at t_dyncover

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
F_inv : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
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
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) n ↑t
t_card : t.card ≤ s.card ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s