-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
inl :
  ∀ (F_inv : MapsTo T ∅ ∅) (h : IsDynCoverOf T ∅ U m (↑s : Set X)),
    ∃ (t : Finset X), IsDynCoverOf T ∅ (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr inr₁ : ∀ (F_nemp : F.Nonempty), ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₂ :
  ∀ (F_nemp : F.Nonempty), Nonempty X → ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₃ :
  ∀ (F_nemp : F.Nonempty),
    Nonempty X →
      ∀ (s_nemp : (↑s : Set X).Nonempty), ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₄ :
  Nonempty X →
    ∀ (s_nemp : (↑s : Set X).Nonempty) (x : X) (x_F : x ∈ F),
      ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₅ :
  Nonempty X →
    ∀ (s_nemp : (↑s : Set X).Nonempty) (x : X) (x_F : x ∈ F) (h : IsDynCoverOf T F U 0 (↑s : Set X)),
      ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (0 * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₆ inr₇ :
  Nonempty X →
    ∀ (s_nemp : (↑s : Set X).Nonempty) (x : X) (x_F : x ∈ F) (m_pos : m > 0),
      ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₈ :
  Nonempty X →
    ∀ (s_nemp : (↑s : Set X).Nonempty) (x : X) (x_F : x ∈ F) (m_pos : m > 0)
      (this :
        ∀ (t : Fin n → ↥s),
          ∃ (y : X),
            ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
              ball y (dynEntourage T (U ○ U) (m * n))),
      ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₉ inr₁₀ :
  Nonempty X →
    ∀ (s_nemp : (↑s : Set X).Nonempty) (x : X) (x_F : x ∈ F) (m_pos : m > 0) (dyncover : (t : Fin n → ↥s) → X)
      (h_dyncover :
        ∀ (t : Fin n → ↥s),
          ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
            ball (dyncover t) (dynEntourage T (U ○ U) (m * n))),
      ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₁₁ :
  Nonempty X →
    ∀ (s_nemp : (↑s : Set X).Nonempty) (x : X) (x_F : x ∈ F) (m_pos : m > 0) (dyncover : (t : Fin n → ↥s) → X)
      (h_dyncover :
        ∀ (t : Fin n → ↥s),
          ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
            ball (dyncover t) (dynEntourage T (U ○ U) (m * n))),
      let sn := range dyncover;
      IsDynCoverOf T F (U ○ U) (m * n) (↑sn.toFinset : Set X)
inr₁₂ inr₁₃ :
  Nonempty X →
    ∀ (s_nemp : (↑s : Set X).Nonempty) (x : X) (x_F : x ∈ F) (m_pos : m > 0) (dyncover : (t : Fin n → ↥s) → X)
      (h_dyncover :
        ∀ (t : Fin n → ↥s),
          ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
            ball (dyncover t) (dynEntourage T (U ○ U) (m * n))),
      let sn := range dyncover;
      #sn.toFinset ≤ #s ^ n
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n

Tactic:
classical
  -- Deal with the edge cases: `F = ∅` or `m = 0`.
  rcases F.eq_empty_or_nonempty with rfl | F_nemp
  · exact ⟨∅, by simp⟩
  have _ : Nonempty X := F_nemp.nonempty
  have s_nemp := h.nonempty F_nemp
  obtain ⟨x, x_F⟩ := F_nemp
  rcases m.eq_zero_or_pos with rfl | m_pos
  · use {x}
    simp only [zero_mul, Finset.coe_singleton, Finset.card_singleton]
    exact ⟨isDynCoverOf_zero T F (U ○ U) (singleton_nonempty x),
      one_le_pow_of_one_le' (Nat.one_le_of_lt (Finset.Nonempty.card_pos s_nemp)) n⟩
  -- The proof goes as follows. Given an orbit of length `(m * n)` starting from `y`, each of its
  -- iterates `y`, `T^[m] y`, `T^[m]^[2] y` ... is `(dynEntourage T U m)`-close to a point of `s`.
  -- Conversely, given a sequence `t 0`, `t 1`, `t 2` of points in `s`, we choose a point
  -- `z = dyncover t` such that  `z`, `T^[m] z`, `T^[m]^[2] z` ... are `(dynEntourage T U m)`-close
  --  to `t 0`, `t 1`, `t 2`... Then  `y`, `T^[m] y`, `T^[m]^[2] y` ... are
  -- `(dynEntourage T (U ○ U) m)`-close to `z`, `T^[m] z`, `T^[m]^[2] z`, so that the union of such
  -- `z` provides the desired cover. Since there are at most `s.card ^ n` sequences of
  -- length `n` with values in `s`, we get the upper bound we want on the cardinality.
  -- First step: construct `dyncover`. Given `t 0`, `t 1`, `t 2`, if we cannot find such a point
  -- `dyncover t`, we use the dummy `x`.
  have (t : Fin n → s) : ∃ y : X, (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)) ⊆
      ball y (dynEntourage T (U ○ U) (m * n)) := by
    rcases (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)).eq_empty_or_nonempty
      with inter_empt | inter_nemp
    · exact inter_empt ▸ ⟨x, empty_subset _⟩
    · obtain ⟨y, y_int⟩ := inter_nemp
      refine ⟨y, fun z z_int ↦ ?_⟩
      simp only [ball, dynEntourage, Prod.map_iterate, mem_iInter, Set.mem_preimage, Prod.map_apply,
        mem_comp] at y_int z_int ⊢
      intro k k_mn
      replace k_mn := Nat.div_lt_of_lt_mul k_mn
      specialize z_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
      rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int
      exact mem_comp_of_mem_ball y_int z_int
  choose! dyncover h_dyncover using this
  -- The cover we want is the set of all `dyncover t`, that is, `range dyncover`. We need to check
  -- that it is indeed a `(U ○ U, m * n)` cover, and that its cardinality is at most `card s ^ n`.
  -- Only the first point requires significant work.
  let sn := range dyncover
  refine ⟨sn.toFinset, ?_, ?_⟩
  · -- We implement the argument at the beginning: given `y ∈ F`, we extract `t 0`, `t 1`, `t 2`
    -- such that `y`, `T^[m] y`, `T^[m]^[2] y` ... is `(dynEntourage T U m)`-close to `t 0`, `t 1`,
    -- `t 2`... Then `dyncover t` is a point of `range dyncover` which satisfies the conclusion
    -- of the lemma.
    rw [Finset.coe_nonempty] at s_nemp
    have _ : Nonempty s := Finset.Nonempty.coe_sort s_nemp
    intro y y_F
    have key : ∀ k : Fin n, ∃ z : s, y ∈ T^[m * k] ⁻¹' ball z (dynEntourage T U m) := by
      intro k
      have := h (MapsTo.iterate F_inv (m * k) y_F)
      simp only [Finset.mem_coe] at this
      obtain ⟨z, z_s, hz⟩ := this
      exact ⟨⟨z, z_s⟩, (dynEntourage T U m).symm hz⟩
    choose! t ht using key
    simp only [toFinset_range, Finset.coe_image, Finset.coe_univ, image_univ, mem_range,
      exists_exists_eq_and, sn]
    refine ⟨t, (dynEntourage T (U ○ U) (m * n)).symm <| h_dyncover t <| by simpa using ht⟩
  · rw [toFinset_card]
    apply (Fintype.card_range_le dyncover).trans
    simp only [Fintype.card_fun, Fintype.card_coe, Fintype.card_fin, le_refl]

Premises used: Set.image_univ, le_refl, Set.mem_range, Fintype.card_fin, Finset.coe_singleton, Set.toFinset_range, Finset.coe_univ, Finset.coe_nonempty, MulZeroClass.zero_mul, Finset.coe_image, Set.toFinset_card, Set.eq_empty_or_nonempty, exists_exists_eq_and, Fintype.card_coe, Nat.eq_zero_or_pos, Fintype.card_fun, rfl, Finset.card_singleton