-- 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
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
t : Fin n → { x // x ∈ s }
y : X
y_int : y ∈ ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
z : X
z_int : z ∈ ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
⊢ z ∈ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
simp only [ball, dynEntourage, Prod.map_iterate, mem_preimage, mem_iInter,
  Prod.map_apply] at y_int z_int ⊢

Result:
case inr.intro
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
t : Fin n → { x // x ∈ s }
y z : X
y_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] y)) ∈ U
z_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] z)) ∈ U
⊢ ∀ i < m * n, (T^[i] y, T^[i] z) ∈ U ○ U

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
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ t.card ≤ s.card ^ n

Tactic:
rcases F.eq_empty_or_nonempty with rfl | F_nemp

Result:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
s : Finset X
F_inv : MapsTo T ∅ ∅
h : IsDynCoverOf T ∅ U m ↑s
⊢ ∃ t, IsDynCoverOf T ∅ (U ○ U) (m * n) ↑t ∧ t.card ≤ s.card ^ n

case 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
F_nemp : F.Nonempty
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ t.card ≤ s.card ^ n

Proof state:
case inr.intro
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
t : Fin n → { x // x ∈ s }
y z : X
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] z)) ∈ U
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] y)) ∈ U
⊢ (T^[k] y, T^[k] z) ∈ U ○ U

Tactic:
rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int

Result:
case inr.intro
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
t : Fin n → { x // x ∈ s }
y z : X
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] z) ∈ U
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] y) ∈ U
⊢ (T^[k] y, T^[k] z) ∈ U ○ U

Proof state:
case inr.intro
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
t : Fin n → { x // x ∈ s }
y z : X
y_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] y)) ∈ U
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] z)) ∈ U
⊢ (T^[k] y, T^[k] z) ∈ U ○ U

Tactic:
specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)

Result:
case inr.intro
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
t : Fin n → { x // x ∈ s }
y z : X
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] z)) ∈ U
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] y)) ∈ U
⊢ (T^[k] y, T^[k] z) ∈ U ○ U

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
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))

Tactic:
rcases (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)).eq_empty_or_nonempty
  with inter_empt | inter_nemp

Result:
case inl
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
t : Fin n → { x // x ∈ s }
inter_empt : ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) = ∅
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

case 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
t : Fin n → { x // x ∈ s }
inter_nemp : (⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)).Nonempty
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Proof state:
case h
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s : Finset X
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 ↑s
⊢ IsDynCoverOf T F (U ○ U) 0 {x} ∧ 1 ≤ s.card ^ n

Tactic:
exact And.intro (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

Result:
no goals