From e91cdbcf5a387801a6225b41b0056c63206a9f7f Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 26 Oct 2024 04:02:06 +0000
Subject: [PATCH 1/9] chore(ContinuousMap): move `compRight*` (#17935)

Also drop some unneeded assumptions and rename/deprecate some lemmas.
---
 .../Instances.lean                            |  5 +-
 .../NonUnital.lean                            |  2 +-
 .../ContinuousFunctionalCalculus/Unique.lean  |  8 +--
 .../ContinuousFunctionalCalculus/Unital.lean  |  2 +-
 .../Topology/Algebra/ContinuousMonoidHom.lean |  4 +-
 Mathlib/Topology/CompactOpen.lean             | 46 ++++++++++++----
 Mathlib/Topology/ContinuousMap/Algebra.lean   |  4 ++
 Mathlib/Topology/ContinuousMap/Compact.lean   | 52 -------------------
 Mathlib/Topology/ContinuousMap/Sigma.lean     |  2 +-
 .../Topology/ContinuousMap/Weierstrass.lean   |  2 +-
 Mathlib/Topology/Homotopy/HomotopyGroup.lean  |  8 +--
 11 files changed, 55 insertions(+), 80 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
index 1ed5d8debe5ce..b4cc643968f53 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
@@ -83,10 +83,7 @@ lemma isClosedEmbedding_cfcₙAux : IsClosedEmbedding (cfcₙAux hp₁ a ha) :=
   refine ((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp
     ContinuousMapZero.isClosedEmbedding_toContinuousMap
   let e : C(σₙ 𝕜 a, 𝕜) ≃ₜ C(σ 𝕜 (a : A⁺¹), 𝕜) :=
-    { (Homeomorph.compStarAlgEquiv' 𝕜 𝕜 <| .setCongr <|
-        (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a).symm) with
-      continuous_toFun := ContinuousMap.continuous_comp_left _
-      continuous_invFun := ContinuousMap.continuous_comp_left _ }
+    (Homeomorph.setCongr (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a)).arrowCongr (.refl _)
   exact e.isClosedEmbedding
 
 @[deprecated (since := "2024-10-20")]
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
index ed76c4a88dc63..458c86fac7e39 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
@@ -178,7 +178,7 @@ theorem cfcₙHom_comp [UniqueNonUnitalContinuousFunctionalCalculus R A] (f : C(
   suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
   refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_
   · refine (cfcₙHom_isClosedEmbedding ha).continuous.comp <| continuous_induced_rng.mpr ?_
-    exact f'.toContinuousMap.continuous_comp_left.comp continuous_induced_dom
+    exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom
   · simp only [φ, ψ, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_mk',
       NonUnitalAlgHom.coe_mk]
     congr
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
index 5186931925074..0643b90789114 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@@ -56,7 +56,7 @@ namespace ContinuousMap
 noncomputable def toNNReal (f : C(X, ℝ)) : C(X, ℝ≥0) := .realToNNReal |>.comp f
 
 @[fun_prop]
-lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_comp _
+lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := continuous_postcomp _
 
 @[simp]
 lemma toNNReal_apply (f : C(X, ℝ)) (x : X) : f.toNNReal x = (f x).toNNReal := rfl
@@ -187,7 +187,7 @@ instance NNReal.instUniqueContinuousFunctionalCalculus [UniqueContinuousFunction
         Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by
       intro ξ'
       refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
-        ContinuousMap.continuous_comp_left _, ?_⟩
+        ContinuousMap.continuous_precomp _, ?_⟩
       exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)
     obtain ⟨hφ', hφ_id⟩ := this φ hφ
     obtain ⟨hψ', hψ_id⟩ := this ψ hψ
@@ -249,7 +249,7 @@ lemma toNNReal_apply (f : C(X, ℝ)₀) (x : X) : f.toNNReal x = Real.toNNReal (
 lemma continuous_toNNReal : Continuous (toNNReal (X := X)) := by
   rw [continuous_induced_rng]
   convert_to Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1
-  exact ContinuousMap.continuous_comp _ |>.comp continuous_induced_dom
+  exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom
 
 lemma toContinuousMapHom_toNNReal (f : C(X, ℝ)₀) :
     (toContinuousMapHom (X := X) (R := ℝ) f).toNNReal =
@@ -401,7 +401,7 @@ instance NNReal.instUniqueNonUnitalContinuousFunctionalCalculus
       intro ξ'
       refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩
       · rw [continuous_induced_rng]
-        exact ContinuousMap.continuous_comp_left _ |>.comp continuous_induced_dom
+        exact ContinuousMap.continuous_precomp _ |>.comp continuous_induced_dom
       · exact ξ.realContinuousMapZeroOfNNReal_apply_comp_toReal (.id h0)
     obtain ⟨hφ', hφ_id⟩ := this φ hφ
     obtain ⟨hψ', hψ_id⟩ := this ψ hψ
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
index b193f3c40b439..820b45e9bdb3c 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
@@ -271,7 +271,7 @@ theorem cfcHom_comp [UniqueContinuousFunctionalCalculus R A] (f : C(spectrum R a
     (cfcHom ha).comp <| ContinuousMap.compStarAlgHom' R R f'
   suffices cfcHom (cfcHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
   refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_
-  · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_comp_left
+  · exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_precomp
   · simp only [φ, StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply]
     congr
     ext x
diff --git a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
index faf9ab016a5e2..ff9ec26c16279 100644
--- a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
+++ b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
@@ -302,13 +302,13 @@ theorem continuous_comp [LocallyCompactSpace B] :
 theorem continuous_comp_left (f : ContinuousMonoidHom A B) :
     Continuous fun g : ContinuousMonoidHom B C => g.comp f :=
   (inducing_toContinuousMap A C).continuous_iff.2 <|
-    f.toContinuousMap.continuous_comp_left.comp (inducing_toContinuousMap B C).continuous
+    f.toContinuousMap.continuous_precomp.comp (inducing_toContinuousMap B C).continuous
 
 @[to_additive]
 theorem continuous_comp_right (f : ContinuousMonoidHom B C) :
     Continuous fun g : ContinuousMonoidHom A B => f.comp g :=
   (inducing_toContinuousMap A C).continuous_iff.2 <|
-    f.toContinuousMap.continuous_comp.comp (inducing_toContinuousMap A B).continuous
+    f.toContinuousMap.continuous_postcomp.comp (inducing_toContinuousMap A B).continuous
 
 variable (E)
 
diff --git a/Mathlib/Topology/CompactOpen.lean b/Mathlib/Topology/CompactOpen.lean
index 4ff883b2e49b1..8f58dc36f0245 100644
--- a/Mathlib/Topology/CompactOpen.lean
+++ b/Mathlib/Topology/CompactOpen.lean
@@ -78,27 +78,45 @@ lemma continuous_compactOpen {f : X → C(Y, Z)} :
 section Functorial
 
 /-- `C(X, ·)` is a functor. -/
-theorem continuous_comp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) :=
+theorem continuous_postcomp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) :=
   continuous_compactOpen.2 fun _K hK _U hU ↦ isOpen_setOf_mapsTo hK (hU.preimage g.2)
 
+@[deprecated (since := "2024-10-19")] alias continuous_comp := continuous_postcomp
+
 /-- If `g : C(Y, Z)` is a topology inducing map,
 then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is a topology inducing map too. -/
-theorem inducing_comp (g : C(Y, Z)) (hg : Inducing g) : Inducing (g.comp : C(X, Y) → C(X, Z)) where
+theorem inducing_postcomp (g : C(Y, Z)) (hg : Inducing g) :
+    Inducing (g.comp : C(X, Y) → C(X, Z)) where
   induced := by
     simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOf_isOpen,
       image2_image_right, MapsTo, mem_preimage, preimage_setOf_eq, comp_apply]
 
+@[deprecated (since := "2024-10-19")] alias inducing_comp := inducing_postcomp
+
 /-- If `g : C(Y, Z)` is a topological embedding,
 then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is an embedding too. -/
-theorem embedding_comp (g : C(Y, Z)) (hg : Embedding g) : Embedding (g.comp : C(X, Y) → C(X, Z)) :=
-  ⟨inducing_comp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩
+theorem embedding_postcomp (g : C(Y, Z)) (hg : Embedding g) :
+    Embedding (g.comp : C(X, Y) → C(X, Z)) :=
+  ⟨inducing_postcomp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩
+
+@[deprecated (since := "2024-10-19")] alias embedding_comp := embedding_postcomp
 
 /-- `C(·, Z)` is a functor. -/
-@[fun_prop]
-theorem continuous_comp_left (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) :=
+@[continuity, fun_prop]
+theorem continuous_precomp (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) :=
   continuous_compactOpen.2 fun K hK U hU ↦ by
     simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU
 
+@[deprecated (since := "2024-10-19")] alias continuous_comp_left := continuous_precomp
+
+variable (Z) in
+/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.
+-/
+@[simps apply]
+def compRightContinuousMap (f : C(X, Y)) :
+    C(C(Y, Z), C(X, Z)) where
+  toFun g := g.comp f
+
 /-- Any pair of homeomorphisms `X ≃ₜ Z` and `Y ≃ₜ T` gives rise to a homeomorphism
 `C(X, Y) ≃ₜ C(Z, T)`. -/
 protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) :
@@ -107,8 +125,16 @@ protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) :
   invFun f := .comp ψ.symm <| f.comp φ
   left_inv f := ext fun _ ↦ ψ.left_inv (f _) |>.trans <| congrArg f <| φ.left_inv _
   right_inv f := ext fun _ ↦ ψ.right_inv (f _) |>.trans <| congrArg f <| φ.right_inv _
-  continuous_toFun := continuous_comp _ |>.comp <| continuous_comp_left _
-  continuous_invFun := continuous_comp _ |>.comp <| continuous_comp_left _
+  continuous_toFun := continuous_postcomp _ |>.comp <| continuous_precomp _
+  continuous_invFun := continuous_postcomp _ |>.comp <| continuous_precomp _
+
+variable (Z) in
+/-- Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps.
+-/
+@[deprecated Homeomorph.arrowCongr (since := "2024-10-19")]
+def compRightHomeomorph (f : X ≃ₜ Y) :
+    C(Y, Z) ≃ₜ C(X, Z) :=
+  .arrowCongr f.symm (.refl _)
 
 variable [LocallyCompactPair Y Z]
 
@@ -234,7 +260,7 @@ section InfInduced
 /-- For any subset `s` of `X`, the restriction of continuous functions to `s` is continuous
 as a function from `C(X, Y)` to `C(s, Y)` with their respective compact-open topologies. -/
 theorem continuous_restrict (s : Set X) : Continuous fun F : C(X, Y) => F.restrict s :=
-  continuous_comp_left <| restrict s <| .id X
+  continuous_precomp <| restrict s <| .id X
 
 theorem compactOpen_le_induced (s : Set X) :
     (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) ≤
@@ -340,7 +366,7 @@ section Curry
     compact, then this is a homeomorphism, see `Homeomorph.curry`. -/
 def curry (f : C(X × Y, Z)) : C(X, C(Y, Z)) where
   toFun a := ⟨Function.curry f a, f.continuous.comp <| by fun_prop⟩
-  continuous_toFun := (continuous_comp f).comp continuous_coev
+  continuous_toFun := (continuous_postcomp f).comp continuous_coev
 
 @[simp]
 theorem curry_apply (f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b) :=
diff --git a/Mathlib/Topology/ContinuousMap/Algebra.lean b/Mathlib/Topology/ContinuousMap/Algebra.lean
index c475ae94f7dc9..c36b582bb8332 100644
--- a/Mathlib/Topology/ContinuousMap/Algebra.lean
+++ b/Mathlib/Topology/ContinuousMap/Algebra.lean
@@ -697,6 +697,10 @@ def ContinuousMap.compRightAlgHom {α β : Type*} [TopologicalSpace α] [Topolog
   map_mul' _ _ := ext fun _ ↦ rfl
   commutes' _ := ext fun _ ↦ rfl
 
+theorem ContinuousMap.compRightAlgHom_continuous {α β : Type*} [TopologicalSpace α]
+    [TopologicalSpace β] (f : C(α, β)) : Continuous (compRightAlgHom R A f) :=
+  continuous_precomp f
+
 variable {A}
 
 /-- Coercion to a function as an `AlgHom`. -/
diff --git a/Mathlib/Topology/ContinuousMap/Compact.lean b/Mathlib/Topology/ContinuousMap/Compact.lean
index 24fb53d8c00e8..9400fa18c4860 100644
--- a/Mathlib/Topology/ContinuousMap/Compact.lean
+++ b/Mathlib/Topology/ContinuousMap/Compact.lean
@@ -417,57 +417,6 @@ end CompLeft
 
 namespace ContinuousMap
 
-/-!
-We now setup variations on `compRight* f`, where `f : C(X, Y)`
-(that is, precomposition by a continuous map),
-as a morphism `C(Y, T) → C(X, T)`, respecting various types of structure.
-
-In particular:
-* `compRightContinuousMap`, the bundled continuous map (for this we need `X Y` compact).
-* `compRightHomeomorph`, when we precompose by a homeomorphism.
-* `compRightAlgHom`, when `T = R` is a topological ring.
--/
-
-
-section CompRight
-
-/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.
--/
-def compRightContinuousMap {X Y : Type*} (T : Type*) [TopologicalSpace X] [CompactSpace X]
-    [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : C(X, Y)) :
-    C(C(Y, T), C(X, T)) where
-  toFun g := g.comp f
-  continuous_toFun := by
-    refine Metric.continuous_iff.mpr ?_
-    intro g ε ε_pos
-    refine ⟨ε, ε_pos, fun g' h => ?_⟩
-    rw [ContinuousMap.dist_lt_iff ε_pos] at h ⊢
-    exact fun x => h (f x)
-
-@[simp]
-theorem compRightContinuousMap_apply {X Y : Type*} (T : Type*) [TopologicalSpace X]
-    [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : C(X, Y))
-    (g : C(Y, T)) : (compRightContinuousMap T f) g = g.comp f :=
-  rfl
-
-/-- Precomposition by a homeomorphism is itself a homeomorphism between spaces of continuous maps.
--/
-def compRightHomeomorph {X Y : Type*} (T : Type*) [TopologicalSpace X] [CompactSpace X]
-    [TopologicalSpace Y] [CompactSpace Y] [PseudoMetricSpace T] (f : X ≃ₜ Y) :
-    C(Y, T) ≃ₜ C(X, T) where
-  toFun := compRightContinuousMap T f
-  invFun := compRightContinuousMap T f.symm
-  left_inv g := ext fun _ => congr_arg g (f.apply_symm_apply _)
-  right_inv g := ext fun _ => congr_arg g (f.symm_apply_apply _)
-
-theorem compRightAlgHom_continuous {X Y : Type*} (R A : Type*) [TopologicalSpace X]
-    [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [CommSemiring R] [Semiring A]
-    [PseudoMetricSpace A] [TopologicalSemiring A] [Algebra R A] (f : C(X, Y)) :
-    Continuous (compRightAlgHom R A f) :=
-  map_continuous (compRightContinuousMap A f)
-
-end CompRight
-
 section LocalNormalConvergence
 
 /-! ### Local normal convergence
@@ -476,7 +425,6 @@ A sum of continuous functions (on a locally compact space) is "locally normally
 sum of its sup-norms on any compact subset is summable. This implies convergence in the topology
 of `C(X, E)` (i.e. locally uniform convergence). -/
 
-
 open TopologicalSpace
 
 variable {X : Type*} [TopologicalSpace X] [LocallyCompactSpace X]
diff --git a/Mathlib/Topology/ContinuousMap/Sigma.lean b/Mathlib/Topology/ContinuousMap/Sigma.lean
index 320fd5cc4ab1f..f205d452cbc48 100644
--- a/Mathlib/Topology/ContinuousMap/Sigma.lean
+++ b/Mathlib/Topology/ContinuousMap/Sigma.lean
@@ -44,7 +44,7 @@ namespace ContinuousMap
 theorem embedding_sigmaMk_comp [Nonempty X] :
     Embedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2) where
   toInducing := inducing_sigma.2
-    ⟨fun i ↦ (sigmaMk i).inducing_comp embedding_sigmaMk.toInducing, fun i ↦
+    ⟨fun i ↦ (sigmaMk i).inducing_postcomp embedding_sigmaMk.toInducing, fun i ↦
       let ⟨x⟩ := ‹Nonempty X›
       ⟨_, (isOpen_sigma_fst_preimage {i}).preimage (continuous_eval_const x), fun _ ↦ Iff.rfl⟩⟩
   inj := by
diff --git a/Mathlib/Topology/ContinuousMap/Weierstrass.lean b/Mathlib/Topology/ContinuousMap/Weierstrass.lean
index 8e903e39101e1..5e1edd95c1dc8 100644
--- a/Mathlib/Topology/ContinuousMap/Weierstrass.lean
+++ b/Mathlib/Topology/ContinuousMap/Weierstrass.lean
@@ -58,7 +58,7 @@ theorem polynomialFunctions_closure_eq_top (a b : ℝ) :
       compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm
     -- This operation is itself a homeomorphism
     -- (with respect to the norm topologies on continuous functions).
-    let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := compRightHomeomorph ℝ (iccHomeoI a b h).symm
+    let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := (iccHomeoI a b h).arrowCongr (.refl _)
     have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
     -- Thus we take the statement of the Weierstrass approximation theorem for `[0,1]`,
     have p := polynomialFunctions_closure_eq_top'
diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean
index 21ad316e36339..65ce882fec5b0 100644
--- a/Mathlib/Topology/Homotopy/HomotopyGroup.lean
+++ b/Mathlib/Topology/Homotopy/HomotopyGroup.lean
@@ -192,7 +192,7 @@ theorem continuous_toLoop (i : N) : Continuous (@toLoop N X _ x _ i) :=
       (continuous_eval.comp <|
         Continuous.prodMap
           (ContinuousMap.continuous_curry.comp <|
-            (ContinuousMap.continuous_comp_left _).comp continuous_subtype_val)
+            (ContinuousMap.continuous_precomp _).comp continuous_subtype_val)
           continuous_id)
       _
 
@@ -211,9 +211,9 @@ def fromLoop (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : Ω^ N X x :=
     · exact GenLoop.boundary _ _ ⟨⟨j, Hne⟩, Hj⟩⟩
 
 theorem continuous_fromLoop (i : N) : Continuous (@fromLoop N X _ x _ i) :=
-  ((ContinuousMap.continuous_comp_left _).comp <|
+  ((ContinuousMap.continuous_precomp _).comp <|
         ContinuousMap.continuous_uncurry.comp <|
-          (ContinuousMap.continuous_comp _).comp continuous_induced_dom).subtype_mk
+          (ContinuousMap.continuous_postcomp _).comp continuous_induced_dom).subtype_mk
     _
 
 theorem to_from (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : toLoop i (fromLoop i p) = p := by
@@ -244,7 +244,7 @@ theorem fromLoop_apply (i : N) {p : Ω (Ω^ { j // j ≠ i } X x) const} {t : I^
 /-- Composition with `Cube.insertAt` as a continuous map. -/
 abbrev cCompInsert (i : N) : C(C(I^N, X), C(I × I^{ j // j ≠ i }, X)) :=
   ⟨fun f => f.comp (Cube.insertAt i),
-    (toContinuousMap <| Cube.insertAt i).continuous_comp_left⟩
+    (toContinuousMap <| Cube.insertAt i).continuous_precomp⟩
 
 /-- A homotopy between `n+1`-dimensional loops `p` and `q` constant on the boundary
   seen as a homotopy between two paths in the space of `n`-dimensional paths. -/

From fd050c2d54938c9a9b5b827fee930496295b1b0d Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Sat, 26 Oct 2024 11:49:25 +0000
Subject: [PATCH 2/9] chore: improve hypotheses to `ContinuousMap.induction_on`
 (#18116)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Instead of requiring `∀ f, p f → p (star f)`, we only require `p (star id)` (and note that `p id` is already a requirement, so there is no added proof burden).
---
 .../ContinuousMap/StoneWeierstrass.lean       | 35 ++++++++++---------
 1 file changed, 19 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
index 7d274f86f8aab..54ba6ba6ff1d1 100644
--- a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
+++ b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
@@ -425,29 +425,31 @@ theorem polynomialFunctions.starClosure_topologicalClosure {𝕜 : Type*} [RCLik
 @[elab_as_elim]
 theorem ContinuousMap.induction_on {𝕜 : Type*} [RCLike 𝕜] {s : Set 𝕜}
     {p : C(s, 𝕜) → Prop} (const : ∀ r, p (.const s r)) (id : p (.restrict s <| .id 𝕜))
+    (star_id : p (star (.restrict s <| .id 𝕜)))
     (add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
-    (star : ∀ f, p f → p (star f))
     (closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ f, p f) (f : C(s, 𝕜)) :
     p f := by
   refine closure (fun f hf => ?_) f
   rw [polynomialFunctions.starClosure_eq_adjoin_X] at hf
-  induction hf using StarAlgebra.adjoin_induction with
+  induction hf using Algebra.adjoin_induction with
   | mem f hf =>
-    simp only [toContinuousMapOnAlgHom_apply, Set.mem_singleton_iff] at hf
-    rwa [hf, toContinuousMapOn_X_eq_restrict_id]
+    simp only [Set.mem_union, Set.mem_singleton_iff, Set.mem_star] at hf
+    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
+    obtain (rfl | rfl) := hf
+    all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
   | algebraMap r => exact const r
   | add _ _ _ _ hf hg => exact add _ _ hf hg
   | mul _ _ _ _ hf hg => exact mul _ _ hf hg
-  | star _ _ hf => exact star _ hf
 
 open Topology in
 @[elab_as_elim]
 theorem ContinuousMap.induction_on_of_compact {𝕜 : Type*} [RCLike 𝕜] {s : Set 𝕜} [CompactSpace s]
     {p : C(s, 𝕜) → Prop} (const : ∀ r, p (.const s r)) (id : p (.restrict s <| .id 𝕜))
+    (star_id : p (star (.restrict s <| .id 𝕜)))
     (add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
-    (star : ∀ f, p f → p (star f)) (frequently : ∀ f, (∃ᶠ g in 𝓝 f, p g) → p f) (f : C(s, 𝕜)) :
+    (frequently : ∀ f, (∃ᶠ g in 𝓝 f, p g) → p f) (f : C(s, 𝕜)) :
     p f := by
-  refine f.induction_on const id add mul star fun h f ↦ frequently f ?_
+  refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_
   have := polynomialFunctions.starClosure_topologicalClosure s ▸ mem_top (x := f)
   rw [← SetLike.mem_coe, topologicalClosure_coe, mem_closure_iff_frequently] at this
   exact this.mp <| .of_forall h
@@ -601,31 +603,32 @@ lemma ContinuousMapZero.adjoin_id_dense {s : Set 𝕜} [Zero s] (h0 : ((0 : s) :
 /-- An induction principle for `C(s, 𝕜)₀`. -/
 @[elab_as_elim]
 lemma ContinuousMapZero.induction_on {s : Set 𝕜} [Zero s] (h0 : ((0 : s) : 𝕜) = 0)
-    {p : C(s, 𝕜)₀ → Prop} (zero : p 0) (id : p (.id h0))
+    {p : C(s, 𝕜)₀ → Prop} (zero : p 0) (id : p (.id h0)) (star_id : p (star (.id h0)))
     (add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
-    (smul : ∀ (r : 𝕜) f, p f → p (r • f)) (star : ∀ f, p f → p (star f))
+    (smul : ∀ (r : 𝕜) f, p f → p (r • f))
     (closure : (∀ f ∈ adjoin 𝕜 {(.id h0 : C(s, 𝕜)₀)}, p f) → ∀ f, p f) (f : C(s, 𝕜)₀) :
     p f := by
   refine closure (fun f hf => ?_) f
-  induction hf using NonUnitalStarAlgebra.adjoin_induction with
+  induction hf using NonUnitalAlgebra.adjoin_induction with
   | mem f hf =>
-    simp only [Set.mem_singleton_iff] at hf
-    rwa [hf]
+    simp only [Set.mem_union, Set.mem_singleton_iff, Set.mem_star] at hf
+    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
+    obtain (rfl | rfl) := hf
+    all_goals assumption
   | zero => exact zero
   | add _ _ _ _ hf hg => exact add _ _ hf hg
   | mul _ _ _ _ hf hg => exact mul _ _ hf hg
   | smul _ _ _ hf => exact smul _ _ hf
-  | star _ _ hf => exact star _ hf
 
 open Topology in
 @[elab_as_elim]
 theorem ContinuousMapZero.induction_on_of_compact {s : Set 𝕜} [Zero s] (h0 : ((0 : s) : 𝕜) = 0)
     [CompactSpace s] {p : C(s, 𝕜)₀ → Prop} (zero : p 0) (id : p (.id h0))
-    (add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
-    (smul : ∀ (r : 𝕜) f, p f → p (r • f)) (star : ∀ f, p f → p (star f))
+    (star_id : p (star (.id h0))) (add : ∀ f g, p f → p g → p (f + g))
+    (mul : ∀ f g, p f → p g → p (f * g)) (smul : ∀ (r : 𝕜) f, p f → p (r • f))
     (frequently : ∀ f, (∃ᶠ g in 𝓝 f, p g) → p f) (f : C(s, 𝕜)₀) :
     p f := by
-  refine f.induction_on h0 zero id add mul smul star fun h f ↦ frequently f ?_
+  refine f.induction_on h0 zero id star_id add mul smul fun h f ↦ frequently f ?_
   have := (ContinuousMapZero.adjoin_id_dense h0).closure_eq ▸ Set.mem_univ (x := f)
   exact mem_closure_iff_frequently.mp this |>.mp <| .of_forall h
 

From e6ba8e0a61b2e29769b333a35aa978c7d3e46e39 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Sat, 26 Oct 2024 11:58:36 +0000
Subject: [PATCH 3/9] feat(NumberTheory/LSeries/Positivity): new file (#18031)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We use the newly added positivity results for holomorphic functions to show that the L-function associated to a sequence `a : ℕ → ℂ` such that `a 1 > 0` and `a n` is nonnegative real for all `n` takes positive real values on the real axis.

From [EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts); this is needed to prove the non-vanishing at `s = 1` of Dirichlet L-functions of nontrivial quadratic characters.
---
 Mathlib.lean                                  |   1 +
 .../Analysis/SpecialFunctions/Pow/Real.lean   |   7 ++
 Mathlib/NumberTheory/LSeries/Basic.lean       |  14 +++
 Mathlib/NumberTheory/LSeries/Positivity.lean  | 109 ++++++++++++++++++
 4 files changed, 131 insertions(+)
 create mode 100644 Mathlib/NumberTheory/LSeries/Positivity.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 61df8bf2227e8..4ddb054c46958 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3582,6 +3582,7 @@ import Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
 import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
 import Mathlib.NumberTheory.LSeries.Linearity
 import Mathlib.NumberTheory.LSeries.MellinEqDirichlet
+import Mathlib.NumberTheory.LSeries.Positivity
 import Mathlib.NumberTheory.LSeries.RiemannZeta
 import Mathlib.NumberTheory.LSeries.ZMod
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
index abdc88a5f991e..a2e922b310ba9 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@@ -997,6 +997,13 @@ lemma abs_cpow_inv_two_im (x : ℂ) : |(x ^ (2⁻¹ : ℂ)).im| = sqrt ((abs x -
     ← Real.sqrt_eq_rpow, _root_.abs_mul, _root_.abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
     ← sqrt_mul (abs.nonneg _), ← mul_div_assoc, mul_sub, mul_one, abs_mul_cos_arg]
 
+open scoped ComplexOrder in
+lemma inv_natCast_cpow_ofReal_pos {n : ℕ} (hn : n ≠ 0) (x : ℝ) :
+    0 < ((n : ℂ) ^ (x : ℂ))⁻¹ := by
+  refine RCLike.inv_pos_of_pos ?_
+  rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']
+  positivity
+
 end Complex
 
 section Tactics
diff --git a/Mathlib/NumberTheory/LSeries/Basic.lean b/Mathlib/NumberTheory/LSeries/Basic.lean
index 7221b06b0360f..99720f95d8532 100644
--- a/Mathlib/NumberTheory/LSeries/Basic.lean
+++ b/Mathlib/NumberTheory/LSeries/Basic.lean
@@ -111,6 +111,20 @@ lemma norm_term_le_of_re_le_re (f : ℕ → ℂ) {s s' : ℂ} (h : s.re ≤ s'.r
   next => rfl
   next hn => gcongr; exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn
 
+section positivity
+
+open scoped ComplexOrder
+
+lemma term_nonneg {a : ℕ → ℂ} {n : ℕ} (h : 0 ≤ a n) (x : ℝ) : 0 ≤ term a x n := by
+  rw [term_def]
+  split_ifs with hn
+  exacts [le_rfl, mul_nonneg h (inv_natCast_cpow_ofReal_pos hn x).le]
+
+lemma term_pos {a : ℕ → ℂ} {n : ℕ} (hn : n ≠ 0) (h : 0 < a n) (x : ℝ) : 0 < term a x n := by
+  simpa only [term_of_ne_zero hn] using mul_pos h <| inv_natCast_cpow_ofReal_pos hn x
+
+end positivity
+
 end LSeries
 
 /-!
diff --git a/Mathlib/NumberTheory/LSeries/Positivity.lean b/Mathlib/NumberTheory/LSeries/Positivity.lean
new file mode 100644
index 0000000000000..b21893b9ed342
--- /dev/null
+++ b/Mathlib/NumberTheory/LSeries/Positivity.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2024 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck, David Loeffler, Michael Stoll
+-/
+import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.Complex.Positivity
+import Mathlib.NumberTheory.ArithmeticFunction
+import Mathlib.NumberTheory.LSeries.Deriv
+
+/-!
+# Positivity of values of L-series
+
+The main results of this file are as follows.
+
+* If `a : ℕ → ℂ` takes nonnegative real values and `a 1 > 0`, then `L a x > 0`
+  when `x : ℝ` is in the open half-plane of absolute convergence; see
+  `LSeries.positive` and `ArithmeticFunction.LSeries_positive`.
+
+* If in addition the L_series of `a` agrees on some open right half-plane where it
+  converges with an entire function `f`, then `f` is positive on the real axis;
+  see `LSeries.positive_of_eq_differentiable` and
+  `ArithmeticFunction.LSeries_positive_of_eq_differentiable`.
+-/
+
+open scoped ComplexOrder
+
+open Complex
+
+namespace LSeries
+
+/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
+real number in the domain of absolute convergence, then the `n`th iterated derivative
+of the associated L-series is nonnegative real when `n` is even and nonpositive real
+when `n` is odd. -/
+lemma iteratedDeriv_alternating {a : ℕ → ℂ} (hn : 0 ≤ a) {x : ℝ}
+    (h : LSeries.abscissaOfAbsConv a < x) (n : ℕ) :
+    0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) x := by
+  rw [LSeries_iteratedDeriv _ h, LSeries, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨n, rfl⟩,
+    one_mul]
+  refine tsum_nonneg fun k ↦ ?_
+  rw [LSeries.term_def]
+  split
+  · exact le_rfl
+  · refine mul_nonneg ?_ <| (inv_natCast_cpow_ofReal_pos (by assumption) x).le
+    induction n with
+    | zero => simpa only [Function.iterate_zero, id_eq] using hn k
+    | succ n IH =>
+        rw [Function.iterate_succ_apply']
+        refine mul_nonneg ?_ IH
+        simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]
+
+/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1` is positive,
+then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`. -/
+lemma positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ} (hx : abscissaOfAbsConv a < x) :
+    0 < LSeries a x := by
+  rw [LSeries]
+  refine tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x
+  exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simpa only [ofReal_re] using hx
+
+/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1`
+is positive, and the L-series of `a` agrees with an entire function `f` on some open
+right half-plane where it converges, then `f` is real and positive on `ℝ`. -/
+lemma positive_of_differentiable_of_eqOn {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {f : ℂ → ℂ}
+    (hf : Differentiable ℂ f) {x : ℝ} (hx : abscissaOfAbsConv a ≤ x)
+    (hf' : {s | x < s.re}.EqOn f (LSeries a)) (y : ℝ) :
+    0 < f y := by
+  have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)
+  have hxy' : abscissaOfAbsConv a < max x y + 1 := hx.trans_lt <| mod_cast hxy
+  have hys : (max x y + 1 : ℂ) ∈ {s | x < s.re} := by
+    simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]
+  have hfx : 0 < f (max x y + 1) := by
+    simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'
+  refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)
+  · have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
+    simpa only [hf'.iteratedDeriv_of_isOpen hs n hys, ofReal_add, ofReal_one] using
+      iteratedDeriv_alternating ha₀ hxy' n
+  · exact_mod_cast (le_max_right x y).trans (lt_add_one _).le
+
+end LSeries
+
+namespace ArithmeticFunction
+
+/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
+real number in the domain of absolute convergence, then the `n`th iterated derivative
+of the associated L-series is nonnegative real when `n` is even and nonpositive real
+when `n` is odd. -/
+lemma iteratedDeriv_LSeries_alternating (a : ArithmeticFunction ℂ) (hn : ∀ n, 0 ≤ a n) {x : ℝ}
+    (h : LSeries.abscissaOfAbsConv a < x) (n : ℕ) :
+    0 ≤ (-1) ^ n * iteratedDeriv n (LSeries (a ·)) x :=
+  LSeries.iteratedDeriv_alternating hn h n
+
+/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1` is
+positive, then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`. -/
+lemma LSeries_positive {a : ℕ → ℂ} (ha₀ : 0 ≤ a) (ha₁ : 0 < a 1) {x : ℝ}
+    (hx : LSeries.abscissaOfAbsConv a < x) :
+    0 < LSeries a x :=
+  LSeries.positive ha₀ ha₁ hx
+
+/-- If all values of a `ℂ`-valued arithmetic function `a` are nonnegative reals and `a 1`
+is positive, and the L-series of `a` agrees with an entire function `f` on some open
+right half-plane where it converges, then `f` is real and positive on `ℝ`. -/
+lemma LSeries_positive_of_differentiable_of_eqOn {a : ArithmeticFunction ℂ} (ha₀ : 0 ≤ (a ·))
+    (ha₁ : 0 < a 1) {f : ℂ → ℂ} (hf : Differentiable ℂ f) {x : ℝ}
+    (hx : LSeries.abscissaOfAbsConv a ≤ x) (hf' : {s | x < s.re}.EqOn f (LSeries a)) (y : ℝ) :
+    0 < f y :=
+  LSeries.positive_of_differentiable_of_eqOn ha₀ ha₁ hf hx hf' y
+
+end ArithmeticFunction

From 83461cc0d7b87880c93523b2ae1df94508776b53 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Sat, 26 Oct 2024 11:58:37 +0000
Subject: [PATCH 4/9] feat: miscellaneous results about inertia degree (#18111)

From flt-regular.
---
 Mathlib/NumberTheory/RamificationInertia.lean | 37 +++++++++++++++++++
 Mathlib/RingTheory/Ideal/Maps.lean            |  2 +
 2 files changed, 39 insertions(+)

diff --git a/Mathlib/NumberTheory/RamificationInertia.lean b/Mathlib/NumberTheory/RamificationInertia.lean
index 71fc4378b8d5f..cd2da449ce790 100644
--- a/Mathlib/NumberTheory/RamificationInertia.lean
+++ b/Mathlib/NumberTheory/RamificationInertia.lean
@@ -124,6 +124,19 @@ theorem le_comap_pow_ramificationIdx : p ≤ comap f (P ^ ramificationIdx f p P)
 theorem le_comap_of_ramificationIdx_ne_zero (h : ramificationIdx f p P ≠ 0) : p ≤ comap f P :=
   Ideal.map_le_iff_le_comap.mp <| le_pow_ramificationIdx.trans <| Ideal.pow_le_self <| h
 
+variable {S₁: Type*} [CommRing S₁] [Algebra R S₁]
+
+lemma ramificationIdx_comap_eq [Algebra R S] (e : S ≃ₐ[R] S₁) (P : Ideal S₁) :
+    ramificationIdx (algebraMap R S) p (P.comap e) = ramificationIdx (algebraMap R S₁) p P := by
+  dsimp only [ramificationIdx]
+  congr
+  ext n
+  simp only [Set.mem_setOf_eq, Ideal.map_le_iff_le_comap]
+  rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
+    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
+    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
+    AlgHom.comp_algebraMap]
+
 namespace IsDedekindDomain
 
 variable [IsDedekindDomain S]
@@ -202,6 +215,30 @@ theorem inertiaDeg_algebraMap [Algebra R S] [Algebra (R ⧸ p) (S ⧸ P)]
   rw [Ideal.Quotient.lift_mk, ← Ideal.Quotient.algebraMap_eq P, ← IsScalarTower.algebraMap_eq,
     ← Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
 
+lemma inertiaDeg_comap_eq [Algebra R S] (e : S ≃ₐ[R] S₁) (P : Ideal S₁) [p.IsMaximal] :
+    inertiaDeg (algebraMap R S) p (P.comap e) = inertiaDeg (algebraMap R S₁) p P := by
+  dsimp only [Ideal.inertiaDeg]
+  have : (P.comap e).comap (algebraMap R S) = p ↔ P.comap (algebraMap R S₁) = p := by
+    rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
+  split
+  swap
+  · rw [dif_neg]; rwa [← this]
+  rw [dif_pos (this.mp ‹_›)]
+  apply (config := { allowSynthFailures := true }) LinearEquiv.finrank_eq
+  have E := quotientEquivAlg (P.comap e) P e (map_comap_of_surjective _ e.surjective P).symm
+  apply (config := {allowSynthFailures := true }) LinearEquiv.mk
+  case toLinearMap =>
+    apply (config := {allowSynthFailures := true }) LinearMap.mk
+    swap
+    · exact E.toLinearMap.toAddHom
+    · intro r x
+      show E (_ * _) = _ * (E x)
+      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
+      simp only [Quotient.mk_comp_algebraMap, Quotient.lift_mk, _root_.map_mul, AlgEquiv.commutes,
+        RingHomCompTriple.comp_apply]
+  · exact E.left_inv
+  · exact E.right_inv
+
 end DecEq
 
 section FinrankQuotientMap
diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean
index 0462faa6fbffb..725382c711dc9 100644
--- a/Mathlib/RingTheory/Ideal/Maps.lean
+++ b/Mathlib/RingTheory/Ideal/Maps.lean
@@ -51,6 +51,8 @@ def comap [RingHomClass F R S] (I : Ideal S) : Ideal R where
 @[simp]
 theorem coe_comap [RingHomClass F R S] (I : Ideal S) : (comap f I : Set R) = f ⁻¹' I := rfl
 
+lemma comap_coe [RingHomClass F R S] (I : Ideal S) : I.comap (f : R →+* S) = I.comap f := rfl
+
 variable {f}
 
 theorem map_mono (h : I ≤ J) : map f I ≤ map f J :=

From 97a5c4677a62fce8992b5c438e12815686b3e50a Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Sat, 26 Oct 2024 11:58:38 +0000
Subject: [PATCH 5/9] feat(Complex/Order): add some results about
 multiplication of a real and a complex (#18136)

This PR is part of the proof of the Analytic Class Number Formula.



Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
---
 Mathlib/Analysis/RCLike/Basic.lean | 14 ++++++++++++++
 Mathlib/Data/Complex/Order.lean    |  6 ++++++
 2 files changed, 20 insertions(+)

diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
index 6df3640fd74f1..039e769c1b674 100644
--- a/Mathlib/Analysis/RCLike/Basic.lean
+++ b/Mathlib/Analysis/RCLike/Basic.lean
@@ -872,6 +872,20 @@ instance {A : Type*} [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrdere
 
 scoped[ComplexOrder] attribute [instance] StarModule.instOrderedSMul
 
+theorem ofReal_mul_pos_iff (x : ℝ) (z : K) :
+    0 < x * z ↔ (x < 0 ∧ z < 0) ∨ (0 < x ∧ 0 < z) := by
+  simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]
+  obtain hx | hx | hx := lt_trichotomy x 0
+  · simp only [mul_pos_iff, not_lt_of_gt hx, false_and, hx, true_and, false_or, mul_eq_zero, hx.ne,
+      or_false]
+  · simp only [hx, zero_mul, lt_self_iff_false, false_and, false_or]
+  · simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero,
+      hx.ne', false_or]
+
+theorem ofReal_mul_neg_iff (x : ℝ) (z : K) :
+    x * z < 0 ↔ (x < 0 ∧ 0 < z) ∨ (0 < x ∧ z < 0) := by
+  simpa only [mul_neg, neg_pos, neg_neg_iff_pos] using ofReal_mul_pos_iff x (-z)
+
 end Order
 
 section CleanupLemmas
diff --git a/Mathlib/Data/Complex/Order.lean b/Mathlib/Data/Complex/Order.lean
index 47d0dd85378f3..9e641fe376939 100644
--- a/Mathlib/Data/Complex/Order.lean
+++ b/Mathlib/Data/Complex/Order.lean
@@ -63,6 +63,12 @@ theorem nonneg_iff {z : ℂ} : 0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im :=
 theorem pos_iff {z : ℂ} : 0 < z ↔ 0 < z.re ∧ 0 = z.im :=
   lt_def
 
+theorem nonpos_iff {z : ℂ} : z ≤ 0 ↔ z.re ≤ 0 ∧ z.im = 0 :=
+  le_def
+
+theorem neg_iff {z : ℂ} : z < 0 ↔ z.re < 0 ∧ z.im = 0 :=
+  lt_def
+
 @[simp, norm_cast]
 theorem real_le_real {x y : ℝ} : (x : ℂ) ≤ (y : ℂ) ↔ x ≤ y := by simp [le_def, ofReal]
 

From 85ae613a6bf0c17553a1f50756c49f8d17decb2a Mon Sep 17 00:00:00 2001
From: Thomas Browning <tb65536@uw.edu>
Date: Sat, 26 Oct 2024 11:58:39 +0000
Subject: [PATCH 6/9] feat(Algebra/BigOperators/GroupWithZero/Action): Action
 of group permutes a product (#18148)

This PR adds a couple lemmas for when the action of a group permutes a product.



Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
---
 .../Algebra/BigOperators/GroupWithZero/Action.lean   | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
index c969334d05c0a..6f377d4ff77be 100644
--- a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
+++ b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
@@ -73,6 +73,18 @@ theorem smul_finprod' {ι : Sort*} [Finite ι] {f : ι → β} (r : α) :
   simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp),
     finprod_eq_prod_of_fintype, Finset.smul_prod']
 
+variable {G : Type*} [Group G] [MulDistribMulAction G β]
+
+theorem Finset.smul_prod_perm [Fintype G] (b : β) (g : G) :
+    (g • ∏ h : G, h • b) = ∏ h : G, h • b := by
+  simp only [smul_prod', smul_smul]
+  exact Finset.prod_bijective (g * ·) (Group.mulLeft_bijective g) (by simp) (fun _ _ ↦ rfl)
+
+theorem smul_finprod_perm [Finite G] (b : β) (g : G) :
+    (g • ∏ᶠ h : G, h • b) = ∏ᶠ h : G, h • b := by
+  cases nonempty_fintype G
+  simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]
+
 end
 
 namespace List

From a0de06886e296efb09c13ac6af1066a06c2be252 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Sat, 26 Oct 2024 11:58:41 +0000
Subject: [PATCH 7/9] feat(LSeries/RiemannZeta): versions of the residue
 computation of the zeta function with tsum and for a real variable (#18166)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The proof of:
```
Tendsto (fun s : ℝ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℝ) ^ s) (𝓝[>] 1) (𝓝 1)
```
using the existing result for the complex variable.

This PR is part of the proof of the Analytic Class Number Formula.
---
 Mathlib/NumberTheory/LSeries/RiemannZeta.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/Mathlib/NumberTheory/LSeries/RiemannZeta.lean b/Mathlib/NumberTheory/LSeries/RiemannZeta.lean
index bcc35496bf6f6..0b29f4b14b30a 100644
--- a/Mathlib/NumberTheory/LSeries/RiemannZeta.lean
+++ b/Mathlib/NumberTheory/LSeries/RiemannZeta.lean
@@ -202,6 +202,25 @@ theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) :
 lemma riemannZeta_residue_one : Tendsto (fun s ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1) := by
   exact hurwitzZetaEven_residue_one 0
 
+/-- The residue of `ζ(s)` at `s = 1` is equal to 1, expressed using `tsum`. -/
+theorem tendsto_sub_mul_tsum_nat_cpow :
+    Tendsto (fun s : ℂ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℂ) ^ s) (𝓝[{s | 1 < re s}] 1) (𝓝 1) := by
+  refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_
+  · simp only [subset_compl_singleton_iff, mem_setOf_eq, one_re, not_lt, le_refl]
+  · filter_upwards [eventually_mem_nhdsWithin] with s hs using
+      congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs
+
+/-- The residue of `ζ(s)` at `s = 1` is equal to 1 expressed using `tsum` and for a
+real variable. -/
+theorem tendsto_sub_mul_tsum_nat_rpow :
+    Tendsto (fun s : ℝ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℝ) ^ s) (𝓝[>] 1) (𝓝 1) := by
+  rw [← tendsto_ofReal_iff, ofReal_one]
+  have : Tendsto (fun s : ℝ ↦ (s : ℂ)) (𝓝[>] 1) (𝓝[{s | 1 < re s}] 1) :=
+    continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin (fun _ _ ↦ by aesop)
+  apply (tendsto_sub_mul_tsum_nat_cpow.comp this).congr fun s ↦ ?_
+  simp only [one_div, Function.comp_apply, ofReal_mul, ofReal_sub, ofReal_one, ofReal_tsum,
+    ofReal_inv, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast]
+
 /- naming scheme was changed from `riemannCompletedZeta` to `completedRiemannZeta`; add
 aliases for the old names -/
 section aliases

From 2e87d1a8a668a70fa5b9f24085270036824c1902 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 26 Oct 2024 11:58:42 +0000
Subject: [PATCH 8/9] =?UTF-8?q?feat:=20`StarOrderedRing=20(=CE=B1=20=C3=97?=
 =?UTF-8?q?=20=CE=B2)`=20(#18209)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The `Pi` version (for `Finite` indices) would be more work due to missing API around `Submonoid.pi`.
---
 Mathlib.lean                                  |  1 +
 Mathlib/Algebra/Group/Subgroup/Basic.lean     |  9 ++++++
 .../Algebra/Group/Submonoid/Operations.lean   |  9 ++++++
 Mathlib/Algebra/Order/Star/Prod.lean          | 30 +++++++++++++++++++
 Mathlib/Logic/Basic.lean                      |  4 +++
 5 files changed, 53 insertions(+)
 create mode 100644 Mathlib/Algebra/Order/Star/Prod.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 4ddb054c46958..81e1f700393e7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -710,6 +710,7 @@ import Mathlib.Algebra.Order.Ring.Unbundled.Rat
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.Star.Basic
 import Mathlib.Algebra.Order.Star.Conjneg
+import Mathlib.Algebra.Order.Star.Prod
 import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Algebra.Order.Sub.Prod
diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
index 9f971900d0349..ca7a9f590871e 100644
--- a/Mathlib/Algebra/Group/Subgroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -1401,6 +1401,15 @@ theorem prod_le_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
 theorem prod_eq_bot_iff {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥ := by
   simpa only [← Subgroup.toSubmonoid_eq] using Submonoid.prod_eq_bot_iff
 
+@[to_additive closure_prod]
+theorem closure_prod {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
+    closure (s ×ˢ t) = (closure s).prod (closure t) :=
+  le_antisymm
+    (closure_le _ |>.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
+    (prod_le_iff.2 ⟨
+      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _x hx => subset_closure ⟨hx, ht⟩,
+      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
+
 /-- Product of subgroups is isomorphic to their product as groups. -/
 @[to_additive prodEquiv
       "Product of additive subgroups is isomorphic to their product
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
index e5ca00f78346e..ee672456df581 100644
--- a/Mathlib/Algebra/Group/Submonoid/Operations.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -715,6 +715,15 @@ theorem prod_le_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)}
       simpa using h2
     simpa using Submonoid.mul_mem _ h1' h2'
 
+@[to_additive closure_prod]
+theorem closure_prod {s : Set M} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
+    closure (s ×ˢ t) = (closure s).prod (closure t) :=
+  le_antisymm
+    (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
+    (prod_le_iff.2 ⟨
+      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, ht⟩,
+      map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)
+
 end Submonoid
 
 namespace MonoidHom
diff --git a/Mathlib/Algebra/Order/Star/Prod.lean b/Mathlib/Algebra/Order/Star/Prod.lean
new file mode 100644
index 0000000000000..f2375c7d57a81
--- /dev/null
+++ b/Mathlib/Algebra/Order/Star/Prod.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Algebra.Order.Star.Basic
+import Mathlib.Algebra.Star.Prod
+import Mathlib.Algebra.Ring.Prod
+
+/-!
+# Products of star-ordered rings
+-/
+
+variable {α β : Type*}
+
+open AddSubmonoid in
+instance Prod.instStarOrderedRing
+    [NonUnitalSemiring α] [NonUnitalSemiring β] [PartialOrder α] [PartialOrder β]
+    [StarRing α] [StarRing β] [StarOrderedRing α] [StarOrderedRing β] :
+    StarOrderedRing (α × β) where
+  le_iff := Prod.forall.2 fun xa xy => Prod.forall.2 fun ya yb => by
+    have :
+        closure (Set.range fun s : α × β ↦ star s * s) =
+          (closure <| Set.range fun s : α ↦ star s * s).prod
+          (closure <| Set.range fun s : β ↦ star s * s) := by
+      rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩),
+        Set.prod_range_range_eq]
+      simp_rw [Prod.mul_def, Prod.star_def]
+    simp only [mk_le_mk, Prod.exists, mk_add_mk, mk.injEq, StarOrderedRing.le_iff, this,
+      AddSubmonoid.mem_prod, exists_and_exists_comm, and_and_and_comm]
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index b4258e60f795c..cf41e0848cfdf 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -485,6 +485,10 @@ theorem imp_forall_iff {α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x,
 theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y :=
   ⟨fun ⟨x, y, h⟩ ↦ ⟨y, x, h⟩, fun ⟨y, x, h⟩ ↦ ⟨x, y, h⟩⟩
 
+theorem exists_and_exists_comm {P : α → Prop} {Q : β → Prop} :
+    (∃ a, P a) ∧ (∃ b, Q b) ↔ ∃ a b, P a ∧ Q b :=
+  ⟨fun ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ↦ ⟨a, b, ⟨ha, hb⟩⟩, fun ⟨a, b, ⟨ha, hb⟩⟩ ↦ ⟨⟨a, ha⟩, ⟨b, hb⟩⟩⟩
+
 export Classical (not_forall)
 
 theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not

From 3e1e5737321bf246eb2737892f1d0728b1192b66 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Sat, 26 Oct 2024 11:58:43 +0000
Subject: [PATCH 9/9] feat(NumberField/Discriminant): Compute some lattices
 covolume (#18246)

This PR is part of the proof of the Analytic Class Number Formula.
---
 .../NumberField/Discriminant/Basic.lean       | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean b/Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
index 69a827b17b1c0..013f14fce60b1 100644
--- a/Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Xavier Roblot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
+import Mathlib.Algebra.Module.ZLattice.Covolume
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
 import Mathlib.Tactic.Rify
@@ -72,6 +73,24 @@ theorem _root_.NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis
     stdBasis_repr_eq_matrixToStdBasis_mul K _ (fun _ => rfl)]
   rfl
 
+theorem _root_.NumberField.mixedEmbedding.covolume_integerLattice :
+    ZLattice.covolume (mixedEmbedding.integerLattice K) =
+      (2 ⁻¹) ^ nrComplexPlaces K * √|discr K| := by
+  rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_integerLattice K),
+    volume_fundamentalDomain_latticeBasis, ENNReal.toReal_mul, ENNReal.toReal_pow,
+    ENNReal.toReal_inv, toReal_ofNat, ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm,
+    Int.norm_eq_abs]
+
+theorem _root_.NumberField.mixedEmbedding.covolume_idealLattice (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
+    ZLattice.covolume (mixedEmbedding.idealLattice K I) =
+      (FractionalIdeal.absNorm (I : FractionalIdeal (𝓞 K)⁰ K)) *
+        (2 ⁻¹) ^ nrComplexPlaces K * √|discr K| := by
+  rw [ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_idealLattice K I),
+    volume_fundamentalDomain_fractionalIdealLatticeBasis, volume_fundamentalDomain_latticeBasis,
+    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_inv, toReal_ofNat,
+    ENNReal.coe_toReal, Real.coe_sqrt, coe_nnnorm, Int.norm_eq_abs,
+    ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.val)), mul_assoc]
+
 theorem exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
     ∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧
       |Algebra.norm ℚ (a : K)| ≤ FractionalIdeal.absNorm I.1 * (4 / π) ^ nrComplexPlaces K *