From 8d5299922214df1a6762bbd675c242d0b00aadfe Mon Sep 17 00:00:00 2001
From: Hannah Scholz <hannah@scholzbande.de>
Date: Tue, 29 Oct 2024 16:22:38 +0000
Subject: [PATCH] feat: Homeomorphisms and IsometryEquivs based on
 `Equiv.piCongrLeft` and `Equiv.sumArrowEquivProdArrow` (#17981)

---
 Mathlib/Data/Fin/Tuple/Basic.lean          |  5 +++
 Mathlib/Logic/Equiv/Fin.lean               |  9 ++++
 Mathlib/Topology/Homeomorph.lean           | 43 +++++++++++++++++++
 Mathlib/Topology/MetricSpace/Isometry.lean | 49 ++++++++++++++++++++++
 4 files changed, 106 insertions(+)

diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index 6f1f772191c56..81cd43b8a59f1 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -394,6 +394,11 @@ lemma append_comp_rev {m n} (xs : Fin m → α) (ys : Fin n → α) :
     append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ cast (Nat.add_comm ..) :=
   funext <| append_rev xs ys
 
+theorem append_castAdd_natAdd {f : Fin (m + n) → α} :
+    append (fun i ↦ f (castAdd n i)) (fun i ↦ f (natAdd m i)) = f := by
+  unfold append addCases
+  simp
+
 end Append
 
 section Repeat
diff --git a/Mathlib/Logic/Equiv/Fin.lean b/Mathlib/Logic/Equiv/Fin.lean
index 9a84638f26396..7e551963a14c7 100644
--- a/Mathlib/Logic/Equiv/Fin.lean
+++ b/Mathlib/Logic/Equiv/Fin.lean
@@ -498,3 +498,12 @@ instance subsingleton_fin_zero : Subsingleton (Fin 0) :=
 /-- `Fin 1` is a subsingleton. -/
 instance subsingleton_fin_one : Subsingleton (Fin 1) :=
   finOneEquiv.subsingleton
+
+/-- The natural `Equiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α`.-/
+@[simps]
+def Fin.appendEquiv {α : Type*} (m n : ℕ) :
+    (Fin m → α) × (Fin n → α) ≃ (Fin (m + n) → α) where
+  toFun fg := Fin.append fg.1 fg.2
+  invFun f := ⟨fun i ↦ f (Fin.castAdd n i), fun i ↦ f (Fin.natAdd m i)⟩
+  left_inv fg := by simp
+  right_inv f := by simp [Fin.append_castAdd_natAdd]
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
index 72c26cc9ed6be..17cbd37091ef9 100644
--- a/Mathlib/Topology/Homeomorph.lean
+++ b/Mathlib/Topology/Homeomorph.lean
@@ -703,6 +703,49 @@ def ulift.{u, v} {X : Type u} [TopologicalSpace X] : ULift.{v, u} X ≃ₜ X whe
   continuous_invFun := continuous_uLift_up
   toEquiv := Equiv.ulift
 
+/-- The natural homeomorphism `(ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)`.
+`Equiv.sumArrowEquivProdArrow` as a homeomorphism. -/
+@[simps!]
+def sumArrowHomeomorphProdArrow {ι ι' : Type*} : (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)  where
+  toEquiv := Equiv.sumArrowEquivProdArrow _ _ _
+  continuous_toFun := by
+    simp only [Equiv.sumArrowEquivProdArrow, Equiv.coe_fn_mk, continuous_prod_mk]
+    continuity
+  continuous_invFun := continuous_pi fun i ↦ match i with
+    | .inl i => by apply (continuous_apply _).comp' continuous_fst
+    | .inr i => by apply (continuous_apply _).comp' continuous_snd
+
+private theorem _root_.Fin.appendEquiv_eq_Homeomorph (m n : ℕ) : Fin.appendEquiv m n =
+    ((sumArrowHomeomorphProdArrow).symm.trans
+    (piCongrLeft (Y := fun _ ↦ X) finSumFinEquiv)).toEquiv := by
+  ext ⟨x1, x2⟩ l
+  simp only [sumArrowHomeomorphProdArrow, Equiv.sumArrowEquivProdArrow,
+    finSumFinEquiv, Fin.addCases, Fin.appendEquiv, Fin.append, Equiv.coe_fn_mk]
+  by_cases h : l < m
+  · simp [h]
+  · simp [h]
+
+theorem _root_.Fin.continuous_append (m n : ℕ) :
+    Continuous fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2 := by
+  suffices Continuous (Fin.appendEquiv m n) by exact this
+  rw [Fin.appendEquiv_eq_Homeomorph]
+  exact Homeomorph.continuous_toFun _
+
+/-- The natural homeomorphism between `(Fin m → X) × (Fin n → X)` and `Fin (m + n) → X`.
+`Fin.appendEquiv` as a homeomorphism.-/
+@[simps!]
+def _root_.Fin.appendHomeomorph (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X) where
+  toEquiv := Fin.appendEquiv m n
+  continuous_toFun := Fin.continuous_append m n
+  continuous_invFun := by
+    rw [Fin.appendEquiv_eq_Homeomorph]
+    exact Homeomorph.continuous_invFun _
+
+@[simp]
+theorem _root_.Fin.appendHomeomorph_toEquiv (m n : ℕ) :
+    (Fin.appendHomeomorph (X := X) m n).toEquiv = Fin.appendEquiv m n :=
+  rfl
+
 section Distrib
 
 /-- `(X ⊕ Y) × Z` is homeomorphic to `X × Z ⊕ Y × Z`. -/
diff --git a/Mathlib/Topology/MetricSpace/Isometry.lean b/Mathlib/Topology/MetricSpace/Isometry.lean
index 7c9282c9271fb..969dd91549017 100644
--- a/Mathlib/Topology/MetricSpace/Isometry.lean
+++ b/Mathlib/Topology/MetricSpace/Isometry.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Topology.MetricSpace.Antilipschitz
+import Mathlib.Data.Fintype.Lattice
 
 /-!
 # Isometries
@@ -488,6 +489,54 @@ theorem completeSpace_iff (e : α ≃ᵢ β) : CompleteSpace α ↔ CompleteSpac
 protected theorem completeSpace [CompleteSpace β] (e : α ≃ᵢ β) : CompleteSpace α :=
   e.completeSpace_iff.2 ‹_›
 
+/-- The natural isometry `∀ i, Y i ≃ᵢ ∀ j, Y (e.symm j)` obtained from a bijection `ι ≃ ι'` of
+fintypes. `Equiv.piCongrLeft'` as an `IsometryEquiv`.-/
+@[simps!]
+def piCongrLeft' {ι' : Type*} [Fintype ι] [Fintype ι'] {Y : ι → Type*}
+    [∀ j, PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y i) ≃ᵢ ∀ j, Y (e.symm j) where
+  toEquiv := Equiv.piCongrLeft' _ e
+  isometry_toFun x1 x2 := by
+    simp_rw [edist_pi_def, Finset.sup_univ_eq_iSup]
+    exact (Equiv.iSup_comp (g := fun b ↦ edist (x1 b) (x2 b)) e.symm)
+
+/-- The natural isometry `∀ i, Y (e i) ≃ᵢ ∀ j, Y j` obtained from a bijection `ι ≃ ι'` of fintypes.
+`Equiv.piCongrLeft` as an `IsometryEquiv`. -/
+@[simps!]
+def piCongrLeft {ι' : Type*} [Fintype ι] [Fintype ι'] {Y : ι' → Type*}
+    [∀ j, PseudoEMetricSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ᵢ ∀ j, Y j :=
+  (piCongrLeft' e.symm).symm
+
+/-- The natural isometry `(α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)` between the type of maps on a sum of
+fintypes `α ⊕ β` and the pairs of functions on the types `α` and `β`.
+`Equiv.sumArrowEquivProdArrow` as an `IsometryEquiv`.-/
+@[simps!]
+def sumArrowIsometryEquivProdArrow [Fintype α] [Fintype β] : (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ) where
+  toEquiv := Equiv.sumArrowEquivProdArrow _ _ _
+  isometry_toFun _ _ := by simp [Prod.edist_eq, edist_pi_def, Finset.sup_univ_eq_iSup, iSup_sum]
+
+@[simp]
+theorem sumArrowIsometryEquivProdArrow_toHomeomorph {α β : Type*} [Fintype α] [Fintype β] :
+    sumArrowIsometryEquivProdArrow.toHomeomorph
+    = Homeomorph.sumArrowHomeomorphProdArrow (ι := α) (ι' := β) (X := γ) :=
+  rfl
+
+theorem _root_.Fin.edist_append_eq_max_edist (m n : ℕ) {x x2 : Fin m → α} {y y2 : Fin n → α} :
+    edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2) := by
+  simp [edist_pi_def, Finset.sup_univ_eq_iSup, ← Equiv.iSup_comp (e := finSumFinEquiv),
+    Prod.edist_eq, iSup_sum]
+
+/-- The natural `IsometryEquiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α`.
+`Fin.appendEquiv` as an `IsometryEquiv`.-/
+@[simps!]
+def _root_.Fin.appendIsometry (m n : ℕ) : (Fin m → α) × (Fin n → α) ≃ᵢ (Fin (m + n) → α) where
+  toEquiv := Fin.appendEquiv _ _
+  isometry_toFun _ _ := by simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]
+
+@[simp]
+theorem _root_.Fin.appendIsometry_toHomeomorph (m n : ℕ) :
+    (Fin.appendIsometry m n).toHomeomorph = Fin.appendHomeomorph (X := α) m n :=
+  rfl
+
 variable (ι α)
 
 /-- `Equiv.funUnique` as an `IsometryEquiv`. -/