From 3e282876aa45d0723aecf81c2eea05c0b24a573e Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 24 Jun 2024 03:28:01 +0200
Subject: [PATCH 1/4] feat(Topology/UniformSpace): add `uniformContinuous_ite `

This PR adds the theorem `uniformContinuous_ite`.

Co-Authored-By: D-Thomine <100795491+D-Thomine@users.noreply.github.com>
---
 Mathlib/Topology/UniformSpace/Basic.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean
index 1e14413fa5818a..e8701e94f721e9 100644
--- a/Mathlib/Topology/UniformSpace/Basic.lean
+++ b/Mathlib/Topology/UniformSpace/Basic.lean
@@ -1120,6 +1120,13 @@ nonrec theorem UniformContinuous.comp [UniformSpace β] [UniformSpace γ] {g : 
   hg.comp hf
 #align uniform_continuous.comp UniformContinuous.comp
 
+theorem uniformContinuous_ite [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) :
+    UniformContinuous T^[n] := by
+  induction' n with n hn
+  · exact uniformContinuous_id
+  · exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h
+#align uniform_continuous_ite uniformContinuous_ite
+
 theorem Filter.HasBasis.uniformContinuous_iff {ι'} [UniformSpace β] {p : ι → Prop}
     {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)}
     (hb : (𝓤 β).HasBasis q t) {f : α → β} :

From e40de6c3a4dde95dde54c30c35d533390ec2e009 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 24 Jun 2024 03:30:33 +0200
Subject: [PATCH 2/4] Update Basic.lean

Co-Authored-By: D-Thomine <100795491+D-Thomine@users.noreply.github.com>
---
 Mathlib/Topology/UniformSpace/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean
index e8701e94f721e9..c85e9d0c94780c 100644
--- a/Mathlib/Topology/UniformSpace/Basic.lean
+++ b/Mathlib/Topology/UniformSpace/Basic.lean
@@ -1120,6 +1120,8 @@ nonrec theorem UniformContinuous.comp [UniformSpace β] [UniformSpace γ] {g : 
   hg.comp hf
 #align uniform_continuous.comp UniformContinuous.comp
 
+/--If a function `T` is uniformly continuous in a uniform space `β`,
+then its `n`-th iterate `T^[n]` is also uniformly continuous.-/
 theorem uniformContinuous_ite [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) :
     UniformContinuous T^[n] := by
   induction' n with n hn

From 2fd6a01761e7ad67aba9a7e7e1b6fff5e72697ba Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 24 Jun 2024 16:55:39 +0200
Subject: [PATCH 3/4] Update Basic.lean

---
 Mathlib/Topology/UniformSpace/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean
index c85e9d0c94780c..cb67b5c6f18fe8 100644
--- a/Mathlib/Topology/UniformSpace/Basic.lean
+++ b/Mathlib/Topology/UniformSpace/Basic.lean
@@ -1122,12 +1122,11 @@ nonrec theorem UniformContinuous.comp [UniformSpace β] [UniformSpace γ] {g : 
 
 /--If a function `T` is uniformly continuous in a uniform space `β`,
 then its `n`-th iterate `T^[n]` is also uniformly continuous.-/
-theorem uniformContinuous_ite [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) :
+theorem UniformContinuous.iterate [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) :
     UniformContinuous T^[n] := by
   induction' n with n hn
   · exact uniformContinuous_id
   · exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h
-#align uniform_continuous_ite uniformContinuous_ite
 
 theorem Filter.HasBasis.uniformContinuous_iff {ι'} [UniformSpace β] {p : ι → Prop}
     {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)}

From 4f488578caa345cec9b61b8870584e8835e8511c Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 24 Jun 2024 18:37:35 +0200
Subject: [PATCH 4/4] Update Basic.lean

---
 Mathlib/Topology/UniformSpace/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean
index cb67b5c6f18fe8..0f3467989592ee 100644
--- a/Mathlib/Topology/UniformSpace/Basic.lean
+++ b/Mathlib/Topology/UniformSpace/Basic.lean
@@ -1124,9 +1124,9 @@ nonrec theorem UniformContinuous.comp [UniformSpace β] [UniformSpace γ] {g : 
 then its `n`-th iterate `T^[n]` is also uniformly continuous.-/
 theorem UniformContinuous.iterate [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) :
     UniformContinuous T^[n] := by
-  induction' n with n hn
-  · exact uniformContinuous_id
-  · exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h
+  induction n with
+  | zero => exact uniformContinuous_id
+  | succ n hn => exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h
 
 theorem Filter.HasBasis.uniformContinuous_iff {ι'} [UniformSpace β] {p : ι → Prop}
     {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)}