-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
/-- From a dynamical cover `s` with entourage `U` and time `m`, we construct covers with entourage
`U ○ U` and any multiple `m * n` of `m` with controlled cardinality. This lemma is the first step
in a submultiplicative-like property of `coverMincard`, with consequences such as explicit bounds
for the topological entropy (`coverEntropyInfEntourage_le_card_div`) and an equality between
two notions of topological entropy (`coverEntropyInf_eq_coverEntropySup_of_inv`). -/
lemma IsDynCoverOf.iterate_le_pow {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)}
    (U_symm : SymmetricRel U) {m : ℕ} (n : ℕ) {s : Finset X} (h : IsDynCoverOf T F U m s) :
    ∃ t : Finset X, IsDynCoverOf T F (U ○ U) (m * n) t ∧ t.card ≤ s.card ^ n

Proof state:
case inr.intro.inr.refine_1
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this : Fintype ↑(range dyncover)
x✝ : Nonempty { x // x ∈ s }
y : X
y_F : y ∈ F
key : ∀ (k : Fin n), ∃ z, y ∈ T^[m * ↑k] ⁻¹' ball (↑z) (dynEntourage T U m)
⊢ y ∈ ⋃ x ∈ ↑sn.toFinset, ball x (dynEntourage T (U ○ U) (m * n))

Tactic:
choose! t ht using key

Result:
case inr.intro.inr.refine_1
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this : Fintype ↑(range dyncover)
x✝ : Nonempty { x // x ∈ s }
y : X
y_F : y ∈ F
t : Fin n → { x // x ∈ s }
ht : ∀ (k : Fin n), y ∈ T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
⊢ y ∈ ⋃ x ∈ ↑sn.toFinset, ball x (dynEntourage T (U ○ U) (m * n))

Proof state:
case inr.intro.inr.refine_1
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this : Fintype ↑(range dyncover)
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset

Tactic:
rw [Finset.coe_nonempty] at s_nemp

Result:
case inr.intro.inr.refine_1
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this : Fintype ↑(range dyncover)
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset

Proof state:
case inr.intro.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
this :
  ∀ (t : Fin n → { x // x ∈ s }),
    ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ t.card ≤ s.card ^ n

Tactic:
choose! dyncover h_dyncover using this

Result:
case inr.intro.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ t.card ≤ s.card ^ n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this : Fintype ↑(range dyncover)
x✝ : Nonempty { x // x ∈ s }
y : X
y_F : y ∈ F
k : Fin n
⊢ ∃ z, y ∈ T^[m * ↑k] ⁻¹' ball (↑z) (dynEntourage T U m)

Tactic:
have := h (MapsTo.iterate F_inv (m * k) y_F)

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this✝ : Fintype ↑(range dyncover)
x✝ : Nonempty { x // x ∈ s }
y : X
y_F : y ∈ F
k : Fin n
this : T^[m * ↑k] y ∈ ⋃ x ∈ ↑s, ball x (dynEntourage T U m)
⊢ ∃ z, y ∈ T^[m * ↑k] ⁻¹' ball (↑z) (dynEntourage T U m)

Proof state:
case inr.intro.inr.refine_1
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this : Fintype ↑(range dyncover)
x✝ : Nonempty { x // x ∈ s }
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset

Tactic:
intro y y_F

Result:
case inr.intro.inr.refine_1
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → { x // x ∈ s }) → X
h_dyncover :
  ∀ (t : Fin n → { x // x ∈ s }),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
this : Fintype ↑(range dyncover)
x✝ : Nonempty { x // x ∈ s }
y : X
y_F : y ∈ F
⊢ y ∈ ⋃ x ∈ ↑sn.toFinset, ball x (dynEntourage T (U ○ U) (m * n))