diff --git a/.github/workflows/nightly_detect_failure.yml b/.github/workflows/nightly_detect_failure.yml
index e1cfd9147086b..140f115408e95 100644
--- a/.github/workflows/nightly_detect_failure.yml
+++ b/.github/workflows/nightly_detect_failure.yml
@@ -210,7 +210,7 @@ jobs:
             bump_branch_suffix = bump_branch.replace('bump/', '')
             payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
             payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
-            payload += f"```bash\n./scripts/create-adaptation-pr.sh {bump_branch_suffix} {current_version}\n```\n"
+            payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
             # Only post if the message is different
             # We compare the first 160 characters, since that includes the date and bump version
             if not messages or messages[0]['content'][:160] != payload[:160]:
diff --git a/Archive/Hairer.lean b/Archive/Hairer.lean
index acd326c0b13bf..e9b91c32132a8 100644
--- a/Archive/Hairer.lean
+++ b/Archive/Hairer.lean
@@ -100,7 +100,7 @@ lemma inj_L : Injective (L ι) :=
         fun g hg _h2g g_supp ↦ by
           simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩)
     simp_rw [MvPolynomial.funext_iff, map_zero]
-    refine fun x ↦ AnalyticOn.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
+    refine fun x ↦ AnalyticOnNhd.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
       |>.eqOn_zero_of_preconnected_of_eventuallyEq_zero
       (preconnectedSpace_iff_univ.mp inferInstance) (z₀ := 0) trivial
       (Filter.mem_of_superset (Metric.ball_mem_nhds 0 zero_lt_one) ?_) trivial
diff --git a/Mathlib.lean b/Mathlib.lean
index aff4c29162bbe..7ef725424dfcf 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -56,7 +56,6 @@ import Mathlib.Algebra.BigOperators.Ring.Multiset
 import Mathlib.Algebra.BigOperators.Ring.Nat
 import Mathlib.Algebra.BigOperators.RingEquiv
 import Mathlib.Algebra.BigOperators.WithTop
-import Mathlib.Algebra.Bounds
 import Mathlib.Algebra.Category.AlgebraCat.Basic
 import Mathlib.Algebra.Category.AlgebraCat.Limits
 import Mathlib.Algebra.Category.AlgebraCat.Monoidal
@@ -566,6 +565,7 @@ import Mathlib.Algebra.Order.Field.Canonical.Defs
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Field.InjSurj
 import Mathlib.Algebra.Order.Field.Pi
+import Mathlib.Algebra.Order.Field.Pointwise
 import Mathlib.Algebra.Order.Field.Power
 import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Algebra.Order.Field.Subfield
@@ -577,6 +577,7 @@ import Mathlib.Algebra.Order.Group.Action
 import Mathlib.Algebra.Order.Group.Action.Synonym
 import Mathlib.Algebra.Order.Group.Basic
 import Mathlib.Algebra.Order.Group.Bounds
+import Mathlib.Algebra.Order.Group.CompleteLattice
 import Mathlib.Algebra.Order.Group.Cone
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.DenselyOrdered
@@ -589,6 +590,8 @@ import Mathlib.Algebra.Order.Group.MinMax
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Order.Group.OrderIso
 import Mathlib.Algebra.Order.Group.PiLex
+import Mathlib.Algebra.Order.Group.Pointwise.Bounds
+import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Group.Synonym
@@ -644,7 +647,6 @@ import Mathlib.Algebra.Order.Nonneg.Floor
 import Mathlib.Algebra.Order.Nonneg.Module
 import Mathlib.Algebra.Order.Nonneg.Ring
 import Mathlib.Algebra.Order.Pi
-import Mathlib.Algebra.Order.Pointwise
 import Mathlib.Algebra.Order.Positive.Field
 import Mathlib.Algebra.Order.Positive.Ring
 import Mathlib.Algebra.Order.Rearrangement
diff --git a/Mathlib/Algebra/Bounds.lean b/Mathlib/Algebra/Bounds.lean
deleted file mode 100644
index 8c9ff1cb53079..0000000000000
--- a/Mathlib/Algebra/Bounds.lean
+++ /dev/null
@@ -1,167 +0,0 @@
-/-
-Copyright (c) 2021 Yury Kudryashov. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
--/
-import Mathlib.Algebra.Group.Pointwise.Set
-import Mathlib.Algebra.Order.Group.OrderIso
-import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
-import Mathlib.Order.Bounds.OrderIso
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
-
-/-!
-# Upper/lower bounds in ordered monoids and groups
-
-In this file we prove a few facts like “`-s` is bounded above iff `s` is bounded below”
-(`bddAbove_neg`).
--/
-
-
-open Function Set
-
-open Pointwise
-
-section InvNeg
-
-variable {G : Type*} [Group G] [Preorder G] [CovariantClass G G (· * ·) (· ≤ ·)]
-  [CovariantClass G G (swap (· * ·)) (· ≤ ·)] {s : Set G} {a : G}
-
-@[to_additive (attr := simp)]
-theorem bddAbove_inv : BddAbove s⁻¹ ↔ BddBelow s :=
-  (OrderIso.inv G).bddAbove_preimage
-
-@[to_additive (attr := simp)]
-theorem bddBelow_inv : BddBelow s⁻¹ ↔ BddAbove s :=
-  (OrderIso.inv G).bddBelow_preimage
-
-@[to_additive]
-theorem BddAbove.inv (h : BddAbove s) : BddBelow s⁻¹ :=
-  bddBelow_inv.2 h
-
-@[to_additive]
-theorem BddBelow.inv (h : BddBelow s) : BddAbove s⁻¹ :=
-  bddAbove_inv.2 h
-
-@[to_additive (attr := simp)]
-theorem isLUB_inv : IsLUB s⁻¹ a ↔ IsGLB s a⁻¹ :=
-  (OrderIso.inv G).isLUB_preimage
-
-@[to_additive]
-theorem isLUB_inv' : IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a :=
-  (OrderIso.inv G).isLUB_preimage'
-
-@[to_additive]
-theorem IsGLB.inv (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹ :=
-  isLUB_inv'.2 h
-
-@[to_additive (attr := simp)]
-theorem isGLB_inv : IsGLB s⁻¹ a ↔ IsLUB s a⁻¹ :=
-  (OrderIso.inv G).isGLB_preimage
-
-@[to_additive]
-theorem isGLB_inv' : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a :=
-  (OrderIso.inv G).isGLB_preimage'
-
-@[to_additive]
-theorem IsLUB.inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ :=
-  isGLB_inv'.2 h
-
-@[to_additive]
-lemma BddBelow.range_inv {α : Type*} {f : α → G} (hf : BddBelow (range f)) :
-    BddAbove (range (fun x => (f x)⁻¹)) :=
-  hf.range_comp (OrderIso.inv G).monotone
-
-@[to_additive]
-lemma BddAbove.range_inv {α : Type*} {f : α → G} (hf : BddAbove (range f)) :
-    BddBelow (range (fun x => (f x)⁻¹)) :=
-  BddBelow.range_inv (G := Gᵒᵈ) hf
-
-end InvNeg
-
-section mul_add
-
-variable {M : Type*} [Mul M] [Preorder M] [CovariantClass M M (· * ·) (· ≤ ·)]
-  [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
-
-@[to_additive]
-theorem mul_mem_upperBounds_mul {s t : Set M} {a b : M} (ha : a ∈ upperBounds s)
-    (hb : b ∈ upperBounds t) : a * b ∈ upperBounds (s * t) :=
-  forall_image2_iff.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy)
-
-@[to_additive]
-theorem subset_upperBounds_mul (s t : Set M) :
-    upperBounds s * upperBounds t ⊆ upperBounds (s * t) :=
-  image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy
-
-@[to_additive]
-theorem mul_mem_lowerBounds_mul {s t : Set M} {a b : M} (ha : a ∈ lowerBounds s)
-    (hb : b ∈ lowerBounds t) : a * b ∈ lowerBounds (s * t) :=
-  mul_mem_upperBounds_mul (M := Mᵒᵈ) ha hb
-
-@[to_additive]
-theorem subset_lowerBounds_mul (s t : Set M) :
-    lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t) :=
-  subset_upperBounds_mul (M := Mᵒᵈ) _ _
-
-@[to_additive]
-theorem BddAbove.mul {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) :=
-  (Nonempty.mul hs ht).mono (subset_upperBounds_mul s t)
-
-@[to_additive]
-theorem BddBelow.mul {s t : Set M} (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) :=
-  (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)
-
-@[to_additive]
-lemma BddAbove.range_mul {α : Type*} {f g : α → M} (hf : BddAbove (range f))
-    (hg : BddAbove (range g)) : BddAbove (range (fun x => f x * g x)) :=
-  BddAbove.range_comp (f := fun x => (⟨f x, g x⟩ : M × M))
-    (bddAbove_range_prod.mpr ⟨hf, hg⟩) (Monotone.mul' monotone_fst monotone_snd)
-
-@[to_additive]
-lemma BddBelow.range_mul {α : Type*} {f g : α → M} (hf : BddBelow (range f))
-    (hg : BddBelow (range g)) : BddBelow (range (fun x => f x * g x)) :=
-  BddAbove.range_mul (M := Mᵒᵈ) hf hg
-
-end mul_add
-
-section ConditionallyCompleteLattice
-
-section Right
-
-variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G]
-  [CovariantClass G G (Function.swap (· * ·)) (· ≤ ·)] [Nonempty ι] {f : ι → G}
-
-@[to_additive]
-theorem ciSup_mul (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a :=
-  (OrderIso.mulRight a).map_ciSup hf
-
-@[to_additive]
-theorem ciSup_div (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by
-  simp only [div_eq_mul_inv, ciSup_mul hf]
-
-@[to_additive]
-theorem ciInf_mul (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) * a = ⨅ i, f i * a :=
-  (OrderIso.mulRight a).map_ciInf hf
-
-@[to_additive]
-theorem ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a := by
-  simp only [div_eq_mul_inv, ciInf_mul hf]
-
-end Right
-
-section Left
-
-variable {ι : Sort*} {G : Type*} [Group G] [ConditionallyCompleteLattice G]
-  [CovariantClass G G (· * ·) (· ≤ ·)] [Nonempty ι] {f : ι → G}
-
-@[to_additive]
-theorem mul_ciSup (hf : BddAbove (range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i :=
-  (OrderIso.mulLeft a).map_ciSup hf
-
-@[to_additive]
-theorem mul_ciInf (hf : BddBelow (range f)) (a : G) : (a * ⨅ i, f i) = ⨅ i, a * f i :=
-  (OrderIso.mulLeft a).map_ciInf hf
-
-end Left
-
-end ConditionallyCompleteLattice
diff --git a/Mathlib/Algebra/Order/CompleteField.lean b/Mathlib/Algebra/Order/CompleteField.lean
index 2c8942e53c15c..680ebceb3f631 100644
--- a/Mathlib/Algebra/Order/CompleteField.lean
+++ b/Mathlib/Algebra/Order/CompleteField.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best, Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Archimedean.Hom
-import Mathlib.Algebra.Order.Pointwise
+import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 /-!
diff --git a/Mathlib/Algebra/Order/Field/Pointwise.lean b/Mathlib/Algebra/Order/Field/Pointwise.lean
new file mode 100644
index 0000000000000..8f2b1867f0d73
--- /dev/null
+++ b/Mathlib/Algebra/Order/Field/Pointwise.lean
@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2021 Alex J. Best. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex J. Best, Yaël Dillies
+-/
+import Mathlib.Algebra.Group.Pointwise.Set
+import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.SMulWithZero
+
+/-!
+# Pointwise operations on ordered algebraic objects
+
+This file contains lemmas about the effect of pointwise operations on sets with an order structure.
+-/
+
+open Function Set
+open scoped Pointwise
+
+variable {α : Type*}
+
+namespace LinearOrderedField
+
+variable {K : Type*} [LinearOrderedField K] {a b r : K} (hr : 0 < r)
+include hr
+
+theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioo]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_lt_mul_left hr).mpr a_h_left_left
+    · exact (mul_lt_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Icc]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_le_mul_left hr).mpr a_h_left_left
+    · exact (mul_le_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ico]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_le_mul_left hr).mpr a_h_left_left
+    · exact (mul_lt_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_lt_mul_left hr).mpr a_h_left_left
+    · exact (mul_le_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_lt_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (lt_div_iff' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+theorem smul_Iio : r • Iio a = Iio (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_lt_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (div_lt_iff' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+theorem smul_Ici : r • Ici a = Ici (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_le_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (le_div_iff₀' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+theorem smul_Iic : r • Iic a = Iic (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_le_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (div_le_iff₀' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+end LinearOrderedField
diff --git a/Mathlib/Algebra/Order/Group/CompleteLattice.lean b/Mathlib/Algebra/Order/Group/CompleteLattice.lean
new file mode 100644
index 0000000000000..19c8f5fda8e68
--- /dev/null
+++ b/Mathlib/Algebra/Order/Group/CompleteLattice.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov
+-/
+import Mathlib.Algebra.Order.Group.OrderIso
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+/-!
+# Distributivity of group operations over supremum/infimum
+-/
+
+open Function Set
+
+variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
+
+section Right
+variable [CovariantClass G G (swap (· * ·)) (· ≤ ·)]
+
+@[to_additive]
+lemma ciSup_mul (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a :=
+  (OrderIso.mulRight a).map_ciSup hf
+
+@[to_additive]
+lemma ciSup_div (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by
+  simp only [div_eq_mul_inv, ciSup_mul hf]
+
+@[to_additive]
+lemma ciInf_mul (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) * a = ⨅ i, f i * a :=
+  (OrderIso.mulRight a).map_ciInf hf
+
+@[to_additive]
+lemma ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a := by
+  simp only [div_eq_mul_inv, ciInf_mul hf]
+
+end Right
+
+section Left
+variable [CovariantClass G G (· * ·) (· ≤ ·)]
+
+@[to_additive]
+lemma mul_ciSup (hf : BddAbove (range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i :=
+  (OrderIso.mulLeft a).map_ciSup hf
+
+@[to_additive]
+lemma mul_ciInf (hf : BddBelow (range f)) (a : G) : (a * ⨅ i, f i) = ⨅ i, a * f i :=
+  (OrderIso.mulLeft a).map_ciInf hf
+
+end Left
diff --git a/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean
new file mode 100644
index 0000000000000..e6a5407931b80
--- /dev/null
+++ b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Algebra.Group.Pointwise.Set
+import Mathlib.Algebra.Order.Group.OrderIso
+import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
+import Mathlib.Order.Bounds.OrderIso
+
+/-!
+# Upper/lower bounds in ordered monoids and groups
+
+In this file we prove a few facts like “`-s` is bounded above iff `s` is bounded below”
+(`bddAbove_neg`).
+-/
+
+open Function Set
+open scoped Pointwise
+
+variable {ι G M : Type*}
+
+section Mul
+variable [Mul M] [Preorder M] [CovariantClass M M (· * ·) (· ≤ ·)]
+  [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {f g : ι → M} {s t : Set M} {a b : M}
+
+@[to_additive]
+lemma mul_mem_upperBounds_mul (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) :
+    a * b ∈ upperBounds (s * t) := forall_image2_iff.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy)
+
+@[to_additive]
+lemma subset_upperBounds_mul (s t : Set M) : upperBounds s * upperBounds t ⊆ upperBounds (s * t) :=
+  image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy
+
+@[to_additive]
+lemma mul_mem_lowerBounds_mul (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) :
+    a * b ∈ lowerBounds (s * t) := mul_mem_upperBounds_mul (M := Mᵒᵈ) ha hb
+
+@[to_additive]
+lemma subset_lowerBounds_mul (s t : Set M) : lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t) :=
+  subset_upperBounds_mul (M := Mᵒᵈ) _ _
+
+@[to_additive]
+lemma BddAbove.mul (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) :=
+  (Nonempty.mul hs ht).mono (subset_upperBounds_mul s t)
+
+@[to_additive]
+lemma BddBelow.mul (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) :=
+  (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)
+
+@[to_additive]
+lemma BddAbove.range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) :
+    BddAbove (range fun i ↦ f i * g i) :=
+  .range_comp (f := fun i ↦ (f i, g i)) (bddAbove_range_prod.2 ⟨hf, hg⟩)
+    (monotone_fst.mul' monotone_snd)
+
+@[to_additive]
+lemma BddBelow.range_mul (hf : BddBelow (range f)) (hg : BddBelow (range g)) :
+    BddBelow (range fun i ↦ f i * g i) := BddAbove.range_mul (M := Mᵒᵈ) hf hg
+
+end Mul
+
+section InvNeg
+variable [Group G] [Preorder G] [CovariantClass G G (· * ·) (· ≤ ·)]
+  [CovariantClass G G (swap (· * ·)) (· ≤ ·)] {s : Set G} {a : G}
+
+@[to_additive (attr := simp)]
+theorem bddAbove_inv : BddAbove s⁻¹ ↔ BddBelow s :=
+  (OrderIso.inv G).bddAbove_preimage
+
+@[to_additive (attr := simp)]
+theorem bddBelow_inv : BddBelow s⁻¹ ↔ BddAbove s :=
+  (OrderIso.inv G).bddBelow_preimage
+
+@[to_additive]
+theorem BddAbove.inv (h : BddAbove s) : BddBelow s⁻¹ :=
+  bddBelow_inv.2 h
+
+@[to_additive]
+theorem BddBelow.inv (h : BddBelow s) : BddAbove s⁻¹ :=
+  bddAbove_inv.2 h
+
+@[to_additive (attr := simp)]
+theorem isLUB_inv : IsLUB s⁻¹ a ↔ IsGLB s a⁻¹ :=
+  (OrderIso.inv G).isLUB_preimage
+
+@[to_additive]
+theorem isLUB_inv' : IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a :=
+  (OrderIso.inv G).isLUB_preimage'
+
+@[to_additive]
+theorem IsGLB.inv (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹ :=
+  isLUB_inv'.2 h
+
+@[to_additive (attr := simp)]
+theorem isGLB_inv : IsGLB s⁻¹ a ↔ IsLUB s a⁻¹ :=
+  (OrderIso.inv G).isGLB_preimage
+
+@[to_additive]
+theorem isGLB_inv' : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a :=
+  (OrderIso.inv G).isGLB_preimage'
+
+@[to_additive]
+theorem IsLUB.inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ :=
+  isGLB_inv'.2 h
+
+@[to_additive]
+lemma BddBelow.range_inv {α : Type*} {f : α → G} (hf : BddBelow (range f)) :
+    BddAbove (range (fun x => (f x)⁻¹)) :=
+  hf.range_comp (OrderIso.inv G).monotone
+
+@[to_additive]
+lemma BddAbove.range_inv {α : Type*} {f : α → G} (hf : BddAbove (range f)) :
+    BddBelow (range (fun x => (f x)⁻¹)) :=
+  BddBelow.range_inv (G := Gᵒᵈ) hf
+
+end InvNeg
diff --git a/Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean b/Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
new file mode 100644
index 0000000000000..6f09d373cffd4
--- /dev/null
+++ b/Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Algebra.Order.Group.Pointwise.Bounds
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+/-!
+# Infima/suprema in ordered monoids and groups
+
+In this file we prove a few facts like “The infimum of `-s` is `-` the supremum of `s`”.
+
+## TODO
+
+`sSup (s • t) = sSup s • sSup t` and `sInf (s • t) = sInf s • sInf t` hold as well but
+`CovariantClass` is currently not polymorphic enough to state it.
+-/
+
+open Function Set
+open scoped Pointwise
+
+variable {ι G M : Type*}
+
+section ConditionallyCompleteLattice
+variable [ConditionallyCompleteLattice M]
+
+section One
+variable [One M]
+
+@[to_additive (attr := simp)] lemma csSup_one : sSup (1 : Set M) = 1 := csSup_singleton _
+@[to_additive (attr := simp)] lemma csInf_one : sInf (1 : Set M) = 1 := csInf_singleton _
+
+end One
+
+section Group
+variable [Group M] [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
+  {s t : Set M}
+
+@[to_additive]
+lemma csSup_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup s⁻¹ = (sInf s)⁻¹ := by
+  rw [← image_inv]
+  exact ((OrderIso.inv _).map_csInf' hs₀ hs₁).symm
+
+@[to_additive]
+lemma csInf_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sInf s⁻¹ = (sSup s)⁻¹ := by
+  rw [← image_inv]
+  exact ((OrderIso.inv _).map_csSup' hs₀ hs₁).symm
+
+@[to_additive]
+lemma csSup_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
+    sSup (s * t) = sSup s * sSup t :=
+  csSup_image2_eq_csSup_csSup (fun _ => (OrderIso.mulRight _).to_galoisConnection)
+    (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁
+
+@[to_additive]
+lemma csInf_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
+    sInf (s * t) = sInf s * sInf t :=
+  csInf_image2_eq_csInf_csInf (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection)
+    (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁
+
+@[to_additive]
+lemma csSup_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
+    sSup (s / t) = sSup s / sInf t := by
+  rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
+
+@[to_additive]
+lemma csInf_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
+    sInf (s / t) = sInf s / sSup t := by
+  rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
+
+end Group
+end ConditionallyCompleteLattice
+
+section CompleteLattice
+variable [CompleteLattice M]
+
+section One
+variable [One M]
+
+@[to_additive] lemma sSup_one : sSup (1 : Set M) = 1 := sSup_singleton
+@[to_additive] lemma sInf_one : sInf (1 : Set M) = 1 := sInf_singleton
+
+end One
+
+section Group
+variable [Group M] [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
+  (s t : Set M)
+
+@[to_additive]
+lemma sSup_inv (s : Set M) : sSup s⁻¹ = (sInf s)⁻¹ := by
+  rw [← image_inv, sSup_image]
+  exact ((OrderIso.inv M).map_sInf _).symm
+
+@[to_additive]
+lemma sInf_inv (s : Set M) : sInf s⁻¹ = (sSup s)⁻¹ := by
+  rw [← image_inv, sInf_image]
+  exact ((OrderIso.inv M).map_sSup _).symm
+
+@[to_additive]
+lemma sSup_mul : sSup (s * t) = sSup s * sSup t :=
+  (sSup_image2_eq_sSup_sSup fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ =>
+    (OrderIso.mulLeft _).to_galoisConnection
+
+@[to_additive]
+lemma sInf_mul : sInf (s * t) = sInf s * sInf t :=
+  (sInf_image2_eq_sInf_sInf fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ =>
+    (OrderIso.mulLeft _).symm.to_galoisConnection
+
+@[to_additive]
+lemma sSup_div : sSup (s / t) = sSup s / sInf t := by simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]
+
+@[to_additive]
+lemma sInf_div : sInf (s / t) = sInf s / sSup t := by simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]
+
+end Group
+end CompleteLattice
diff --git a/Mathlib/Algebra/Order/Pointwise.lean b/Mathlib/Algebra/Order/Pointwise.lean
deleted file mode 100644
index 5a6d4539414dd..0000000000000
--- a/Mathlib/Algebra/Order/Pointwise.lean
+++ /dev/null
@@ -1,250 +0,0 @@
-/-
-Copyright (c) 2021 Alex J. Best. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alex J. Best, Yaël Dillies
--/
-import Mathlib.Algebra.Bounds
-import Mathlib.Algebra.Order.Field.Basic -- Porting note: `LinearOrderedField`, etc
-import Mathlib.Algebra.SMulWithZero
-
-/-!
-# Pointwise operations on ordered algebraic objects
-
-This file contains lemmas about the effect of pointwise operations on sets with an order structure.
-
-## TODO
-
-`sSup (s • t) = sSup s • sSup t` and `sInf (s • t) = sInf s • sInf t` hold as well but
-`CovariantClass` is currently not polymorphic enough to state it.
--/
-
-
-open Function Set
-
-open Pointwise
-
-variable {α : Type*}
-
--- Porting note: Swapped the place of `CompleteLattice` and `ConditionallyCompleteLattice`
--- due to simpNF problem between `sSup_xx` `csSup_xx`.
-
-section CompleteLattice
-
-variable [CompleteLattice α]
-
-section One
-
-variable [One α]
-
-@[to_additive (attr := simp)]
-theorem sSup_one : sSup (1 : Set α) = 1 :=
-  sSup_singleton
-
-@[to_additive (attr := simp)]
-theorem sInf_one : sInf (1 : Set α) = 1 :=
-  sInf_singleton
-
-end One
-
-section Group
-
-variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
-  (s t : Set α)
-
-@[to_additive]
-theorem sSup_inv (s : Set α) : sSup s⁻¹ = (sInf s)⁻¹ := by
-  rw [← image_inv, sSup_image]
-  exact ((OrderIso.inv α).map_sInf _).symm
-
-@[to_additive]
-theorem sInf_inv (s : Set α) : sInf s⁻¹ = (sSup s)⁻¹ := by
-  rw [← image_inv, sInf_image]
-  exact ((OrderIso.inv α).map_sSup _).symm
-
-@[to_additive]
-theorem sSup_mul : sSup (s * t) = sSup s * sSup t :=
-  (sSup_image2_eq_sSup_sSup fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ =>
-    (OrderIso.mulLeft _).to_galoisConnection
-
-@[to_additive]
-theorem sInf_mul : sInf (s * t) = sInf s * sInf t :=
-  (sInf_image2_eq_sInf_sInf fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ =>
-    (OrderIso.mulLeft _).symm.to_galoisConnection
-
-@[to_additive]
-theorem sSup_div : sSup (s / t) = sSup s / sInf t := by simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]
-
-@[to_additive]
-theorem sInf_div : sInf (s / t) = sInf s / sSup t := by simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]
-
-end Group
-
-end CompleteLattice
-
-section ConditionallyCompleteLattice
-
-variable [ConditionallyCompleteLattice α]
-
-section One
-
-variable [One α]
-
-@[to_additive (attr := simp)]
-theorem csSup_one : sSup (1 : Set α) = 1 :=
-  csSup_singleton _
-
-@[to_additive (attr := simp)]
-theorem csInf_one : sInf (1 : Set α) = 1 :=
-  csInf_singleton _
-
-end One
-
-section Group
-
-variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
-  {s t : Set α}
-
-@[to_additive]
-theorem csSup_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup s⁻¹ = (sInf s)⁻¹ := by
-  rw [← image_inv]
-  exact ((OrderIso.inv α).map_csInf' hs₀ hs₁).symm
-
-@[to_additive]
-theorem csInf_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sInf s⁻¹ = (sSup s)⁻¹ := by
-  rw [← image_inv]
-  exact ((OrderIso.inv α).map_csSup' hs₀ hs₁).symm
-
-@[to_additive]
-theorem csSup_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
-    sSup (s * t) = sSup s * sSup t :=
-  csSup_image2_eq_csSup_csSup (fun _ => (OrderIso.mulRight _).to_galoisConnection)
-    (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁
-
-@[to_additive]
-theorem csInf_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
-    sInf (s * t) = sInf s * sInf t :=
-  csInf_image2_eq_csInf_csInf (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection)
-    (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁
-
-@[to_additive]
-theorem csSup_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
-    sSup (s / t) = sSup s / sInf t := by
-  rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
-
-@[to_additive]
-theorem csInf_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
-    sInf (s / t) = sInf s / sSup t := by
-  rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
-
-end Group
-
-end ConditionallyCompleteLattice
-
-namespace LinearOrderedField
-
-variable {K : Type*} [LinearOrderedField K] {a b r : K} (hr : 0 < r)
-include hr
-
-open Set
-
-theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Ioo]
-  constructor
-  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
-    constructor
-    · exact (mul_lt_mul_left hr).mpr a_h_left_left
-    · exact (mul_lt_mul_left hr).mpr a_h_left_right
-  · rintro ⟨a_left, a_right⟩
-    use x / r
-    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
-    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
-
-theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Icc]
-  constructor
-  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
-    constructor
-    · exact (mul_le_mul_left hr).mpr a_h_left_left
-    · exact (mul_le_mul_left hr).mpr a_h_left_right
-  · rintro ⟨a_left, a_right⟩
-    use x / r
-    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
-    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
-
-theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Ico]
-  constructor
-  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
-    constructor
-    · exact (mul_le_mul_left hr).mpr a_h_left_left
-    · exact (mul_lt_mul_left hr).mpr a_h_left_right
-  · rintro ⟨a_left, a_right⟩
-    use x / r
-    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
-    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
-
-theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
-  constructor
-  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
-    constructor
-    · exact (mul_lt_mul_left hr).mpr a_h_left_left
-    · exact (mul_le_mul_left hr).mpr a_h_left_right
-  · rintro ⟨a_left, a_right⟩
-    use x / r
-    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
-    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
-
-theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
-  constructor
-  · rintro ⟨a_w, a_h_left, rfl⟩
-    exact (mul_lt_mul_left hr).mpr a_h_left
-  · rintro h
-    use x / r
-    constructor
-    · exact (lt_div_iff' hr).mpr h
-    · exact mul_div_cancel₀ _ (ne_of_gt hr)
-
-theorem smul_Iio : r • Iio a = Iio (r • a) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
-  constructor
-  · rintro ⟨a_w, a_h_left, rfl⟩
-    exact (mul_lt_mul_left hr).mpr a_h_left
-  · rintro h
-    use x / r
-    constructor
-    · exact (div_lt_iff' hr).mpr h
-    · exact mul_div_cancel₀ _ (ne_of_gt hr)
-
-theorem smul_Ici : r • Ici a = Ici (r • a) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
-  constructor
-  · rintro ⟨a_w, a_h_left, rfl⟩
-    exact (mul_le_mul_left hr).mpr a_h_left
-  · rintro h
-    use x / r
-    constructor
-    · exact (le_div_iff₀' hr).mpr h
-    · exact mul_div_cancel₀ _ (ne_of_gt hr)
-
-theorem smul_Iic : r • Iic a = Iic (r • a) := by
-  ext x
-  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
-  constructor
-  · rintro ⟨a_w, a_h_left, rfl⟩
-    exact (mul_le_mul_left hr).mpr a_h_left
-  · rintro h
-    use x / r
-    constructor
-    · exact (div_le_iff₀' hr).mpr h
-    · exact mul_div_cancel₀ _ (ne_of_gt hr)
-
-end LinearOrderedField
diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
index 1abdcf481ef99..b2a03d4aec9d9 100644
--- a/Mathlib/Analysis/Analytic/Basic.lean
+++ b/Mathlib/Analysis/Analytic/Basic.lean
@@ -49,13 +49,13 @@ Additionally, let `f` be a function from `E` to `F`.
 * `HasFPowerSeriesAt f p x`: on some ball of center `x` with positive radius, holds
   `HasFPowerSeriesOnBall f p x r`.
 * `AnalyticAt 𝕜 f x`: there exists a power series `p` such that holds `HasFPowerSeriesAt f p x`.
-* `AnalyticOn 𝕜 f s`: the function `f` is analytic at every point of `s`.
+* `AnalyticOnNhd 𝕜 f s`: the function `f` is analytic at every point of `s`.
 
-We also define versions of `HasFPowerSeriesOnBall`, `AnalyticAt`, and `AnalyticOn` restricted to a
-set, similar to `ContinuousWithinAt`. See `Mathlib.Analysis.Analytic.Within` for basic properties.
+We also define versions of `HasFPowerSeriesOnBall`, `AnalyticAt`, and `AnalyticOnNhd` restricted to
+a set, similar to `ContinuousWithinAt`. See `Mathlib.Analysis.Analytic.Within` for basic properties.
 
 * `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[s ∪ {x}] x`.
-* `AnalyticWithinOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
+* `AnalyticOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
 
 We develop the basic properties of these notions, notably:
 * If a function admits a power series, it is continuous (see
@@ -384,14 +384,17 @@ def AnalyticWithinAt (f : E → F) (s : Set E) (x : E) : Prop :=
 
 /-- Given a function `f : E → F`, we say that `f` is analytic on a set `s` if it is analytic around
 every point of `s`. -/
-def AnalyticOn (f : E → F) (s : Set E) :=
+def AnalyticOnNhd (f : E → F) (s : Set E) :=
   ∀ x, x ∈ s → AnalyticAt 𝕜 f x
 
 /-- `f` is analytic within `s` if it is analytic within `s` at each point of `t`.  Note that
-this is weaker than `AnalyticOn 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`. -/
-def AnalyticWithinOn (f : E → F) (s : Set E) : Prop :=
+this is weaker than `AnalyticOnNhd 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`. -/
+def AnalyticOn (f : E → F) (s : Set E) : Prop :=
   ∀ x ∈ s, AnalyticWithinAt 𝕜 f s x
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn := AnalyticOn
+
 /-!
 ### `HasFPowerSeriesOnBall` and `HasFPowerSeriesWithinOnBall`
 -/
@@ -612,9 +615,12 @@ theorem HasFPowerSeriesAt.coeff_zero (hf : HasFPowerSeriesAt f pf x) (v : Fin 0
     AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x := by
   simp [AnalyticWithinAt, AnalyticAt]
 
-@[simp] lemma analyticWithinOn_univ {f : E → F} :
-    AnalyticWithinOn 𝕜 f univ ↔ AnalyticOn 𝕜 f univ := by
-  simp only [AnalyticWithinOn, analyticWithinAt_univ, AnalyticOn]
+@[simp] lemma analyticOn_univ {f : E → F} :
+    AnalyticOn 𝕜 f univ ↔ AnalyticOnNhd 𝕜 f univ := by
+  simp only [AnalyticOn, analyticWithinAt_univ, AnalyticOnNhd]
+
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_univ := analyticOn_univ
 
 lemma AnalyticWithinAt.mono (hf : AnalyticWithinAt 𝕜 f s x) (h : t ⊆ s) :
     AnalyticWithinAt 𝕜 f t x := by
@@ -625,25 +631,37 @@ lemma AnalyticAt.analyticWithinAt (hf : AnalyticAt 𝕜 f x) : AnalyticWithinAt
   rw [← analyticWithinAt_univ] at hf
   apply hf.mono (subset_univ _)
 
-lemma AnalyticOn.analyticWithinOn (hf : AnalyticOn 𝕜 f s) : AnalyticWithinOn 𝕜 f s :=
+lemma AnalyticOnNhd.analyticOn (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOn 𝕜 f s :=
   fun x hx ↦ (hf x hx).analyticWithinAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.analyticWithinOn := AnalyticOnNhd.analyticOn
+
 lemma AnalyticWithinAt.congr_of_eventuallyEq {f g : E → F} {s : Set E} {x : E}
     (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) :
     AnalyticWithinAt 𝕜 g s x := by
   rcases hf with ⟨p, hp⟩
   exact ⟨p, hp.congr hs hx⟩
 
+lemma AnalyticWithinAt.congr_of_eventuallyEq_insert {f g : E → F} {s : Set E} {x : E}
+    (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[insert x s] x] f) :
+    AnalyticWithinAt 𝕜 g s x := by
+  apply hf.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) hs)
+  apply mem_of_mem_nhdsWithin (mem_insert x s) hs
+
 lemma AnalyticWithinAt.congr {f g : E → F} {s : Set E} {x : E}
     (hf : AnalyticWithinAt 𝕜 f s x) (hs : EqOn g f s) (hx : g x = f x) :
     AnalyticWithinAt 𝕜 g s x :=
   hf.congr_of_eventuallyEq hs.eventuallyEq_nhdsWithin hx
 
-lemma AnalyticWithinOn.congr {f g : E → F} {s : Set E}
-    (hf : AnalyticWithinOn 𝕜 f s) (hs : EqOn g f s) :
-    AnalyticWithinOn 𝕜 g s :=
+lemma AnalyticOn.congr {f g : E → F} {s : Set E}
+    (hf : AnalyticOn 𝕜 f s) (hs : EqOn g f s) :
+    AnalyticOn 𝕜 g s :=
   fun x m ↦ (hf x m).congr hs (hs m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.congr := AnalyticOn.congr
+
 theorem AnalyticAt.congr (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 g x :=
   let ⟨_, hpf⟩ := hf
   (hpf.congr hg).analyticAt
@@ -651,28 +669,41 @@ theorem AnalyticAt.congr (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : An
 theorem analyticAt_congr (h : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 g x :=
   ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
 
-theorem AnalyticOn.mono {s t : Set E} (hf : AnalyticOn 𝕜 f t) (hst : s ⊆ t) : AnalyticOn 𝕜 f s :=
+theorem AnalyticOnNhd.mono {s t : Set E} (hf : AnalyticOnNhd 𝕜 f t) (hst : s ⊆ t) :
+    AnalyticOnNhd 𝕜 f s :=
   fun z hz => hf z (hst hz)
 
-theorem AnalyticOn.congr' (hf : AnalyticOn 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) :
-    AnalyticOn 𝕜 g s :=
+theorem AnalyticOnNhd.congr' (hf : AnalyticOnNhd 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) :
+    AnalyticOnNhd 𝕜 g s :=
   fun z hz => (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz)
 
-theorem analyticOn_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s :=
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.congr' := AnalyticOnNhd.congr'
+
+theorem analyticOnNhd_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s :=
   ⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩
 
-theorem AnalyticOn.congr (hs : IsOpen s) (hf : AnalyticOn 𝕜 f s) (hg : s.EqOn f g) :
-    AnalyticOn 𝕜 g s :=
+@[deprecated (since := "2024-09-26")]
+alias analyticOn_congr' := analyticOnNhd_congr'
+
+theorem AnalyticOnNhd.congr (hs : IsOpen s) (hf : AnalyticOnNhd 𝕜 f s) (hg : s.EqOn f g) :
+    AnalyticOnNhd 𝕜 g s :=
   hf.congr' <| mem_nhdsSet_iff_forall.mpr
     (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)
 
-theorem analyticOn_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOn 𝕜 f s ↔
-    AnalyticOn 𝕜 g s := ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩
+theorem analyticOnNhd_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOnNhd 𝕜 f s ↔
+    AnalyticOnNhd 𝕜 g s := ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩
 
-lemma AnalyticWithinOn.mono {f : E → F} {s t : Set E} (h : AnalyticWithinOn 𝕜 f t)
-    (hs : s ⊆ t) : AnalyticWithinOn 𝕜 f s :=
+@[deprecated (since := "2024-09-26")]
+alias analyticOn_congr := analyticOnNhd_congr
+
+lemma AnalyticOn.mono {f : E → F} {s t : Set E} (h : AnalyticOn 𝕜 f t)
+    (hs : s ⊆ t) : AnalyticOn 𝕜 f s :=
   fun _ m ↦ (h _ (hs m)).mono hs
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.mono := AnalyticOn.mono
+
 /-!
 ### Composition with linear maps
 -/
@@ -691,12 +722,16 @@ theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall (g : F →L[𝕜] G)
 
 /-- If a function `f` is analytic on a set `s` and `g` is linear, then `g ∘ f` is analytic
 on `s`. -/
-theorem ContinuousLinearMap.comp_analyticOn {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOn 𝕜 f s) :
-    AnalyticOn 𝕜 (g ∘ f) s := by
+theorem ContinuousLinearMap.comp_analyticOnNhd
+    {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOnNhd 𝕜 f s) :
+    AnalyticOnNhd 𝕜 (g ∘ f) s := by
   rintro x hx
   rcases h x hx with ⟨p, r, hp⟩
   exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩
 
+@[deprecated (since := "2024-09-26")]
+alias ContinuousLinearMap.comp_analyticOn := ContinuousLinearMap.comp_analyticOnNhd
+
 /-!
 ### Relation between analytic function and the partial sums of its power series
 -/
@@ -1164,17 +1199,24 @@ protected theorem AnalyticAt.continuousAt (hf : AnalyticAt 𝕜 f x) : Continuou
   let ⟨_, hp⟩ := hf
   hp.continuousAt
 
-protected theorem AnalyticOn.continuousOn {s : Set E} (hf : AnalyticOn 𝕜 f s) : ContinuousOn f s :=
+protected theorem AnalyticOnNhd.continuousOn {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) :
+    ContinuousOn f s :=
   fun x hx => (hf x hx).continuousAt.continuousWithinAt
 
-protected lemma AnalyticWithinOn.continuousOn {f : E → F} {s : Set E} (h : AnalyticWithinOn 𝕜 f s) :
+protected lemma AnalyticOn.continuousOn {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) :
     ContinuousOn f s :=
   fun x m ↦ (h x m).continuousWithinAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.continuousOn := AnalyticOn.continuousOn
+
 /-- Analytic everywhere implies continuous -/
-theorem AnalyticOn.continuous {f : E → F} (fa : AnalyticOn 𝕜 f univ) : Continuous f := by
+theorem AnalyticOnNhd.continuous {f : E → F} (fa : AnalyticOnNhd 𝕜 f univ) : Continuous f := by
   rw [continuous_iff_continuousOn_univ]; exact fa.continuousOn
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.continuous := AnalyticOnNhd.continuous
+
 /-- In a complete space, the sum of a converging power series `p` admits `p` as a power series.
 This is not totally obvious as we need to check the convergence of the series. -/
 protected theorem FormalMultilinearSeries.hasFPowerSeriesOnBall [CompleteSpace F]
diff --git a/Mathlib/Analysis/Analytic/CPolynomial.lean b/Mathlib/Analysis/Analytic/CPolynomial.lean
index bda50d02ecbfb..611b6258978a1 100644
--- a/Mathlib/Analysis/Analytic/CPolynomial.lean
+++ b/Mathlib/Analysis/Analytic/CPolynomial.lean
@@ -29,7 +29,7 @@ for `n : ℕ`, and let `f` be a function from `E` to `F`.
 We develop the basic properties of these notions, notably:
 * If a function is continuously polynomial, then it is analytic, see
   `HasFiniteFPowerSeriesOnBall.hasFPowerSeriesOnBall`, `HasFiniteFPowerSeriesAt.hasFPowerSeriesAt`,
-  `CPolynomialAt.analyticAt` and `CPolynomialOn.analyticOn`.
+  `CPolynomialAt.analyticAt` and `CPolynomialOn.analyticOnNhd`.
 * The sum of a finite formal power series with positive radius is well defined on the whole space,
   see `FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite`.
 * If a function admits a finite power series in a ball, then it is continuously polynomial at
@@ -116,9 +116,16 @@ theorem CPolynomialAt.analyticAt (hf : CPolynomialAt 𝕜 f x) : AnalyticAt 𝕜
   let ⟨p, _, hp⟩ := hf
   ⟨p, hp.toHasFPowerSeriesAt⟩
 
-theorem CPolynomialOn.analyticOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s :=
+theorem CPolynomialAt.analyticWithinAt {s : Set E} (hf : CPolynomialAt 𝕜 f x) :
+    AnalyticWithinAt 𝕜 f s x :=
+  hf.analyticAt.analyticWithinAt
+
+theorem CPolynomialOn.analyticOnNhd {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOnNhd 𝕜 f s :=
   fun x hx ↦ (hf x hx).analyticAt
 
+theorem CPolynomialOn.analyticOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s :=
+  hf.analyticOnNhd.analyticOn
+
 theorem HasFiniteFPowerSeriesOnBall.congr (hf : HasFiniteFPowerSeriesOnBall f p x n r)
     (hg : EqOn f g (EMetric.ball x r)) : HasFiniteFPowerSeriesOnBall g p x n r :=
   ⟨hf.1.congr hg, hf.finite⟩
@@ -335,7 +342,7 @@ protected theorem CPolynomialAt.continuousAt (hf : CPolynomialAt 𝕜 f x) : Con
 
 protected theorem CPolynomialOn.continuousOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) :
     ContinuousOn f s :=
-  hf.analyticOn.continuousOn
+  hf.analyticOnNhd.continuousOn
 
 /-- Continuously polynomial everywhere implies continuous -/
 theorem CPolynomialOn.continuous {f : E → F} (fa : CPolynomialOn 𝕜 f univ) : Continuous f := by
@@ -571,10 +578,12 @@ lemma cpolynomialAt  : CPolynomialAt 𝕜 f x :=
 
 lemma cpolyomialOn : CPolynomialOn 𝕜 f s := fun _ _ ↦ f.cpolynomialAt
 
-lemma analyticOn : AnalyticOn 𝕜 f s := f.cpolyomialOn.analyticOn
+lemma analyticOnNhd : AnalyticOnNhd 𝕜 f s := f.cpolyomialOn.analyticOnNhd
+
+lemma analyticOn : AnalyticOn 𝕜 f s := f.analyticOnNhd.analyticOn
 
-lemma analyticWithinOn : AnalyticWithinOn 𝕜 f s :=
-  f.analyticOn.analyticWithinOn
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn := analyticOn
 
 lemma analyticAt : AnalyticAt 𝕜 f x := f.cpolynomialAt.analyticAt
 
@@ -624,12 +633,16 @@ lemma cpolyomialOn_uncurry_of_multilinear :
     CPolynomialOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
   fun _ _ ↦ f.cpolynomialAt_uncurry_of_multilinear
 
-lemma analyticOn_uncurry_of_multilinear : AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
-  f.cpolyomialOn_uncurry_of_multilinear.analyticOn
+lemma analyticOnNhd_uncurry_of_multilinear :
+    AnalyticOnNhd 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
+  f.cpolyomialOn_uncurry_of_multilinear.analyticOnNhd
+
+lemma analyticOn_uncurry_of_multilinear :
+    AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
+  f.analyticOnNhd_uncurry_of_multilinear.analyticOn
 
-lemma analyticWithinOn_uncurry_of_multilinear :
-    AnalyticWithinOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
-  f.analyticOn_uncurry_of_multilinear.analyticWithinOn
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_uncurry_of_multilinear := analyticOn_uncurry_of_multilinear
 
 lemma analyticAt_uncurry_of_multilinear : AnalyticAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
   f.cpolynomialAt_uncurry_of_multilinear.analyticAt
@@ -640,11 +653,11 @@ lemma analyticWithinAt_uncurry_of_multilinear :
 
 lemma continuousOn_uncurry_of_multilinear :
     ContinuousOn (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s :=
-  f.analyticOn_uncurry_of_multilinear.continuousOn
+  f.analyticOnNhd_uncurry_of_multilinear.continuousOn
 
 lemma continuous_uncurry_of_multilinear :
     Continuous (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) :=
-  f.analyticOn_uncurry_of_multilinear.continuous
+  f.analyticOnNhd_uncurry_of_multilinear.continuous
 
 lemma continuousAt_uncurry_of_multilinear :
     ContinuousAt (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
diff --git a/Mathlib/Analysis/Analytic/ChangeOrigin.lean b/Mathlib/Analysis/Analytic/ChangeOrigin.lean
index de0ca613e74d3..ea293a3262884 100644
--- a/Mathlib/Analysis/Analytic/ChangeOrigin.lean
+++ b/Mathlib/Analysis/Analytic/ChangeOrigin.lean
@@ -318,10 +318,13 @@ theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p
   rw [add_sub_cancel] at this
   exact this.analyticAt
 
-theorem HasFPowerSeriesOnBall.analyticOn (hf : HasFPowerSeriesOnBall f p x r) :
-    AnalyticOn 𝕜 f (EMetric.ball x r) :=
+theorem HasFPowerSeriesOnBall.analyticOnNhd (hf : HasFPowerSeriesOnBall f p x r) :
+    AnalyticOnNhd 𝕜 f (EMetric.ball x r) :=
   fun _y hy => hf.analyticAt_of_mem hy
 
+@[deprecated (since := "2024-09-26")]
+alias HasFPowerSeriesOnBall.analyticOn := HasFPowerSeriesOnBall.analyticOnNhd
+
 variable (𝕜 f) in
 /-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such
 that `f` is analytic at `x` is open. -/
@@ -334,13 +337,19 @@ theorem AnalyticAt.eventually_analyticAt (h : AnalyticAt 𝕜 f x) :
     ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y :=
   (isOpen_analyticAt 𝕜 f).mem_nhds h
 
-theorem AnalyticAt.exists_mem_nhds_analyticOn (h : AnalyticAt 𝕜 f x) :
-    ∃ s ∈ 𝓝 x, AnalyticOn 𝕜 f s :=
+theorem AnalyticAt.exists_mem_nhds_analyticOnNhd (h : AnalyticAt 𝕜 f x) :
+    ∃ s ∈ 𝓝 x, AnalyticOnNhd 𝕜 f s :=
   h.eventually_analyticAt.exists_mem
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticAt.exists_mem_nhds_analyticOn := AnalyticAt.exists_mem_nhds_analyticOnNhd
+
 /-- If we're analytic at a point, we're analytic in a nonempty ball -/
-theorem AnalyticAt.exists_ball_analyticOn (h : AnalyticAt 𝕜 f x) :
-    ∃ r : ℝ, 0 < r ∧ AnalyticOn 𝕜 f (Metric.ball x r) :=
+theorem AnalyticAt.exists_ball_analyticOnNhd (h : AnalyticAt 𝕜 f x) :
+    ∃ r : ℝ, 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r) :=
   Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticAt.exists_ball_analyticOn := AnalyticAt.exists_ball_analyticOnNhd
+
 end
diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
index a6ee6bbde78ed..8b33f213f757e 100644
--- a/Mathlib/Analysis/Analytic/Composition.lean
+++ b/Mathlib/Analysis/Analytic/Composition.lean
@@ -830,11 +830,14 @@ theorem AnalyticWithinAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E}
   rw [← hy] at hg
   exact hg.comp hf h
 
-lemma AnalyticWithinOn.comp {f : F → G} {g : E → F} {s : Set F}
-    {t : Set E} (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g t) (h : Set.MapsTo g t s) :
-    AnalyticWithinOn 𝕜 (f ∘ g) t :=
+lemma AnalyticOn.comp {f : F → G} {g : E → F} {s : Set F}
+    {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
+    AnalyticOn 𝕜 (f ∘ g) t :=
   fun x m ↦ (hf _ (h m)).comp (hg x m) h
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.comp := AnalyticOn.comp
+
 /-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
 analytic at `x`. -/
 theorem AnalyticAt.comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x))
@@ -862,19 +865,26 @@ theorem AnalyticAt.comp_analyticWithinAt_of_eq {g : F → G} {f : E → F} {x :
 
 /-- If two functions `g` and `f` are analytic respectively on `s.image f` and `s`, then `g ∘ f` is
 analytic on `s`. -/
-theorem AnalyticOn.comp' {s : Set E} {g : F → G} {f : E → F} (hg : AnalyticOn 𝕜 g (s.image f))
-    (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (g ∘ f) s :=
+theorem AnalyticOnNhd.comp' {s : Set E} {g : F → G} {f : E → F} (hg : AnalyticOnNhd 𝕜 g (s.image f))
+    (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (g ∘ f) s :=
   fun z hz => (hg (f z) (Set.mem_image_of_mem f hz)).comp (hf z hz)
 
-theorem AnalyticOn.comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} (hg : AnalyticOn 𝕜 g t)
-    (hf : AnalyticOn 𝕜 f s) (st : Set.MapsTo f s t) : AnalyticOn 𝕜 (g ∘ f) s :=
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.comp' := AnalyticOnNhd.comp'
+
+theorem AnalyticOnNhd.comp {s : Set E} {t : Set F} {g : F → G} {f : E → F}
+    (hg : AnalyticOnNhd 𝕜 g t) (hf : AnalyticOnNhd 𝕜 f s) (st : Set.MapsTo f s t) :
+    AnalyticOnNhd 𝕜 (g ∘ f) s :=
   comp' (mono hg (Set.mapsTo'.mp st)) hf
 
-lemma AnalyticOn.comp_analyticWithinOn {f : F → G} {g : E → F} {s : Set F}
-    {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g t) (h : Set.MapsTo g t s) :
-    AnalyticWithinOn 𝕜 (f ∘ g) t :=
+lemma AnalyticOnNhd.comp_analyticOn {f : F → G} {g : E → F} {s : Set F}
+    {t : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
+    AnalyticOn 𝕜 (f ∘ g) t :=
   fun x m ↦ (hf _ (h m)).comp_analyticWithinAt (hg x m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.comp_analyticWithinOn := AnalyticOnNhd.comp_analyticOn
+
 /-!
 ### Associativity of the composition of formal multilinear series
 
diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean
index 5b268c5b5d826..7ef5b6a75773b 100644
--- a/Mathlib/Analysis/Analytic/Constructions.lean
+++ b/Mathlib/Analysis/Analytic/Constructions.lean
@@ -48,14 +48,17 @@ theorem hasFPowerSeriesAt_const {c : F} {e : E} :
 theorem analyticAt_const {v : F} {x : E} : AnalyticAt 𝕜 (fun _ => v) x :=
   ⟨constFormalMultilinearSeries 𝕜 E v, hasFPowerSeriesAt_const⟩
 
-theorem analyticOn_const {v : F} {s : Set E} : AnalyticOn 𝕜 (fun _ => v) s :=
+theorem analyticOnNhd_const {v : F} {s : Set E} : AnalyticOnNhd 𝕜 (fun _ => v) s :=
   fun _ _ => analyticAt_const
 
 theorem analyticWithinAt_const {v : F} {s : Set E} {x : E} : AnalyticWithinAt 𝕜 (fun _ => v) s x :=
   analyticAt_const.analyticWithinAt
 
-theorem analyticWithinOn_const {v : F} {s : Set E} : AnalyticWithinOn 𝕜 (fun _ => v) s :=
-  analyticOn_const.analyticWithinOn
+theorem analyticOn_const {v : F} {s : Set E} : AnalyticOn 𝕜 (fun _ => v) s :=
+  analyticOnNhd_const.analyticOn
+
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_const := analyticOn_const
 
 /-!
 ### Addition, negation, subtraction
@@ -159,28 +162,37 @@ theorem AnalyticAt.sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
     AnalyticAt 𝕜 (f - g) x := by
   simpa only [sub_eq_add_neg] using hf.add hg.neg
 
-theorem AnalyticWithinOn.add (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) :
-    AnalyticWithinOn 𝕜 (f + g) s :=
-  fun z hz => (hf z hz).add (hg z hz)
-
 theorem AnalyticOn.add (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
     AnalyticOn 𝕜 (f + g) s :=
   fun z hz => (hf z hz).add (hg z hz)
 
-theorem AnalyticWithinOn.neg (hf : AnalyticWithinOn 𝕜 f s) : AnalyticWithinOn 𝕜 (-f) s :=
-  fun z hz ↦ (hf z hz).neg
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.add := AnalyticOn.add
+
+theorem AnalyticOnNhd.add (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
+    AnalyticOnNhd 𝕜 (f + g) s :=
+  fun z hz => (hf z hz).add (hg z hz)
 
 theorem AnalyticOn.neg (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (-f) s :=
   fun z hz ↦ (hf z hz).neg
 
-theorem AnalyticWithinOn.sub (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) :
-    AnalyticWithinOn 𝕜 (f - g) s :=
-  fun z hz => (hf z hz).sub (hg z hz)
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.neg := AnalyticOn.neg
+
+theorem AnalyticOnNhd.neg (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (-f) s :=
+  fun z hz ↦ (hf z hz).neg
 
 theorem AnalyticOn.sub (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
     AnalyticOn 𝕜 (f - g) s :=
   fun z hz => (hf z hz).sub (hg z hz)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.sub := AnalyticOn.sub
+
+theorem AnalyticOnNhd.sub (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
+    AnalyticOnNhd 𝕜 (f - g) s :=
+  fun z hz => (hf z hz).sub (hg z hz)
+
 end
 
 /-!
@@ -270,17 +282,20 @@ lemma AnalyticAt.prod {e : E} {f : E → F} {g : E → G}
   exact ⟨_, hf.prod hg⟩
 
 /-- The Cartesian product of analytic functions within a set is analytic. -/
-lemma AnalyticWithinOn.prod {f : E → F} {g : E → G} {s : Set E}
-    (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) :
-    AnalyticWithinOn 𝕜 (fun x ↦ (f x, g x)) s :=
-  fun x hx ↦ (hf x hx).prod (hg x hx)
-
-/-- The Cartesian product of analytic functions is analytic. -/
 lemma AnalyticOn.prod {f : E → F} {g : E → G} {s : Set E}
     (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
     AnalyticOn 𝕜 (fun x ↦ (f x, g x)) s :=
   fun x hx ↦ (hf x hx).prod (hg x hx)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.prod := AnalyticOn.prod
+
+/-- The Cartesian product of analytic functions is analytic. -/
+lemma AnalyticOnNhd.prod {f : E → F} {g : E → G} {s : Set E}
+    (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
+    AnalyticOnNhd 𝕜 (fun x ↦ (f x, g x)) s :=
+  fun x hx ↦ (hf x hx).prod (hg x hx)
+
 /-- `AnalyticAt.comp` for functions on product spaces -/
 theorem AnalyticAt.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {x : E}
     (ha : AnalyticAt 𝕜 h (f x, g x)) (fa : AnalyticAt 𝕜 f x)
@@ -304,20 +319,23 @@ theorem AnalyticAt.comp₂_analyticWithinAt
     AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) s x :=
   AnalyticAt.comp_analyticWithinAt ha (fa.prod ga)
 
-/-- `AnalyticOn.comp` for functions on product spaces -/
-theorem AnalyticOn.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E}
-    (ha : AnalyticOn 𝕜 h s) (fa : AnalyticOn 𝕜 f t) (ga : AnalyticOn 𝕜 g t)
-    (m : ∀ x, x ∈ t → (f x, g x) ∈ s) : AnalyticOn 𝕜 (fun x ↦ h (f x, g x)) t :=
+/-- `AnalyticOnNhd.comp` for functions on product spaces -/
+theorem AnalyticOnNhd.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E}
+    (ha : AnalyticOnNhd 𝕜 h s) (fa : AnalyticOnNhd 𝕜 f t) (ga : AnalyticOnNhd 𝕜 g t)
+    (m : ∀ x, x ∈ t → (f x, g x) ∈ s) : AnalyticOnNhd 𝕜 (fun x ↦ h (f x, g x)) t :=
   fun _ xt ↦ (ha _ (m _ xt)).comp₂ (fa _ xt) (ga _ xt)
 
-/-- `AnalyticWithinOn.comp` for functions on product spaces -/
-theorem AnalyticWithinOn.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)}
+/-- `AnalyticOn.comp` for functions on product spaces -/
+theorem AnalyticOn.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)}
     {t : Set E}
-    (ha : AnalyticWithinOn 𝕜 h s) (fa : AnalyticWithinOn 𝕜 f t)
-    (ga : AnalyticWithinOn 𝕜 g t) (m : Set.MapsTo (fun y ↦ (f y, g y)) t s) :
-    AnalyticWithinOn 𝕜 (fun x ↦ h (f x, g x)) t :=
+    (ha : AnalyticOn 𝕜 h s) (fa : AnalyticOn 𝕜 f t)
+    (ga : AnalyticOn 𝕜 g t) (m : Set.MapsTo (fun y ↦ (f y, g y)) t s) :
+    AnalyticOn 𝕜 (fun x ↦ h (f x, g x)) t :=
   fun x hx ↦ (ha _ (m hx)).comp₂ (fa x hx) (ga x hx) m
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.comp₂ := AnalyticOn.comp₂
+
 /-- Analytic functions on products are analytic in the first coordinate -/
 theorem AnalyticAt.curry_left {f : E × F → G} {p : E × F} (fa : AnalyticAt 𝕜 f p) :
     AnalyticAt 𝕜 (fun x ↦ f (x, p.2)) p.1 :=
@@ -341,27 +359,41 @@ theorem AnalyticWithinAt.curry_right
   AnalyticWithinAt.comp₂ fa  analyticWithinAt_const analyticWithinAt_id (fun _ hx ↦ hx)
 
 /-- Analytic functions on products are analytic in the first coordinate -/
-theorem AnalyticOn.curry_left {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOn 𝕜 f s) :
-    AnalyticOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} :=
+theorem AnalyticOnNhd.curry_left {f : E × F → G} {s : Set (E × F)} {y : F}
+    (fa : AnalyticOnNhd 𝕜 f s) :
+    AnalyticOnNhd 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} :=
   fun x m ↦ (fa (x, y) m).curry_left
-alias AnalyticOn.along_fst := AnalyticOn.curry_left
+alias AnalyticOnNhd.along_fst := AnalyticOnNhd.curry_left
+
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.along_fst := AnalyticOnNhd.curry_left
 
-theorem AnalyticWithinOn.curry_left
-    {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticWithinOn 𝕜 f s) :
-    AnalyticWithinOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} :=
+theorem AnalyticOn.curry_left
+    {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOn 𝕜 f s) :
+    AnalyticOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} :=
   fun x m ↦ (fa (x, y) m).curry_left
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.curry_left := AnalyticOn.curry_left
+
 /-- Analytic functions on products are analytic in the second coordinate -/
-theorem AnalyticOn.curry_right {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOn 𝕜 f s) :
-    AnalyticOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} :=
+theorem AnalyticOnNhd.curry_right {f : E × F → G} {x : E} {s : Set (E × F)}
+    (fa : AnalyticOnNhd 𝕜 f s) :
+    AnalyticOnNhd 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} :=
   fun y m ↦ (fa (x, y) m).curry_right
-alias AnalyticOn.along_snd := AnalyticOn.curry_right
+alias AnalyticOnNhd.along_snd := AnalyticOnNhd.curry_right
 
-theorem AnalyticWithinOn.curry_right
-    {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticWithinOn 𝕜 f s) :
-    AnalyticWithinOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} :=
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.along_snd := AnalyticOnNhd.curry_right
+
+theorem AnalyticOn.curry_right
+    {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOn 𝕜 f s) :
+    AnalyticOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} :=
   fun y m ↦ (fa (x, y) m).curry_right
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.curry_right := AnalyticOn.curry_right
+
 /-!
 ### Analyticity in Pi spaces
 
@@ -491,20 +523,26 @@ lemma analyticAt_pi_iff :
   simp_rw [← analyticWithinAt_univ]
   exact analyticWithinAt_pi_iff
 
-lemma AnalyticWithinOn.pi (hf : ∀ i, AnalyticWithinOn 𝕜 (f i) s) :
-    AnalyticWithinOn 𝕜 (fun x ↦ (f · x)) s :=
+lemma AnalyticOn.pi (hf : ∀ i, AnalyticOn 𝕜 (f i) s) :
+    AnalyticOn 𝕜 (fun x ↦ (f · x)) s :=
   fun x hx ↦ AnalyticWithinAt.pi (fun i ↦ hf i x hx)
 
-lemma analyticWithinOn_pi_iff :
-    AnalyticWithinOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticWithinOn 𝕜 (f i) s :=
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.pi := AnalyticOn.pi
+
+lemma analyticOn_pi_iff :
+    AnalyticOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOn 𝕜 (f i) s :=
   ⟨fun h i x hx ↦ analyticWithinAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩
 
-lemma AnalyticOn.pi (hf : ∀ i, AnalyticOn 𝕜 (f i) s) :
-    AnalyticOn 𝕜 (fun x ↦ (f · x)) s :=
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_pi_iff := analyticOn_pi_iff
+
+lemma AnalyticOnNhd.pi (hf : ∀ i, AnalyticOnNhd 𝕜 (f i) s) :
+    AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s :=
   fun x hx ↦ AnalyticAt.pi (fun i ↦ hf i x hx)
 
-lemma analyticOn_pi_iff :
-    AnalyticOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOn 𝕜 (f i) s :=
+lemma analyticOnNhd_pi_iff :
+    AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOnNhd 𝕜 (f i) s :=
   ⟨fun h i x hx ↦ analyticAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩
 
 end
@@ -540,16 +578,19 @@ lemma AnalyticAt.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E 
   (analyticAt_smul _).comp₂ hf hg
 
 /-- Scalar multiplication of one analytic function by another. -/
-lemma AnalyticWithinOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F]
+lemma AnalyticOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F]
     {f : E → 𝕝} {g : E → F} {s : Set E}
-    (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) :
-    AnalyticWithinOn 𝕜 (fun x ↦ f x • g x) s :=
+    (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
+    AnalyticOn 𝕜 (fun x ↦ f x • g x) s :=
   fun _ m ↦ (hf _ m).smul (hg _ m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.smul := AnalyticOn.smul
+
 /-- Scalar multiplication of one analytic function by another. -/
-lemma AnalyticOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E}
-    (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
-    AnalyticOn 𝕜 (fun x ↦ f x • g x) s :=
+lemma AnalyticOnNhd.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E}
+    (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
+    AnalyticOnNhd 𝕜 (fun x ↦ f x • g x) s :=
   fun _ m ↦ (hf _ m).smul (hg _ m)
 
 /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
@@ -564,14 +605,18 @@ lemma AnalyticAt.mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : An
   (analyticAt_mul _).comp₂ hf hg
 
 /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
-lemma AnalyticWithinOn.mul {f g : E → A} {s : Set E}
-    (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) :
-    AnalyticWithinOn 𝕜 (fun x ↦ f x * g x) s :=
+lemma AnalyticOn.mul {f g : E → A} {s : Set E}
+    (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
+    AnalyticOn 𝕜 (fun x ↦ f x * g x) s :=
   fun _ m ↦ (hf _ m).mul (hg _ m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.mul := AnalyticOn.mul
+
 /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
-lemma AnalyticOn.mul {f g : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
-    AnalyticOn 𝕜 (fun x ↦ f x * g x) s :=
+lemma AnalyticOnNhd.mul {f g : E → A} {s : Set E}
+    (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
+    AnalyticOnNhd 𝕜 (fun x ↦ f x * g x) s :=
   fun _ m ↦ (hf _ m).mul (hg _ m)
 
 /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
@@ -592,13 +637,16 @@ lemma AnalyticAt.pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ)
   exact hf.pow n
 
 /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-lemma AnalyticWithinOn.pow {f : E → A} {s : Set E} (hf : AnalyticWithinOn 𝕜 f s) (n : ℕ) :
-    AnalyticWithinOn 𝕜 (fun x ↦ f x ^ n) s :=
+lemma AnalyticOn.pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) :
+    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s :=
   fun _ m ↦ (hf _ m).pow n
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.pow := AnalyticOn.pow
+
 /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
-lemma AnalyticOn.pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) :
-    AnalyticOn 𝕜 (fun x ↦ f x ^ n) s :=
+lemma AnalyticOnNhd.pow {f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
+    AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s :=
   fun _ m ↦ (hf _ m).pow n
 
 section Geometric
@@ -726,9 +774,12 @@ lemma analyticAt_inv {z : 𝕝} (hz : z ≠ 0) : AnalyticAt 𝕜 Inv.inv z := by
   exact Ring.inverse_eq_inv'.symm
 
 /-- `x⁻¹` is analytic away from zero -/
-lemma analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := by
+lemma analyticOnNhd_inv : AnalyticOnNhd 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := by
   intro z m; exact analyticAt_inv m
 
+lemma analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} :=
+  analyticOnNhd_inv.analyticOn
+
 /-- `(f x)⁻¹` is analytic away from `f x = 0` -/
 theorem AnalyticWithinAt.inv {f : E → 𝕝} {x : E} {s : Set E}
     (fa : AnalyticWithinAt 𝕜 f s x) (f0 : f x ≠ 0) :
@@ -741,14 +792,18 @@ theorem AnalyticAt.inv {f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 :
   (analyticAt_inv f0).comp fa
 
 /-- `(f x)⁻¹` is analytic away from `f x = 0` -/
-theorem AnalyticWithinOn.inv {f : E → 𝕝} {s : Set E}
-    (fa : AnalyticWithinOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
-    AnalyticWithinOn 𝕜 (fun x ↦ (f x)⁻¹) s :=
+theorem AnalyticOn.inv {f : E → 𝕝} {s : Set E}
+    (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
+    AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s :=
   fun x m ↦ (fa x m).inv (f0 x m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.inv := AnalyticOn.inv
+
 /-- `(f x)⁻¹` is analytic away from `f x = 0` -/
-theorem AnalyticOn.inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
-    AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s :=
+theorem AnalyticOnNhd.inv {f : E → 𝕝} {s : Set E}
+    (fa : AnalyticOnNhd 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
+    AnalyticOnNhd 𝕜 (fun x ↦ (f x)⁻¹) s :=
   fun x m ↦ (fa x m).inv (f0 x m)
 
 /-- `f x / g x` is analytic away from `g x = 0` -/
@@ -763,18 +818,21 @@ theorem AnalyticAt.div {f g : E → 𝕝} {x : E}
     AnalyticAt 𝕜 (fun x ↦ f x / g x) x := by
   simp_rw [div_eq_mul_inv]; exact fa.mul (ga.inv g0)
 
-/-- `f x / g x` is analytic away from `g x = 0` -/
-theorem AnalyticWithinOn.div {f g : E → 𝕝} {s : Set E}
-    (fa : AnalyticWithinOn 𝕜 f s) (ga : AnalyticWithinOn 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
-    AnalyticWithinOn 𝕜 (fun x ↦ f x / g x) s := fun x m ↦
-  (fa x m).div (ga x m) (g0 x m)
-
 /-- `f x / g x` is analytic away from `g x = 0` -/
 theorem AnalyticOn.div {f g : E → 𝕝} {s : Set E}
     (fa : AnalyticOn 𝕜 f s) (ga : AnalyticOn 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
     AnalyticOn 𝕜 (fun x ↦ f x / g x) s := fun x m ↦
   (fa x m).div (ga x m) (g0 x m)
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.div := AnalyticOn.div
+
+/-- `f x / g x` is analytic away from `g x = 0` -/
+theorem AnalyticOnNhd.div {f g : E → 𝕝} {s : Set E}
+    (fa : AnalyticOnNhd 𝕜 f s) (ga : AnalyticOnNhd 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
+    AnalyticOnNhd 𝕜 (fun x ↦ f x / g x) s := fun x m ↦
+  (fa x m).div (ga x m) (g0 x m)
+
 /-!
 ### Finite sums and products of analytic functions
 -/
@@ -797,16 +855,19 @@ theorem Finset.analyticAt_sum {f : α → E → F} {c : E}
   simp_rw [← analyticWithinAt_univ] at h ⊢
   exact N.analyticWithinAt_sum h
 
-/-- Finite sums of analytic functions are analytic -/
-theorem Finset.analyticWithinOn_sum {f : α → E → F} {s : Set E}
-    (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinOn 𝕜 (f n) s) :
-    AnalyticWithinOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s :=
-  fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs)
-
 /-- Finite sums of analytic functions are analytic -/
 theorem Finset.analyticOn_sum {f : α → E → F} {s : Set E}
     (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
     AnalyticOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s :=
+  fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs)
+
+@[deprecated (since := "2024-09-26")]
+alias Finset.analyticWithinOn_sum := Finset.analyticOn_sum
+
+/-- Finite sums of analytic functions are analytic -/
+theorem Finset.analyticOnNhd_sum {f : α → E → F} {s : Set E}
+    (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
+    AnalyticOnNhd 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s :=
   fun z zs ↦ N.analyticAt_sum (fun n m ↦ h n m z zs)
 
 /-- Finite products of analytic functions are analytic -/
@@ -827,14 +888,17 @@ theorem Finset.analyticAt_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 
   simp_rw [← analyticWithinAt_univ] at h ⊢
   exact N.analyticWithinAt_prod h
 
-/-- Finite products of analytic functions are analytic -/
-theorem Finset.analyticWithinOn_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
-    {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinOn 𝕜 (f n) s) :
-    AnalyticWithinOn 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s :=
-  fun z zs ↦ N.analyticWithinAt_prod (fun n m ↦ h n m z zs)
-
 /-- Finite products of analytic functions are analytic -/
 theorem Finset.analyticOn_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
     {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) :
     AnalyticOn 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s :=
+  fun z zs ↦ N.analyticWithinAt_prod (fun n m ↦ h n m z zs)
+
+@[deprecated (since := "2024-09-26")]
+alias Finset.analyticWithinOn_prod := Finset.analyticOn_prod
+
+/-- Finite products of analytic functions are analytic -/
+theorem Finset.analyticOnNhd_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
+    {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
+    AnalyticOnNhd 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s :=
   fun z zs ↦ N.analyticAt_prod (fun n m ↦ h n m z zs)
diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 00ccc0c8bbeea..1f37145b0dc28 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -20,7 +20,7 @@ useful in this setup.
 * `AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` is the main statement that if a function is
   analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not
   vanish in a punctured neighborhood of `z₀`.
-* `AnalyticOn.eqOn_of_preconnected_of_frequently_eq` is the identity theorem for analytic
+* `AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq` is the identity theorem for analytic
   functions: if a function `f` is analytic on a connected set `U` and is zero on a set with an
   accumulation point in `U` then `f` is identically `0` on `U`.
 -/
@@ -221,7 +221,7 @@ lemma order_eq_nat_iff (hf : AnalyticAt 𝕜 f z₀) (n : ℕ) : hf.order = ↑n
 
 end AnalyticAt
 
-namespace AnalyticOn
+namespace AnalyticOnNhd
 
 variable {U : Set 𝕜}
 
@@ -229,13 +229,13 @@ variable {U : Set 𝕜}
 analytic on a connected set `U` and vanishes in arbitrary neighborhoods of a point `z₀ ∈ U`, then
 it is identically zero in `U`.
 For higher-dimensional versions requiring that the function vanishes in a neighborhood of `z₀`,
-see `AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero`. -/
-theorem eqOn_zero_of_preconnected_of_frequently_eq_zero (hf : AnalyticOn 𝕜 f U)
+see `AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero`. -/
+theorem eqOn_zero_of_preconnected_of_frequently_eq_zero (hf : AnalyticOnNhd 𝕜 f U)
     (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfw : ∃ᶠ z in 𝓝[≠] z₀, f z = 0) : EqOn f 0 U :=
   hf.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀
     ((hf z₀ h₀).frequently_zero_iff_eventually_zero.1 hfw)
 
-theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hU : IsPreconnected U)
+theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U)
     (h₀ : z₀ ∈ U) (hfz₀ : z₀ ∈ closure ({z | f z = 0} \ {z₀})) : EqOn f 0 U :=
   hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀
     (mem_closure_ne_iff_frequently_within.mp hfz₀)
@@ -244,15 +244,15 @@ theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hU
 analytic on a connected set `U` and coincide at points which accumulate to a point `z₀ ∈ U`, then
 they coincide globally in `U`.
 For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
-see `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`. -/
-theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U)
+see `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`. -/
+theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
     (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U := by
   have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 :=
     hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
   simpa [sub_eq_zero] using fun z hz =>
     (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz
 
-theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U)
+theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
     (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : z₀ ∈ closure ({z | f z = g z} \ {z₀})) :
     EqOn f g U :=
   hf.eqOn_of_preconnected_of_frequently_eq hg hU h₀ (mem_closure_ne_iff_frequently_within.mp hfg)
@@ -261,10 +261,13 @@ theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hg : Ana
 field `𝕜` are analytic everywhere and coincide at points which accumulate to a point `z₀`, then
 they coincide globally.
 For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
-see `AnalyticOn.eq_of_eventuallyEq`. -/
-theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOn 𝕜 f univ) (hg : AnalyticOn 𝕜 g univ)
-    (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : f = g :=
+see `AnalyticOnNhd.eq_of_eventuallyEq`. -/
+theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOnNhd 𝕜 f univ)
+    (hg : AnalyticOnNhd 𝕜 g univ) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : f = g :=
   funext fun x =>
     eqOn_of_preconnected_of_frequently_eq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x)
 
-end AnalyticOn
+@[deprecated (since := "2024-09-26")]
+alias _root_.AnalyticOn.eq_of_frequently_eq := eq_of_frequently_eq
+
+end AnalyticOnNhd
diff --git a/Mathlib/Analysis/Analytic/Linear.lean b/Mathlib/Analysis/Analytic/Linear.lean
index ee4fa10f65092..e527cda45057c 100644
--- a/Mathlib/Analysis/Analytic/Linear.lean
+++ b/Mathlib/Analysis/Analytic/Linear.lean
@@ -44,15 +44,18 @@ protected theorem hasFPowerSeriesAt (f : E →L[𝕜] F) (x : E) :
 protected theorem analyticAt (f : E →L[𝕜] F) (x : E) : AnalyticAt 𝕜 f x :=
   (f.hasFPowerSeriesAt x).analyticAt
 
-protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s :=
+protected theorem analyticOnNhd (f : E →L[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 f s :=
   fun x _ ↦ f.analyticAt x
 
 protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x :=
   (f.analyticAt x).analyticWithinAt
 
-protected theorem analyticWithinOn (f : E →L[𝕜] F) (s : Set E) : AnalyticWithinOn 𝕜 f s :=
+protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s :=
   fun x _ ↦ f.analyticWithinAt _ x
 
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn := ContinuousLinearMap.analyticOn
+
 /-- Reinterpret a bilinear map `f : E →L[𝕜] F →L[𝕜] G` as a multilinear map
 `(E × F) [×2]→L[𝕜] G`. This multilinear map is the second term in the formal
 multilinear series expansion of `uncurry f`. It is given by
@@ -121,9 +124,17 @@ protected theorem analyticAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E 
     AnalyticAt 𝕜 (fun x : E × F => f x.1 x.2) x :=
   (f.hasFPowerSeriesAt_bilinear x).analyticAt
 
+protected theorem analyticWithinAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) (x : E × F) :
+    AnalyticWithinAt 𝕜 (fun x : E × F => f x.1 x.2) s x :=
+  (f.analyticAt_bilinear x).analyticWithinAt
+
+protected theorem analyticOnNhd_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) :
+    AnalyticOnNhd 𝕜 (fun x : E × F => f x.1 x.2) s :=
+  fun x _ ↦ f.analyticAt_bilinear x
+
 protected theorem analyticOn_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) :
     AnalyticOn 𝕜 (fun x : E × F => f x.1 x.2) s :=
-  fun x _ ↦ f.analyticAt_bilinear x
+  (f.analyticOnNhd_bilinear s).analyticOn
 
 end ContinuousLinearMap
 
@@ -136,12 +147,15 @@ lemma analyticWithinAt_id : AnalyticWithinAt 𝕜 (id : E → E) s z :=
   analyticAt_id.analyticWithinAt
 
 /-- `id` is entire -/
-theorem analyticOn_id : AnalyticOn 𝕜 (fun x : E ↦ x) s :=
+theorem analyticOnNhd_id : AnalyticOnNhd 𝕜 (fun x : E ↦ x) s :=
   fun _ _ ↦ analyticAt_id
 
-theorem analyticWithinOn_id : AnalyticWithinOn 𝕜 (fun x : E ↦ x) s :=
+theorem analyticOn_id : AnalyticOn 𝕜 (fun x : E ↦ x) s :=
   fun _ _ ↦ analyticWithinAt_id
 
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_id := analyticOn_id
+
 /-- `fst` is analytic -/
 theorem analyticAt_fst  : AnalyticAt 𝕜 (fun p : E × F ↦ p.fst) p :=
   (ContinuousLinearMap.fst 𝕜 E F).analyticAt p
@@ -157,19 +171,25 @@ theorem analyticWithinAt_snd : AnalyticWithinAt 𝕜 (fun p : E × F ↦ p.snd)
   analyticAt_snd.analyticWithinAt
 
 /-- `fst` is entire -/
-theorem analyticOn_fst : AnalyticOn 𝕜 (fun p : E × F ↦ p.fst) t :=
+theorem analyticOnNhd_fst : AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.fst) t :=
   fun _ _ ↦ analyticAt_fst
 
-theorem analyticWithinOn_fst : AnalyticWithinOn 𝕜 (fun p : E × F ↦ p.fst) t :=
+theorem analyticOn_fst : AnalyticOn 𝕜 (fun p : E × F ↦ p.fst) t :=
   fun _ _ ↦ analyticWithinAt_fst
 
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_fst := analyticOn_fst
+
 /-- `snd` is entire -/
-theorem analyticOn_snd : AnalyticOn 𝕜 (fun p : E × F ↦ p.snd) t :=
+theorem analyticOnNhd_snd : AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.snd) t :=
   fun _ _ ↦ analyticAt_snd
 
-theorem analyticWithinOn_snd : AnalyticWithinOn 𝕜 (fun p : E × F ↦ p.snd) t :=
+theorem analyticOn_snd : AnalyticOn 𝕜 (fun p : E × F ↦ p.snd) t :=
   fun _ _ ↦ analyticWithinAt_snd
 
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_snd := analyticOn_snd
+
 namespace ContinuousLinearEquiv
 
 variable (f : E ≃L[𝕜] F) (s : Set E) (x : E)
@@ -177,15 +197,18 @@ variable (f : E ≃L[𝕜] F) (s : Set E) (x : E)
 protected theorem analyticAt : AnalyticAt 𝕜 f x :=
   ((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt
 
-protected theorem analyticOn : AnalyticOn 𝕜 f s :=
+protected theorem analyticOnNhd : AnalyticOnNhd 𝕜 f s :=
   fun x _ ↦ f.analyticAt x
 
 protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x :=
   (f.analyticAt x).analyticWithinAt
 
-protected theorem analyticWithinOn (f : E →L[𝕜] F) (s : Set E) : AnalyticWithinOn 𝕜 f s :=
+protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s :=
   fun x _ ↦ f.analyticWithinAt _ x
 
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn := ContinuousLinearEquiv.analyticOn
+
 end ContinuousLinearEquiv
 
 namespace LinearIsometryEquiv
@@ -195,13 +218,16 @@ variable (f : E ≃ₗᵢ[𝕜] F) (s : Set E) (x : E)
 protected theorem analyticAt : AnalyticAt 𝕜 f x :=
   ((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt
 
-protected theorem analyticOn : AnalyticOn 𝕜 f s :=
+protected theorem analyticOnNhd : AnalyticOnNhd 𝕜 f s :=
   fun x _ ↦ f.analyticAt x
 
 protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x :=
   (f.analyticAt x).analyticWithinAt
 
-protected theorem analyticWithinOn (f : E →L[𝕜] F) (s : Set E) : AnalyticWithinOn 𝕜 f s :=
+protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s :=
   fun x _ ↦ f.analyticWithinAt _ x
 
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn := LinearIsometryEquiv.analyticOn
+
 end LinearIsometryEquiv
diff --git a/Mathlib/Analysis/Analytic/Meromorphic.lean b/Mathlib/Analysis/Analytic/Meromorphic.lean
index 1a29b6bb5cff9..4c3349d87d078 100644
--- a/Mathlib/Analysis/Analytic/Meromorphic.lean
+++ b/Mathlib/Analysis/Analytic/Meromorphic.lean
@@ -237,10 +237,12 @@ end MeromorphicAt
 /-- Meromorphy of a function on a set. -/
 def MeromorphicOn (f : 𝕜 → E) (U : Set 𝕜) : Prop := ∀ x ∈ U, MeromorphicAt f x
 
-lemma AnalyticOn.meromorphicOn {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOn 𝕜 f U) :
+lemma AnalyticOnNhd.meromorphicOn {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) :
     MeromorphicOn f U :=
   fun x hx ↦ (hf x hx).meromorphicAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.meromorphicOn := AnalyticOnNhd.meromorphicOn
 
 namespace MeromorphicOn
 
diff --git a/Mathlib/Analysis/Analytic/Polynomial.lean b/Mathlib/Analysis/Analytic/Polynomial.lean
index 74ea377c682ac..77e62fd5b542b 100644
--- a/Mathlib/Analysis/Analytic/Polynomial.lean
+++ b/Mathlib/Analysis/Analytic/Polynomial.lean
@@ -23,17 +23,28 @@ open Polynomial
 
 variable [NormedRing B] [NormedAlgebra 𝕜 B] [Algebra A B] {f : E → B}
 
-theorem AnalyticAt.aeval_polynomial (hf : AnalyticAt 𝕜 f z) (p : A[X]) :
-    AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z := by
+theorem AnalyticWithinAt.aeval_polynomial (hf : AnalyticWithinAt 𝕜 f s z) (p : A[X]) :
+    AnalyticWithinAt 𝕜 (fun x ↦ aeval (f x) p) s z := by
   refine p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
-  · simp_rw [aeval_C]; apply analyticAt_const
+  · simp_rw [aeval_C]; apply analyticWithinAt_const
   · simp_rw [aeval_add]; exact hp.add hq
   · convert hp.mul hf
     simp_rw [pow_succ, aeval_mul, ← mul_assoc, aeval_X]
 
+theorem AnalyticAt.aeval_polynomial (hf : AnalyticAt 𝕜 f z) (p : A[X]) :
+    AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z := by
+  rw [← analyticWithinAt_univ] at hf ⊢
+  exact hf.aeval_polynomial p
+
+theorem AnalyticOnNhd.aeval_polynomial (hf : AnalyticOnNhd 𝕜 f s) (p : A[X]) :
+    AnalyticOnNhd 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ (hf x hx).aeval_polynomial p
+
 theorem AnalyticOn.aeval_polynomial (hf : AnalyticOn 𝕜 f s) (p : A[X]) :
     AnalyticOn 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ (hf x hx).aeval_polynomial p
 
+theorem AnalyticOnNhd.eval_polynomial {A} [NormedCommRing A] [NormedAlgebra 𝕜 A] (p : A[X]) :
+    AnalyticOnNhd 𝕜 (eval · p) Set.univ := analyticOnNhd_id.aeval_polynomial p
+
 theorem AnalyticOn.eval_polynomial {A} [NormedCommRing A] [NormedAlgebra 𝕜 A] (p : A[X]) :
     AnalyticOn 𝕜 (eval · p) Set.univ := analyticOn_id.aeval_polynomial p
 
@@ -51,27 +62,47 @@ theorem AnalyticAt.aeval_mvPolynomial (hf : ∀ i, AnalyticAt 𝕜 (f · i) z) (
   · simp_rw [map_add]; exact hp.add hq
   · simp_rw [map_mul, aeval_X]; exact hp.mul (hf i)
 
-theorem AnalyticOn.aeval_mvPolynomial (hf : ∀ i, AnalyticOn 𝕜 (f · i) s) (p : MvPolynomial σ A) :
-    AnalyticOn 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ .aeval_mvPolynomial (hf · x hx) p
+theorem AnalyticOnNhd.aeval_mvPolynomial
+    (hf : ∀ i, AnalyticOnNhd 𝕜 (f · i) s) (p : MvPolynomial σ A) :
+    AnalyticOnNhd 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ .aeval_mvPolynomial (hf · x hx) p
+
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.aeval_mvPolynomial := AnalyticOnNhd.aeval_mvPolynomial
 
-theorem AnalyticOn.eval_continuousLinearMap (f : E →L[𝕜] σ → B) (p : MvPolynomial σ B) :
-    AnalyticOn 𝕜 (fun x ↦ eval (f x) p) Set.univ :=
+theorem AnalyticOnNhd.eval_continuousLinearMap (f : E →L[𝕜] σ → B) (p : MvPolynomial σ B) :
+    AnalyticOnNhd 𝕜 (fun x ↦ eval (f x) p) Set.univ :=
   fun x _ ↦ .aeval_mvPolynomial (fun i ↦ ((ContinuousLinearMap.proj i).comp f).analyticAt x) p
 
-theorem AnalyticOn.eval_continuousLinearMap' (f : σ → E →L[𝕜] B) (p : MvPolynomial σ B) :
-    AnalyticOn 𝕜 (fun x ↦ eval (f · x) p) Set.univ :=
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.eval_continuousLinearMap := AnalyticOnNhd.eval_continuousLinearMap
+
+theorem AnalyticOnNhd.eval_continuousLinearMap' (f : σ → E →L[𝕜] B) (p : MvPolynomial σ B) :
+    AnalyticOnNhd 𝕜 (fun x ↦ eval (f · x) p) Set.univ :=
   fun x _ ↦ .aeval_mvPolynomial (fun i ↦ (f i).analyticAt x) p
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.eval_continuousLinearMap' := AnalyticOnNhd.eval_continuousLinearMap'
+
 variable [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E]
 
-theorem AnalyticOn.eval_linearMap (f : E →ₗ[𝕜] σ → B) (p : MvPolynomial σ B) :
-    AnalyticOn 𝕜 (fun x ↦ eval (f x) p) Set.univ :=
-  AnalyticOn.eval_continuousLinearMap { f with cont := f.continuous_of_finiteDimensional } p
+theorem AnalyticOnNhd.eval_linearMap (f : E →ₗ[𝕜] σ → B) (p : MvPolynomial σ B) :
+    AnalyticOnNhd 𝕜 (fun x ↦ eval (f x) p) Set.univ :=
+  AnalyticOnNhd.eval_continuousLinearMap { f with cont := f.continuous_of_finiteDimensional } p
+
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.eval_linearMap := AnalyticOnNhd.eval_linearMap
+
+theorem AnalyticOnNhd.eval_linearMap' (f : σ → E →ₗ[𝕜] B) (p : MvPolynomial σ B) :
+    AnalyticOnNhd 𝕜 (fun x ↦ eval (f · x) p) Set.univ := AnalyticOnNhd.eval_linearMap (.pi f) p
+
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.eval_linearMap' := AnalyticOnNhd.eval_linearMap'
 
-theorem AnalyticOn.eval_linearMap' (f : σ → E →ₗ[𝕜] B) (p : MvPolynomial σ B) :
-    AnalyticOn 𝕜 (fun x ↦ eval (f · x) p) Set.univ := AnalyticOn.eval_linearMap (.pi f) p
+theorem AnalyticOnNhd.eval_mvPolynomial [Fintype σ] (p : MvPolynomial σ 𝕜) :
+    AnalyticOnNhd 𝕜 (eval · p) Set.univ :=
+  AnalyticOnNhd.eval_linearMap (.id (R := 𝕜) (M := σ → 𝕜)) p
 
-theorem AnalyticOn.eval_mvPolynomial [Fintype σ] (p : MvPolynomial σ 𝕜) :
-    AnalyticOn 𝕜 (eval · p) Set.univ := AnalyticOn.eval_linearMap (.id (R := 𝕜) (M := σ → 𝕜)) p
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.eval_mvPolynomial := AnalyticOnNhd.eval_mvPolynomial
 
 end MvPolynomial
diff --git a/Mathlib/Analysis/Analytic/Uniqueness.lean b/Mathlib/Analysis/Analytic/Uniqueness.lean
index 088cf07ea867d..6c836c8afcab6 100644
--- a/Mathlib/Analysis/Analytic/Uniqueness.lean
+++ b/Mathlib/Analysis/Analytic/Uniqueness.lean
@@ -13,7 +13,7 @@ import Mathlib.Analysis.Analytic.ChangeOrigin
 # Uniqueness principle for analytic functions
 
 We show that two analytic functions which coincide around a point coincide on whole connected sets,
-in `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`.
+in `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`.
 -/
 
 
@@ -154,13 +154,14 @@ theorem HasFPowerSeriesOnBall.r_eq_top_of_exists {f : 𝕜 → E} {r : ℝ≥0
 
 end Uniqueness
 
-namespace AnalyticOn
+namespace AnalyticOnNhd
 
 /-- If an analytic function vanishes around a point, then it is uniformly zero along
 a connected set. Superseded by `eqOn_zero_of_preconnected_of_locally_zero` which does not assume
 completeness of the target space. -/
 theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux [CompleteSpace F] {f : E → F} {U : Set E}
-    (hf : AnalyticOn 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) :
+    (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U)
+    {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) :
     EqOn f 0 U := by
   /- Let `u` be the set of points around which `f` vanishes. It is clearly open. We have to show
     that its limit points in `U` still belong to it, from which the inclusion `U ⊆ u` will follow
@@ -204,11 +205,12 @@ neighborhood of a point `z₀`, then it is uniformly zero along a connected set.
 version assuming only that the function vanishes at some points arbitrarily close to `z₀`, see
 `eqOn_zero_of_preconnected_of_frequently_eq_zero`. -/
 theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero {f : E → F} {U : Set E}
-    (hf : AnalyticOn 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) :
+    (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U)
+    {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) :
     EqOn f 0 U := by
   let F' := UniformSpace.Completion F
   set e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
-  have : AnalyticOn 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx)
+  have : AnalyticOnNhd 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx)
   have A : EqOn (e ∘ f) 0 U := by
     apply eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux this hU h₀
     filter_upwards [hfz₀] with x hx
@@ -221,8 +223,8 @@ theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero {f : E → F} {U : Set E}
 neighborhood of a point `z₀`, then they coincide globally along a connected set.
 For a one-dimensional version assuming only that the functions coincide at some points
 arbitrarily close to `z₀`, see `eqOn_of_preconnected_of_frequently_eq`. -/
-theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : AnalyticOn 𝕜 f U)
-    (hg : AnalyticOn 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[𝓝 z₀] g) :
+theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U)
+    (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[𝓝 z₀] g) :
     EqOn f g U := by
   have hfg' : f - g =ᶠ[𝓝 z₀] 0 := hfg.mono fun z h => by simp [h]
   simpa [sub_eq_zero] using fun z hz =>
@@ -232,9 +234,9 @@ theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : A
 coincide in a neighborhood of a point `z₀`, then they coincide everywhere.
 For a one-dimensional version assuming only that the functions coincide at some points
 arbitrarily close to `z₀`, see `eq_of_frequently_eq`. -/
-theorem eq_of_eventuallyEq {f g : E → F} [PreconnectedSpace E] (hf : AnalyticOn 𝕜 f univ)
-    (hg : AnalyticOn 𝕜 g univ) {z₀ : E} (hfg : f =ᶠ[𝓝 z₀] g) : f = g :=
+theorem eq_of_eventuallyEq {f g : E → F} [PreconnectedSpace E] (hf : AnalyticOnNhd 𝕜 f univ)
+    (hg : AnalyticOnNhd 𝕜 g univ) {z₀ : E} (hfg : f =ᶠ[𝓝 z₀] g) : f = g :=
   funext fun x =>
     eqOn_of_preconnected_of_eventuallyEq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x)
 
-end AnalyticOn
+end AnalyticOnNhd
diff --git a/Mathlib/Analysis/Analytic/Within.lean b/Mathlib/Analysis/Analytic/Within.lean
index 7b1093877a659..7703eb9524ef0 100644
--- a/Mathlib/Analysis/Analytic/Within.lean
+++ b/Mathlib/Analysis/Analytic/Within.lean
@@ -11,7 +11,7 @@ import Mathlib.Analysis.Analytic.Constructions
 From `Mathlib.Analysis.Analytic.Basic`, we have the definitions
 
 1. `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[insert x s] x`.
-2. `AnalyticWithinOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
+2. `AnalyticOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`.
 
 This means there exists an extension of `f` which is analytic and agrees with `f` on `s ∪ {x}`, but
 `f` is allowed to be arbitrary elsewhere.
@@ -56,10 +56,10 @@ lemma analyticWithinAt_of_singleton_mem {f : E → F} {s : Set E} {x : E} (h : {
       apply (hasFPowerSeriesOnBall_const (e := 0)).hasSum
       simp only [Metric.emetric_ball_top, mem_univ] }⟩
 
-/-- If `f` is `AnalyticWithinOn` near each point in a set, it is `AnalyticWithinOn` the set -/
-lemma analyticWithinOn_of_locally_analyticWithinOn {f : E → F} {s : Set E}
-    (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticWithinOn 𝕜 f (s ∩ u)) :
-    AnalyticWithinOn 𝕜 f s := by
+/-- If `f` is `AnalyticOn` near each point in a set, it is `AnalyticOn` the set -/
+lemma analyticOn_of_locally_analyticOn {f : E → F} {s : Set E}
+    (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)) :
+    AnalyticOn 𝕜 f s := by
   intro x m
   rcases h x m with ⟨u, ou, xu, fu⟩
   rcases Metric.mem_nhds_iff.mp (ou.mem_nhds xu) with ⟨r, r0, ru⟩
@@ -79,10 +79,13 @@ lemma analyticWithinOn_of_locally_analyticWithinOn {f : E → F} {s : Set E}
             simp only [Metric.mem_ball, dist_self_add_left, yr]
         · simp only [EMetric.mem_ball, yr] }⟩
 
-/-- On open sets, `AnalyticOn` and `AnalyticWithinOn` coincide -/
-lemma IsOpen.analyticWithinOn_iff_analyticOn {f : E → F} {s : Set E} (hs : IsOpen s) :
-    AnalyticWithinOn 𝕜 f s ↔ AnalyticOn 𝕜 f s := by
-  refine ⟨?_, AnalyticOn.analyticWithinOn⟩
+@[deprecated (since := "2024-09-26")]
+alias analyticWithinOn_of_locally_analyticWithinOn := analyticOn_of_locally_analyticOn
+
+/-- On open sets, `AnalyticOnNhd` and `AnalyticOn` coincide -/
+lemma IsOpen.analyticOn_iff_analyticOnNhd {f : E → F} {s : Set E} (hs : IsOpen s) :
+    AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s := by
+  refine ⟨?_, AnalyticOnNhd.analyticOn⟩
   intro hf x m
   rcases Metric.mem_nhds_iff.mp (hs.mem_nhds m) with ⟨r, r0, rs⟩
   rcases hf x m with ⟨p, t, fp⟩
@@ -97,13 +100,16 @@ lemma IsOpen.analyticWithinOn_iff_analyticOn {f : E → F} {s : Set E} (hs : IsO
       apply rs
       simp only [Metric.mem_ball, dist_self_add_left, ym.1] }⟩
 
+@[deprecated (since := "2024-09-26")]
+alias IsOpen.analyticWithinOn_iff_analyticOn := IsOpen.analyticOn_iff_analyticOnNhd
+
 
 /-!
 ### Equivalence to analyticity of a local extension
 
 We show that `HasFPowerSeriesWithinOnBall`, `HasFPowerSeriesWithinAt`, and `AnalyticWithinAt` are
 equivalent to the existence of a local extension with full analyticity.  We do not yet show a
-result for `AnalyticWithinOn`, as this requires a bit more work to show that local extensions can
+result for `AnalyticOn`, as this requires a bit more work to show that local extensions can
 be stitched together.
 -/
 
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
index e5c7cea5ca34e..2895a56f474d3 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@@ -428,9 +428,9 @@ open scoped ContinuousMapZero
 variable {F R S A B : Type*} {p : A → Prop} {q : B → Prop}
   [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R]
   [ContinuousStar R] [CommRing S] [Algebra R S]
-  [Ring A] [StarRing A] [TopologicalSpace A] [Module R A]
+  [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A]
   [IsScalarTower R A A] [SMulCommClass R A A]
-  [Ring B] [StarRing B] [TopologicalSpace B] [Module R B]
+  [NonUnitalRing B] [StarRing B] [TopologicalSpace B] [Module R B]
   [IsScalarTower R B B] [SMulCommClass R B B]
   [Module S A] [Module S B] [IsScalarTower R S A] [IsScalarTower R S B]
   [NonUnitalContinuousFunctionalCalculus R p] [NonUnitalContinuousFunctionalCalculus R q]
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index ef38ec6312a71..896125484853c 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -68,9 +68,13 @@ theorem HasFPowerSeriesOnBall.differentiableOn [CompleteSpace F]
     (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (EMetric.ball x r) := fun _ hy =>
   (h.analyticAt_of_mem hy).differentiableWithinAt
 
-theorem AnalyticOn.differentiableOn (h : AnalyticOn 𝕜 f s) : DifferentiableOn 𝕜 f s := fun y hy =>
+theorem AnalyticOnNhd.differentiableOn (h : AnalyticOnNhd 𝕜 f s) :
+    DifferentiableOn 𝕜 f s := fun y hy =>
   (h y hy).differentiableWithinAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.differentiableOn := AnalyticOnNhd.differentiableOn
+
 theorem HasFPowerSeriesOnBall.hasFDerivAt [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r)
     {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) :
     HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1)) (x + y) :=
@@ -95,32 +99,38 @@ theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F] (h : HasFPowerSeriesOnBal
   simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz
 
 /-- If a function is analytic on a set `s`, so is its Fréchet derivative. -/
-theorem AnalyticOn.fderiv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) :
-    AnalyticOn 𝕜 (fderiv 𝕜 f) s := by
+theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
+    AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s := by
   intro y hy
   rcases h y hy with ⟨p, r, hp⟩
   exact hp.fderiv.analyticAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.fderiv := AnalyticOnNhd.fderiv
+
 /-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. -/
-theorem AnalyticOn.iteratedFDeriv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) (n : ℕ) :
-    AnalyticOn 𝕜 (iteratedFDeriv 𝕜 n f) s := by
+theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
+    AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s := by
   induction n with
   | zero =>
     rw [iteratedFDeriv_zero_eq_comp]
-    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_analyticOn h
+    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_analyticOnNhd h
   | succ n IH =>
     rw [iteratedFDeriv_succ_eq_comp_left]
     -- Porting note: for reasons that I do not understand at all, `?g` cannot be inlined.
-    convert ContinuousLinearMap.comp_analyticOn ?g IH.fderiv
+    convert ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv
     case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
     simp
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.iteratedFDeriv := AnalyticOnNhd.iteratedFDeriv
+
 /-- An analytic function is infinitely differentiable. -/
-theorem AnalyticOn.contDiffOn [CompleteSpace F] (h : AnalyticOn 𝕜 f s) {n : ℕ∞} :
+theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) {n : ℕ∞} :
     ContDiffOn 𝕜 n f s :=
   let t := { x | AnalyticAt 𝕜 f x }
   suffices ContDiffOn 𝕜 n f t from this.mono h
-  have H : AnalyticOn 𝕜 f t := fun _x hx ↦ hx
+  have H : AnalyticOnNhd 𝕜 f t := fun _x hx ↦ hx
   have t_open : IsOpen t := isOpen_analyticAt 𝕜 f
   contDiffOn_of_continuousOn_differentiableOn
     (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr
@@ -130,7 +140,7 @@ theorem AnalyticOn.contDiffOn [CompleteSpace F] (h : AnalyticOn 𝕜 f s) {n : 
 
 theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : ℕ∞} :
     ContDiffAt 𝕜 n f x := by
-  obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOn
+  obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOnNhd
   exact hf.contDiffOn.contDiffAt hs
 
 lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
@@ -138,10 +148,13 @@ lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set
   rcases h.exists_analyticAt with ⟨g, fx, fg, hg⟩
   exact hg.contDiffAt.contDiffWithinAt.congr (fg.mono (subset_insert _ _)) fx
 
-lemma AnalyticWithinOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
-    (h : AnalyticWithinOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s :=
+lemma AnalyticOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E}
+    (h : AnalyticOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s :=
   fun x m ↦ (h x m).contDiffWithinAt
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticWithinOn.contDiffOn := AnalyticOn.contDiffOn
+
 end fderiv
 
 section deriv
@@ -162,16 +175,23 @@ protected theorem HasFPowerSeriesAt.deriv (h : HasFPowerSeriesAt f p x) :
   h.hasDerivAt.deriv
 
 /-- If a function is analytic on a set `s`, so is its derivative. -/
-theorem AnalyticOn.deriv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (deriv f) s :=
-  (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOn h.fderiv
+theorem AnalyticOnNhd.deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
+    AnalyticOnNhd 𝕜 (deriv f) s :=
+  (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd h.fderiv
+
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.deriv := AnalyticOnNhd.deriv
 
 /-- If a function is analytic on a set `s`, so are its successive derivatives. -/
-theorem AnalyticOn.iterated_deriv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) (n : ℕ) :
-    AnalyticOn 𝕜 (_root_.deriv^[n] f) s := by
+theorem AnalyticOnNhd.iterated_deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
+    AnalyticOnNhd 𝕜 (_root_.deriv^[n] f) s := by
   induction n with
   | zero => exact h
   | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
 
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.iterated_deriv := AnalyticOnNhd.iterated_deriv
+
 end deriv
 section fderiv
 
@@ -258,7 +278,7 @@ theorem CPolynomialOn.contDiffOn (h : CPolynomialOn 𝕜 f s) {n : ℕ∞} :
   contDiffOn_of_continuousOn_differentiableOn
     (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr
       fun  _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
-    (fun m _ ↦ (H.iteratedFDeriv m).analyticOn.differentiableOn.congr
+    (fun m _ ↦ (H.iteratedFDeriv m).analyticOnNhd.differentiableOn.congr
       fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx)
 
 theorem CPolynomialAt.contDiffAt (h : CPolynomialAt 𝕜 f x) {n : ℕ∞} :
diff --git a/Mathlib/Analysis/Complex/CauchyIntegral.lean b/Mathlib/Analysis/Complex/CauchyIntegral.lean
index acb07715c395f..ebc991f8801e8 100644
--- a/Mathlib/Analysis/Complex/CauchyIntegral.lean
+++ b/Mathlib/Analysis/Complex/CauchyIntegral.lean
@@ -568,14 +568,18 @@ protected theorem _root_.DifferentiableOn.analyticAt {s : Set ℂ} {f : ℂ →
   lift R to ℝ≥0 using hR0.le
   exact ((hd.mono hRs).hasFPowerSeriesOnBall hR0).analyticAt
 
+theorem _root_.DifferentiableOn.analyticOnNhd {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s)
+    (hs : IsOpen s) : AnalyticOnNhd ℂ f s := fun _z hz => hd.analyticAt (hs.mem_nhds hz)
+
 theorem _root_.DifferentiableOn.analyticOn {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s)
-    (hs : IsOpen s) : AnalyticOn ℂ f s := fun _z hz => hd.analyticAt (hs.mem_nhds hz)
+    (hs : IsOpen s) : AnalyticOn ℂ f s :=
+  (hd.analyticOnNhd hs).analyticOn
 
 /-- If `f : ℂ → E` is complex differentiable on some open set `s`, then it is continuously
 differentiable on `s`. -/
 protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E} {n : ℕ}
     (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : ContDiffOn ℂ n f s :=
-  (hd.analyticOn hs).contDiffOn
+  (hd.analyticOnNhd hs).contDiffOn
 
 /-- A complex differentiable function `f : ℂ → E` is analytic at every point. -/
 protected theorem _root_.Differentiable.analyticAt {f : ℂ → E} (hf : Differentiable ℂ f) (z : ℂ) :
@@ -594,16 +598,27 @@ protected theorem _root_.Differentiable.hasFPowerSeriesOnBall {f : ℂ → E} (h
   (h.differentiableOn.hasFPowerSeriesOnBall hR).r_eq_top_of_exists fun _r hr =>
     ⟨_, h.differentiableOn.hasFPowerSeriesOnBall hr⟩
 
+/-- On an open set, `f : ℂ → E` is analytic iff it is differentiable -/
+theorem analyticOnNhd_iff_differentiableOn {f : ℂ → E} {s : Set ℂ} (o : IsOpen s) :
+    AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s :=
+  ⟨AnalyticOnNhd.differentiableOn, fun d _ zs ↦ d.analyticAt (o.mem_nhds zs)⟩
+
 /-- On an open set, `f : ℂ → E` is analytic iff it is differentiable -/
 theorem analyticOn_iff_differentiableOn {f : ℂ → E} {s : Set ℂ} (o : IsOpen s) :
-    AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s :=
-  ⟨AnalyticOn.differentiableOn, fun d _ zs ↦ d.analyticAt (o.mem_nhds zs)⟩
+    AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s := by
+  rw [o.analyticOn_iff_analyticOnNhd]
+  exact analyticOnNhd_iff_differentiableOn o
 
 /-- `f : ℂ → E` is entire iff it's differentiable -/
+theorem analyticOnNhd_univ_iff_differentiable {f : ℂ → E} :
+    AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f := by
+  simp only [← differentiableOn_univ]
+  exact analyticOnNhd_iff_differentiableOn isOpen_univ
+
 theorem analyticOn_univ_iff_differentiable {f : ℂ → E} :
     AnalyticOn ℂ f univ ↔ Differentiable ℂ f := by
-  simp only [← differentiableOn_univ]
-  exact analyticOn_iff_differentiableOn isOpen_univ
+  rw [analyticOn_univ]
+  exact analyticOnNhd_univ_iff_differentiable
 
 /-- `f : ℂ → E` is analytic at `z` iff it's differentiable near `z` -/
 theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} :
@@ -614,8 +629,8 @@ theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} :
     apply AnalyticAt.differentiableAt
   · intro d
     rcases _root_.eventually_nhds_iff.mp d with ⟨s, d, o, m⟩
-    have h : AnalyticOn ℂ f s := by
-      refine DifferentiableOn.analyticOn ?_ o
+    have h : AnalyticOnNhd ℂ f s := by
+      refine DifferentiableOn.analyticOnNhd ?_ o
       intro z m
       exact (d z m).differentiableWithinAt
     exact h _ m
diff --git a/Mathlib/Analysis/Complex/OpenMapping.lean b/Mathlib/Analysis/Complex/OpenMapping.lean
index 9ce4d01945319..c37d82d1058c9 100644
--- a/Mathlib/Analysis/Complex/OpenMapping.lean
+++ b/Mathlib/Analysis/Complex/OpenMapping.lean
@@ -27,7 +27,7 @@ That second step is implemented in `DiffContOnCl.ball_subset_image_closedBall`.
 
 * `AnalyticAt.eventually_constant_or_nhds_le_map_nhds` is the local version of the open mapping
   theorem around a point;
-* `AnalyticOn.is_constant_or_isOpen` is the open mapping theorem on a connected open set.
+* `AnalyticOnNhd.is_constant_or_isOpen` is the open mapping theorem on a connected open set.
 -/
 
 
@@ -51,7 +51,7 @@ theorem DiffContOnCl.ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball
   have h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r) := h.sub_const v
   have h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r) :=
     continuous_norm.comp_continuousOn (closure_ball z₀ hr.ne.symm ▸ h1.continuousOn)
-  have h3 : AnalyticOn ℂ f (ball z₀ r) := h.differentiableOn.analyticOn isOpen_ball
+  have h3 : AnalyticOnNhd ℂ f (ball z₀ r) := h.differentiableOn.analyticOnNhd isOpen_ball
   have h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖ := fun z hz => by
     linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball.mp hv,
       norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]
@@ -64,7 +64,7 @@ theorem DiffContOnCl.ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball
   have h7 : ∀ᶠ w in 𝓝 z, f w = f z := by filter_upwards [key] with h; field_simp
   replace h7 : ∃ᶠ w in 𝓝[≠] z, f w = f z := (h7.filter_mono nhdsWithin_le_nhds).frequently
   have h8 : IsPreconnected (ball z₀ r) := (convex_ball z₀ r).isPreconnected
-  have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOn_const h8 hz1 h7
+  have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOnNhd_const h8 hz1 h7
   have h10 : f z = f z₀ := (h9 (mem_ball_self hr)).symm
   exact not_eventually.mpr hz₀ (mem_of_superset (ball_mem_nhds z₀ hr) (h10 ▸ h9))
 
@@ -83,7 +83,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux (hf : AnalyticAt
   have h1 := (hf.eventually_eq_or_eventually_ne analyticAt_const).resolve_left h
   have h2 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).eventually_mem hf
   obtain ⟨ρ, hρ, h3, h4⟩ :
-    ∃ ρ > 0, AnalyticOn ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ := by
+    ∃ ρ > 0, AnalyticOnNhd ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ := by
     simpa only [setOf_and, subset_inter_iff] using
       nhds_basis_closedBall.mem_iff.mp (h2.and (eventually_nhdsWithin_iff.mp h1))
   replace h3 : DiffContOnCl ℂ f (ball z₀ ρ) :=
@@ -118,7 +118,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal
   let ray : E → ℂ → E := fun z t => z₀ + t • z
   let gray : E → ℂ → ℂ := fun z => g ∘ ray z
   obtain ⟨r, hr, hgr⟩ := isOpen_iff.mp (isOpen_analyticAt ℂ g) z₀ hg
-  have h1 : ∀ z ∈ sphere (0 : E) 1, AnalyticOn ℂ (gray z) (ball 0 r) := by
+  have h1 : ∀ z ∈ sphere (0 : E) 1, AnalyticOnNhd ℂ (gray z) (ball 0 r) := by
     refine fun z hz t ht => AnalyticAt.comp ?_ ?_
     · exact hgr (by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using ht)
     · exact analyticAt_const.add
@@ -134,7 +134,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal
       have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected
       have e2 : w ∈ sphere (0 : E) 1 := by simp [w, norm_smul, inv_mul_cancel₀ h']
       specialize h1 w e2
-      apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOn_const e1 (mem_ball_self hr)
+      apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr)
       simpa [ray, gray] using h w e2
     have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using mem_ball.mp hz
     replace h4 : ↑‖z - z₀‖ ∈ ball (0 : ℂ) r := by
@@ -156,13 +156,16 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal
 /-- The *open mapping theorem* for holomorphic functions, global version: if a function `g : E → ℂ`
 is analytic on a connected set `U`, then either it is constant on `U`, or it is open on `U` (in the
 sense that it maps any open set contained in `U` to an open set in `ℂ`). -/
-theorem AnalyticOn.is_constant_or_isOpen (hg : AnalyticOn ℂ g U) (hU : IsPreconnected U) :
+theorem AnalyticOnNhd.is_constant_or_isOpen (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) :
     (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s) := by
   by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
   · obtain ⟨z₀, hz₀, h⟩ := h
-    exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOn_const hU hz₀ h⟩
+    exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const hU hz₀ h⟩
   · push_neg at h
     refine Or.inr fun s hs1 hs2 => isOpen_iff_mem_nhds.mpr ?_
     rintro z ⟨w, hw1, rfl⟩
     exact (hg w (hs1 hw1)).eventually_constant_or_nhds_le_map_nhds.resolve_left (h w (hs1 hw1))
         (image_mem_map (hs2.mem_nhds hw1))
+
+@[deprecated (since := "2024-09-26")]
+alias AnalyticOn.is_constant_or_isOpen := AnalyticOnNhd.is_constant_or_isOpen
diff --git a/Mathlib/Analysis/Normed/Module/Completion.lean b/Mathlib/Analysis/Normed/Module/Completion.lean
index bb143e6302377..c4377b5b2a68a 100644
--- a/Mathlib/Analysis/Normed/Module/Completion.lean
+++ b/Mathlib/Analysis/Normed/Module/Completion.lean
@@ -27,20 +27,16 @@ namespace UniformSpace
 
 namespace Completion
 
-variable (𝕜 E : Type*) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable (𝕜 E : Type*)
 
-instance (priority := 100) NormedSpace.to_uniformContinuousConstSMul :
-    UniformContinuousConstSMul 𝕜 E :=
-  ⟨fun c => (lipschitzWith_smul c).uniformContinuous⟩
+instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
+    NormedSpace 𝕜 (Completion E) where
+  norm_smul_le := norm_smul_le
 
-instance : NormedSpace 𝕜 (Completion E) :=
-  { Completion.instModule with
-    norm_smul_le := fun c x =>
-      induction_on x
-        (isClosed_le (continuous_const_smul _).norm (continuous_const.mul continuous_norm)) fun y =>
-        by simp only [← coe_smul, norm_coe, norm_smul, le_rfl] }
+section Module
 
 variable {𝕜 E}
+variable [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E]
 
 /-- Embedding of a normed space to its completion as a linear isometry. -/
 def toComplₗᵢ : E →ₗᵢ[𝕜] Completion E :=
@@ -66,46 +62,38 @@ theorem norm_toComplL {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [NormedAdd
     [NormedSpace 𝕜 E] [Nontrivial E] : ‖(toComplL : E →L[𝕜] Completion E)‖ = 1 :=
   (toComplₗᵢ : E →ₗᵢ[𝕜] Completion E).norm_toContinuousLinearMap
 
+end Module
+
 section Algebra
 
-variable (𝕜) (A : Type*)
-
-instance [SeminormedRing A] : NormedRing (Completion A) :=
-  { Completion.ring,
-    Completion.instMetricSpace with
-    dist_eq := fun x y => by
-      refine Completion.induction_on₂ x y ?_ ?_ <;> clear x y
-      · refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_
-        exact Continuous.comp Completion.continuous_extension continuous_sub
-      · intro x y
-        rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]
-    norm_mul := fun x y => by
-      refine Completion.induction_on₂ x y ?_ ?_ <;> clear x y
-      · exact
-          isClosed_le (Continuous.comp continuous_norm continuous_mul)
-            (Continuous.comp _root_.continuous_mul
-              (Continuous.prod_map continuous_norm continuous_norm))
-      · intro x y
-        simp only [← coe_mul, norm_coe]
-        exact norm_mul_le x y }
-
-instance [SeminormedCommRing A] [NormedAlgebra 𝕜 A] [UniformContinuousConstSMul 𝕜 A] :
-    NormedAlgebra 𝕜 (Completion A) :=
-  { Completion.algebra A 𝕜 with
-    norm_smul_le := fun r x => by
-      refine Completion.induction_on x ?_ ?_ <;> clear x
-      · exact
-          isClosed_le (Continuous.comp continuous_norm (continuous_const_smul r))
-            (Continuous.comp (continuous_mul_left _) continuous_norm)
-      · intro x
-        simp only [← coe_smul, norm_coe]
-        exact norm_smul_le r x }
+variable (A : Type*)
+
+instance [SeminormedRing A] : NormedRing (Completion A) where
+  __ : NormedAddCommGroup (Completion A) := inferInstance
+  __ : Ring (Completion A) := inferInstance
+  norm_mul x y := by
+    induction x, y using induction_on₂ with
+    | hp =>
+      exact
+        isClosed_le (Continuous.comp continuous_norm continuous_mul)
+          (Continuous.comp _root_.continuous_mul
+            (Continuous.prod_map continuous_norm continuous_norm))
+    | ih x y =>
+      simp only [← coe_mul, norm_coe]
+      exact norm_mul_le x y
+
+instance [SeminormedCommRing A] : NormedCommRing (Completion A) where
+  __ : CommRing (Completion A) := inferInstance
+  __ : NormedRing (Completion A) := inferInstance
+
+instance [NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] :
+    NormedAlgebra 𝕜 (Completion A) where
+  norm_smul_le := norm_smul_le
 
 instance [NormedField A] [CompletableTopField A] :
     NormedField (UniformSpace.Completion A) where
-  dist_eq x y := by
-    refine induction_on₂ x y ?_ (by simp [← coe_sub, dist_eq_norm])
-    exact isClosed_eq (uniformContinuous_extension₂ _).continuous (by fun_prop)
+  __ : NormedCommRing (Completion A) := inferInstance
+  __ : Field (Completion A) := inferInstance
   norm_mul' x y := induction_on₂ x y (isClosed_eq (by fun_prop) (by fun_prop)) (by simp [← coe_mul])
 
 end Algebra
diff --git a/Mathlib/Analysis/Normed/MulAction.lean b/Mathlib/Analysis/Normed/MulAction.lean
index 1c42cc236b1e9..2c9c706fdb6c1 100644
--- a/Mathlib/Analysis/Normed/MulAction.lean
+++ b/Mathlib/Analysis/Normed/MulAction.lean
@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.Topology.MetricSpace.Algebra
+import Mathlib.Topology.Algebra.UniformMulAction
 
 /-!
 # Lemmas for `BoundedSMul` over normed additive groups
diff --git a/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean b/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
index 1ddd022c490b2..299585582989c 100644
--- a/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
+++ b/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
@@ -211,8 +211,7 @@ theorem injectiveSeminorm_le_projectiveSeminorm :
     existsi PUnit, inferInstance, inferInstance
     ext x
     simp only [Seminorm.zero_apply, Seminorm.comp_apply, coe_normSeminorm]
-    have heq : toDualContinuousMultilinearMap PUnit x = 0 := by ext _
-    rw [heq, norm_zero]
+    rw [Subsingleton.elim (toDualContinuousMultilinearMap PUnit x) 0, norm_zero]
   · intro p hp
     simp only [Set.mem_setOf_eq] at hp
     obtain ⟨G, _, _, h⟩ := hp
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
index 18ea3db3671d5..dfa5088bf9e96 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
@@ -21,21 +21,30 @@ variable {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E]
 variable {f g : E → ℂ} {z : ℂ} {x : E} {s : Set E}
 
 /-- `exp` is entire -/
-theorem analyticOn_cexp : AnalyticOn ℂ exp univ := by
-  rw [analyticOn_univ_iff_differentiable]; exact differentiable_exp
+theorem analyticOnNhd_cexp : AnalyticOnNhd ℂ exp univ := by
+  rw [analyticOnNhd_univ_iff_differentiable]; exact differentiable_exp
+
+theorem analyticOn_cexp : AnalyticOn ℂ exp univ := analyticOnNhd_cexp.analyticOn
 
 /-- `exp` is analytic at any point -/
 theorem analyticAt_cexp : AnalyticAt ℂ exp z :=
-  analyticOn_cexp z (mem_univ _)
+  analyticOnNhd_cexp z (mem_univ _)
 
 /-- `exp ∘ f` is analytic -/
 theorem AnalyticAt.cexp (fa : AnalyticAt ℂ f x) : AnalyticAt ℂ (fun z ↦ exp (f z)) x :=
   analyticAt_cexp.comp fa
 
+theorem AnalyticWithinAt.cexp (fa : AnalyticWithinAt ℂ f s x) :
+    AnalyticWithinAt ℂ (fun z ↦ exp (f z)) s x :=
+  analyticAt_cexp.comp_analyticWithinAt fa
+
 /-- `exp ∘ f` is analytic -/
-theorem AnalyticOn.cexp (fs : AnalyticOn ℂ f s) : AnalyticOn ℂ (fun z ↦ exp (f z)) s :=
+theorem AnalyticOnNhd.cexp (fs : AnalyticOnNhd ℂ f s) : AnalyticOnNhd ℂ (fun z ↦ exp (f z)) s :=
   fun z n ↦ analyticAt_cexp.comp (fs z n)
 
+theorem AnalyticOn.cexp (fs : AnalyticOn ℂ f s) : AnalyticOn ℂ (fun z ↦ exp (f z)) s :=
+  analyticOnNhd_cexp.comp_analyticOn fs (mapsTo_univ _ _)
+
 /-- `log` is analytic away from nonpositive reals -/
 theorem analyticAt_clog (m : z ∈ slitPlane) : AnalyticAt ℂ log z := by
   rw [analyticAt_iff_eventually_differentiableAt]
@@ -48,21 +57,40 @@ theorem AnalyticAt.clog (fa : AnalyticAt ℂ f x) (m : f x ∈ slitPlane) :
     AnalyticAt ℂ (fun z ↦ log (f z)) x :=
   (analyticAt_clog m).comp fa
 
+theorem AnalyticWithinAt.clog (fa : AnalyticWithinAt ℂ f s x) (m : f x ∈ slitPlane) :
+    AnalyticWithinAt ℂ (fun z ↦ log (f z)) s x :=
+  (analyticAt_clog m).comp_analyticWithinAt fa
+
 /-- `log` is analytic away from nonpositive reals -/
+theorem AnalyticOnNhd.clog (fs : AnalyticOnNhd ℂ f s) (m : ∀ z ∈ s, f z ∈ slitPlane) :
+    AnalyticOnNhd ℂ (fun z ↦ log (f z)) s :=
+  fun z n ↦ (analyticAt_clog (m z n)).comp (fs z n)
+
 theorem AnalyticOn.clog (fs : AnalyticOn ℂ f s) (m : ∀ z ∈ s, f z ∈ slitPlane) :
     AnalyticOn ℂ (fun z ↦ log (f z)) s :=
-  fun z n ↦ (analyticAt_clog (m z n)).comp (fs z n)
+  fun z n ↦ (analyticAt_clog (m z n)).analyticWithinAt.comp (fs z n) m
 
 /-- `f z ^ g z` is analytic if `f z` is not a nonpositive real -/
-theorem AnalyticAt.cpow (fa : AnalyticAt ℂ f x) (ga : AnalyticAt ℂ g x)
-    (m : f x ∈ slitPlane) : AnalyticAt ℂ (fun z ↦ f z ^ g z) x := by
-  have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝 x] fun z ↦ exp (log (f z) * g z) := by
-    filter_upwards [(fa.continuousAt.eventually_ne (slitPlane_ne_zero m))]
+theorem AnalyticWithinAt.cpow (fa : AnalyticWithinAt ℂ f s x) (ga : AnalyticWithinAt ℂ g s x)
+    (m : f x ∈ slitPlane) : AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) s x := by
+  have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ exp (log (f z) * g z) := by
+    filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]
     intro z fz
     simp only [fz, cpow_def, if_false]
-  rw [analyticAt_congr e]
+  apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e
   exact ((fa.clog m).mul ga).cexp
 
+/-- `f z ^ g z` is analytic if `f z` is not a nonpositive real -/
+theorem AnalyticAt.cpow (fa : AnalyticAt ℂ f x) (ga : AnalyticAt ℂ g x)
+    (m : f x ∈ slitPlane) : AnalyticAt ℂ (fun z ↦ f z ^ g z) x := by
+  rw [← analyticWithinAt_univ] at fa ga ⊢
+  exact fa.cpow ga m
+
+/-- `f z ^ g z` is analytic if `f z` avoids nonpositive reals -/
+theorem AnalyticOnNhd.cpow (fs : AnalyticOnNhd ℂ f s) (gs : AnalyticOnNhd ℂ g s)
+    (m : ∀ z ∈ s, f z ∈ slitPlane) : AnalyticOnNhd ℂ (fun z ↦ f z ^ g z) s :=
+  fun z n ↦ (fs z n).cpow (gs z n) (m z n)
+
 /-- `f z ^ g z` is analytic if `f z` avoids nonpositive reals -/
 theorem AnalyticOn.cpow (fs : AnalyticOn ℂ f s) (gs : AnalyticOn ℂ g s)
     (m : ∀ z ∈ s, f z ∈ slitPlane) : AnalyticOn ℂ (fun z ↦ f z ^ g z) s :=
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
index 8f72e2ec290e0..4d4cee818d69d 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
@@ -547,13 +547,13 @@ theorem Gamma_mul_Gamma_add_half (s : ℂ) :
     convert congr_arg Inv.inv (congr_fun this s) using 1
     · rw [mul_inv, inv_inv, inv_inv]
     · rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-  have h1 : AnalyticOn ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ := by
-    refine DifferentiableOn.analyticOn ?_ isOpen_univ
+  have h1 : AnalyticOnNhd ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ := by
+    refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
     refine (differentiable_one_div_Gamma.mul ?_).differentiableOn
     exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))
-  have h2 : AnalyticOn ℂ
+  have h2 : AnalyticOnNhd ℂ
       (fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π)) univ := by
-    refine DifferentiableOn.analyticOn ?_ isOpen_univ
+    refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
     refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn
     apply Differentiable.mul
     · exact differentiable_one_div_Gamma.comp (differentiable_id'.const_mul _)
@@ -563,7 +563,7 @@ theorem Gamma_mul_Gamma_add_half (s : ℂ) :
     rw [tendsto_nhdsWithin_iff]; constructor
     · exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt
     · exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)
-  refine AnalyticOn.eq_of_frequently_eq h1 h2 (h3.frequently ?_)
+  refine AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_)
   refine ((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently
   refine (eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_)
   rw [← mul_inv, Gamma_ofReal, (by norm_num : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean
index c4ac634c52efb..e25efebbe63d0 100644
--- a/Mathlib/CategoryTheory/Closed/Cartesian.lean
+++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean
@@ -226,21 +226,15 @@ end CartesianClosed
 
 open CartesianClosed
 
-/-- Show that the exponential of the terminal object is isomorphic to itself, i.e. `X^1 ≅ X`.
+/-- The exponential with the terminal object is naturally isomorphic to the identity. The typeclass
+argument is explicit: any instance can be used.-/
+def expTerminalNatIso [Exponentiable (⊤_ C)] : 𝟭 C ≅ exp (⊤_ C) :=
+  MonoidalClosed.unitNatIso (C := C)
 
-The typeclass argument is explicit: any instance can be used.
--/
+/-- The exponential of any object with the terminal object is isomorphic to itself, i.e. `X^1 ≅ X`.
+The typeclass argument is explicit: any instance can be used.-/
 def expTerminalIsoSelf [Exponentiable (⊤_ C)] : (⊤_ C) ⟹ X ≅ X :=
-  Yoneda.ext ((⊤_ C) ⟹ X) X
-    (fun {Y} f => (Limits.prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f)
-    (fun {Y} f => CartesianClosed.curry ((Limits.prod.leftUnitor Y).hom ≫ f))
-    (fun g => by
-      rw [curry_eq_iff, Iso.hom_inv_id_assoc])
-    (fun g => by simp)
-    (fun f g => by
-      -- Porting note: `rw` is a bit brittle here, requiring the `dsimp` rule cancellation.
-      dsimp [-prod.leftUnitor_inv]
-      rw [uncurry_natural_left, prod.leftUnitor_inv_naturality_assoc f])
+  (expTerminalNatIso.app X).symm
 
 /-- The internal element which points at the given morphism. -/
 def internalizeHom (f : A ⟶ Y) : ⊤_ C ⟶ A ⟹ Y :=
diff --git a/Mathlib/CategoryTheory/Closed/Monoidal.lean b/Mathlib/CategoryTheory/Closed/Monoidal.lean
index 8309157796ab1..43af4d461c0de 100644
--- a/Mathlib/CategoryTheory/Closed/Monoidal.lean
+++ b/Mathlib/CategoryTheory/Closed/Monoidal.lean
@@ -196,6 +196,10 @@ theorem curry_id_eq_coev : curry (𝟙 _) = (ihom.coev A).app X := by
   rw [curry_eq, (ihom A).map_id (A ⊗ _)]
   apply comp_id
 
+/-- The internal hom out of the unit is naturally isomorphic to the identity functor.-/
+def unitNatIso [Closed (𝟙_ C)] : 𝟭 C ≅ ihom (𝟙_ C) :=
+  conjugateIsoEquiv (Adjunction.id (C := C)) (ihom.adjunction (𝟙_ C))
+    (leftUnitorNatIso C)
 section Pre
 
 variable {A B}
diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean
index 5b38bcb33b6e3..b68c2fb925d3d 100644
--- a/Mathlib/Data/Matrix/Invertible.lean
+++ b/Mathlib/Data/Matrix/Invertible.lean
@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Eric Wieser
+Authors: Eric Wieser, Ahmad Alkhalawi
 -/
 import Mathlib.Data.Matrix.Basic
+import Mathlib.Tactic.Abel
 
 /-! # Extra lemmas about invertible matrices
 
@@ -47,10 +48,12 @@ protected theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α)
 protected theorem mul_invOf_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
     A * B * ⅟ B = A := by rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]
 
-@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := invOf_mul_cancel_left
-@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := mul_invOf_cancel_left
-@[deprecated (since := "2024-09-07")] alias mul_invOf_mul_self_cancel := invOf_mul_cancel_right
-@[deprecated (since := "2024-09-07")] alias mul_mul_invOf_self_cancel := mul_invOf_cancel_right
+@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := Matrix.invOf_mul_cancel_left
+@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := Matrix.mul_invOf_cancel_left
+@[deprecated (since := "2024-09-07")]
+alias mul_invOf_mul_self_cancel := Matrix.invOf_mul_cancel_right
+@[deprecated (since := "2024-09-07")]
+alias mul_mul_invOf_self_cancel := Matrix.mul_invOf_cancel_right
 
 section ConjTranspose
 variable [StarRing α] (A : Matrix n n α)
@@ -106,4 +109,68 @@ def transposeInvertibleEquivInvertible : Invertible Aᵀ ≃ Invertible A where
 
 end CommSemiring
 
+section Ring
+
+section Woodbury
+
+variable [Fintype m] [DecidableEq m] [Ring α]
+    (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
+    [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)]
+
+-- No spaces around multiplication signs for better clarity
+lemma add_mul_mul_invOf_mul_eq_one :
+    (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) = 1 := by
+  calc
+    (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)
+    _ = A*⅟A - A*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A - U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by
+      simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]
+    _ = (1 + U*C*V*⅟A) - (U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) := by
+      rw [mul_invOf_self, Matrix.one_mul]
+      abel
+    _ = 1 + U*C*V*⅟A - (U + U*C*V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
+      rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]
+    _ = 1 + U*C*V*⅟A - U*C*(⅟C + V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
+      congr
+      simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc]
+    _ = 1 := by
+      rw [Matrix.mul_invOf_cancel_right]
+      abel
+
+/-- Like `add_mul_mul_invOf_mul_eq_one`, but with multiplication reversed. -/
+lemma add_mul_mul_invOf_mul_eq_one' :
+    (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V) = 1 := by
+  calc
+    (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V)
+    _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by
+      simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc]
+    _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by
+      rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]
+      abel
+    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by
+      rw [sub_right_inj, Matrix.mul_add]
+      simp_rw [Matrix.mul_assoc]
+    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by
+      congr 1
+      simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc,
+        Matrix.invOf_mul_cancel_right]
+    _ = 1 := by
+      rw [Matrix.invOf_mul_cancel_right]
+      abel
+
+/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A + U * C * V`-/
+def invertibleAddMulMul : Invertible (A + U*C*V) where
+  invOf := ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A
+  invOf_mul_self := add_mul_mul_invOf_mul_eq_one' _ _ _ _
+  mul_invOf_self := add_mul_mul_invOf_mul_eq_one _ _ _ _
+
+/-- The **Woodbury Identity** (`⅟` version). -/
+theorem invOf_add_mul_mul [Invertible (A + U*C*V)] :
+    ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by
+  letI := invertibleAddMulMul A U C V
+  convert (rfl : ⅟(A + U*C*V) = _)
+
+end Woodbury
+
+end Ring
+
 end Matrix
diff --git a/Mathlib/Data/Real/Archimedean.lean b/Mathlib/Data/Real/Archimedean.lean
index 320d601909bab..4df84980d7abb 100644
--- a/Mathlib/Data/Real/Archimedean.lean
+++ b/Mathlib/Data/Real/Archimedean.lean
@@ -3,8 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
 -/
-import Mathlib.Algebra.Bounds
 import Mathlib.Algebra.Order.Archimedean.Basic
+import Mathlib.Algebra.Order.Group.Pointwise.Bounds
 import Mathlib.Data.Real.Basic
 import Mathlib.Order.Interval.Set.Disjoint
 
diff --git a/Mathlib/Geometry/Manifold/AnalyticManifold.lean b/Mathlib/Geometry/Manifold/AnalyticManifold.lean
index 442b24423f19a..8ef606a4540a1 100644
--- a/Mathlib/Geometry/Manifold/AnalyticManifold.lean
+++ b/Mathlib/Geometry/Manifold/AnalyticManifold.lean
@@ -17,7 +17,7 @@ interior and smooth everywhere (including at the boundary).  The definition mirr
 analytic manifolds are smooth manifolds.
 
 Completeness is required throughout, but this is nonessential: it is due to many of the lemmas about
-AnalyticWithinOn` requiring completeness for ease of proof.
+AnalyticOn` requiring completeness for ease of proof.
 -/
 
 noncomputable section
@@ -42,10 +42,10 @@ analytic on the interior, and map the interior to itself.  This allows us to def
 section analyticGroupoid
 
 /-- Given a model with corners `(E, H)`, we define the pregroupoid of analytic transformations of
-`H` as the maps that are `AnalyticWithinOn` when read in `E` through `I`.  Using `AnalyticWithinOn`
-rather than `AnalyticOn` gives us meaningful definitions at boundary points. -/
+`H` as the maps that are `AnalyticOn` when read in `E` through `I`.  Using `AnalyticOn`
+rather than `AnalyticOnNhd` gives us meaningful definitions at boundary points. -/
 def analyticPregroupoid : Pregroupoid H where
-  property f s := AnalyticWithinOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I)
+  property f s := AnalyticOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I)
   comp {f g u v} hf hg _ _ _ := by
     have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp
     simp only [this]
@@ -54,12 +54,12 @@ def analyticPregroupoid : Pregroupoid H where
     · rintro x ⟨hx1, _⟩
       simpa only [mfld_simps] using hx1.2
   id_mem := by
-    apply analyticWithinOn_id.congr
+    apply analyticOn_id.congr
     rintro x ⟨_, hx2⟩
     obtain ⟨y, hy⟩ := mem_range.1 hx2
     simp only [mfld_simps, ← hy]
   locality {f u} _ H := by
-    apply analyticWithinOn_of_locally_analyticWithinOn
+    apply analyticOn_of_locally_analyticOn
     rintro y ⟨hy1, hy2⟩
     obtain ⟨x, hx⟩ := mem_range.1 hy2
     simp only [mfld_simps, ← hx] at hy1 ⊢
@@ -75,8 +75,8 @@ def analyticPregroupoid : Pregroupoid H where
     rw [fg _ hy1]
 
 /-- Given a model with corners `(E, H)`, we define the groupoid of analytic transformations of
-`H` as the maps that are `AnalyticWithinOn` when read in `E` through `I`.  Using `AnalyticWithinOn`
-rather than `AnalyticOn` gives us meaningful definitions at boundary points. -/
+`H` as the maps that are `AnalyticOn` when read in `E` through `I`.  Using `AnalyticOn`
+rather than `AnalyticOnNhd` gives us meaningful definitions at boundary points. -/
 def analyticGroupoid : StructureGroupoid H :=
   (analyticPregroupoid I).groupoid
 
@@ -84,9 +84,9 @@ def analyticGroupoid : StructureGroupoid H :=
 theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) :
     PartialHomeomorph.ofSet s hs ∈ analyticGroupoid I := by
   rw [analyticGroupoid, mem_groupoid_of_pregroupoid]
-  suffices h : AnalyticWithinOn 𝕜 (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by
+  suffices h : AnalyticOn 𝕜 (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by
     simp [h, analyticPregroupoid]
-  have hi : AnalyticWithinOn 𝕜 id (univ : Set E) := analyticWithinOn_id
+  have hi : AnalyticOn 𝕜 id (univ : Set E) := analyticOn_id
   exact (hi.mono (subset_univ _)).congr (fun x hx ↦ I.right_inv hx.2)
 
 /-- The composition of a partial homeomorphism from `H` to `M` and its inverse belongs to
@@ -108,17 +108,17 @@ instance : ClosedUnderRestriction (analyticGroupoid I) :=
 /-- `f ∈ analyticGroupoid` iff it and its inverse are analytic within `range I`. -/
 lemma mem_analyticGroupoid {I : ModelWithCorners 𝕜 E H} {f : PartialHomeomorph H H} :
     f ∈ analyticGroupoid I ↔
-      AnalyticWithinOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' f.source ∩ range I) ∧
-      AnalyticWithinOn 𝕜 (I ∘ f.symm ∘ I.symm) (I.symm ⁻¹' f.target ∩ range I) := by
+      AnalyticOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' f.source ∩ range I) ∧
+      AnalyticOn 𝕜 (I ∘ f.symm ∘ I.symm) (I.symm ⁻¹' f.target ∩ range I) := by
   rfl
 
 /-- The analytic groupoid on a boundaryless charted space modeled on a complete vector space
 consists of the partial homeomorphisms which are analytic and have analytic inverse. -/
 theorem mem_analyticGroupoid_of_boundaryless [I.Boundaryless] (e : PartialHomeomorph H H) :
-    e ∈ analyticGroupoid I ↔ AnalyticOn 𝕜 (I ∘ e ∘ I.symm) (I '' e.source) ∧
-      AnalyticOn 𝕜 (I ∘ e.symm ∘ I.symm) (I '' e.target) := by
+    e ∈ analyticGroupoid I ↔ AnalyticOnNhd 𝕜 (I ∘ e ∘ I.symm) (I '' e.source) ∧
+      AnalyticOnNhd 𝕜 (I ∘ e.symm ∘ I.symm) (I '' e.target) := by
   simp only [mem_analyticGroupoid, I.range_eq_univ, inter_univ, I.image_eq]
-  rw [IsOpen.analyticWithinOn_iff_analyticOn, IsOpen.analyticWithinOn_iff_analyticOn]
+  rw [IsOpen.analyticOn_iff_analyticOnNhd, IsOpen.analyticOn_iff_analyticOnNhd]
   · exact I.continuous_symm.isOpen_preimage _ e.open_target
   · exact I.continuous_symm.isOpen_preimage _ e.open_source
 
@@ -131,12 +131,12 @@ theorem analyticGroupoid_prod {E A : Type} [NormedAddCommGroup E] [NormedSpace 
     f.prod g ∈ analyticGroupoid (I.prod J) := by
   have pe : range (I.prod J) = (range I).prod (range J) := I.range_prod
   simp only [mem_analyticGroupoid, Function.comp, image_subset_iff] at fa ga ⊢
-  exact ⟨AnalyticWithinOn.prod
-      (fa.1.comp analyticWithinOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
-      (ga.1.comp analyticWithinOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩),
-    AnalyticWithinOn.prod
-      (fa.2.comp analyticWithinOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
-      (ga.2.comp analyticWithinOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩)⟩
+  exact ⟨AnalyticOn.prod
+      (fa.1.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
+      (ga.1.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩),
+    AnalyticOn.prod
+      (fa.2.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
+      (ga.2.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩)⟩
 
 end analyticGroupoid
 
diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
index 0ba84d9e908d0..1482f940cd82d 100644
--- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
+++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
@@ -607,6 +607,24 @@ theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse
 
 end Diagonal
 
+section Woodbury
+
+variable [Fintype m] [DecidableEq m]
+variable (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
+
+/-- The **Woodbury Identity** (`⁻¹` version). -/
+theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) :
+    (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ := by
+  obtain ⟨_⟩ := hA.nonempty_invertible
+  obtain ⟨_⟩ := hC.nonempty_invertible
+  obtain ⟨iAC⟩ := hAC.nonempty_invertible
+  simp only [← invOf_eq_nonsing_inv] at iAC
+  letI := invertibleAddMulMul A U C V
+  simp only [← invOf_eq_nonsing_inv]
+  apply invOf_add_mul_mul
+
+end Woodbury
+
 @[simp]
 theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := by
   by_cases h : IsUnit A.det
diff --git a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
index 9326504897129..76566b1a9cc1e 100644
--- a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
+++ b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Order.Pointwise
+import Mathlib.Algebra.Order.Field.Pointwise
 import Mathlib.Analysis.NormedSpace.SphereNormEquiv
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.MeasureTheory.Constructions.Prod.Integral
diff --git a/Mathlib/NumberTheory/LSeries/Deriv.lean b/Mathlib/NumberTheory/LSeries/Deriv.lean
index d9a355faf2a9f..f8f5726a088aa 100644
--- a/Mathlib/NumberTheory/LSeries/Deriv.lean
+++ b/Mathlib/NumberTheory/LSeries/Deriv.lean
@@ -20,7 +20,7 @@ import Mathlib.Analysis.Complex.HalfPlane
 * We prove similar results for iterated derivatives (`LSeries.iteratedDeriv`).
 
 * We use this to show that `LSeries f` is holomorphic on the right half-plane of
-  absolute convergence (`LSeries.analyticOn`).
+  absolute convergence (`LSeries.analyticOnNhd`).
 
 ## Implementation notes
 
@@ -151,6 +151,10 @@ lemma LSeries_differentiableOn (f : ℕ → ℂ) :
   fun _ hz ↦ (LSeries_hasDerivAt hz).differentiableAt.differentiableWithinAt
 
 /-- The L-series of `f` is holomorphic on its open half-plane of absolute convergence. -/
+lemma LSeries_analyticOnNhd (f : ℕ → ℂ) :
+    AnalyticOnNhd ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} :=
+  (LSeries_differentiableOn f).analyticOnNhd <| isOpen_re_gt_EReal _
+
 lemma LSeries_analyticOn (f : ℕ → ℂ) :
     AnalyticOn ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} :=
-  (LSeries_differentiableOn f).analyticOn <| isOpen_re_gt_EReal _
+  (LSeries_analyticOnNhd f).analyticOn
diff --git a/Mathlib/NumberTheory/LSeries/ZMod.lean b/Mathlib/NumberTheory/LSeries/ZMod.lean
index 66dbde51f1f55..2ef6c910b132d 100644
--- a/Mathlib/NumberTheory/LSeries/ZMod.lean
+++ b/Mathlib/NumberTheory/LSeries/ZMod.lean
@@ -177,13 +177,13 @@ lemma LFunction_stdAddChar_eq_expZeta (j : ZMod N) (s : ℂ) (hjs : j ≠ 0 ∨
   let g := expZeta (toAddCircle j)
   have hU {u} : u ∈ U ↔ u ≠ 1 ∨ j ≠ 0 := by simp only [mem_ite_univ_right, U]; tauto
   -- hypotheses for uniqueness of analytic continuation
-  have hf : AnalyticOn ℂ f U := by
-    refine DifferentiableOn.analyticOn (fun u hu ↦ ?_) hUo
+  have hf : AnalyticOnNhd ℂ f U := by
+    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
     refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
     simp only [mul_comm j, AddChar.sum_mulShift _ (isPrimitive_stdAddChar _), h,
       ↓reduceIte, CharP.cast_eq_zero, or_true]
-  have hg : AnalyticOn ℂ g U := by
-    refine DifferentiableOn.analyticOn (fun u hu ↦ ?_) hUo
+  have hg : AnalyticOnNhd ℂ g U := by
+    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
     refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
     rwa [ne_eq, toAddCircle_eq_zero]
   have hUc : IsPreconnected U := by
@@ -451,7 +451,7 @@ Functional equation for completed L-functions (even case), valid at all points o
 theorem completedLFunction_one_sub_even (hΦ : Φ.Even) (s : ℂ)
     (hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0) (hs₁ : s ≠ 1 ∨ Φ 0 = 0) :
     completedLFunction Φ (1 - s) = N ^ (s - 1) * completedLFunction (𝓕 Φ) s := by
-  -- We prove this using `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`, so we need to
+  -- We prove this using `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`, so we need to
   -- gather up the ingredients for this big theorem.
   -- First set up some notations:
   let F (t) := completedLFunction Φ (1 - t)
@@ -477,12 +477,14 @@ theorem completedLFunction_one_sub_even (hΦ : Φ.Even) (s : ℂ)
       simp [U, Uc, h, h', and_comm]
     · simp only [rank_real_complex, Nat.one_lt_ofNat]
   -- Analyticity on U:
-  have hF : AnalyticOn ℂ F U := by
-    refine DifferentiableOn.analyticOn (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo
+  have hF : AnalyticOnNhd ℂ F U := by
+    refine DifferentiableOn.analyticOnNhd
+      (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo
     refine (differentiableAt_completedLFunction Φ _ ?_ ?_).comp t (differentiableAt_id.const_sub 1)
     exacts [ht.2.imp_left (sub_ne_zero.mpr ∘ Ne.symm), ht.1.imp_left sub_eq_self.not.mpr]
-  have hG : AnalyticOn ℂ G U := by
-    refine DifferentiableOn.analyticOn (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo
+  have hG : AnalyticOnNhd ℂ G U := by
+    refine DifferentiableOn.analyticOnNhd
+      (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo
     apply ((differentiableAt_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul
     apply differentiableAt_completedLFunction _ _ (ht.1.imp_right fun h ↦ dft_apply_zero Φ ▸ h)
     exact ht.2.imp_right (fun h ↦ by simp only [← dft_apply_zero, dft_dft, neg_zero, h, smul_zero])
@@ -512,7 +514,7 @@ theorem completedLFunction_one_sub_odd (hΦ : Φ.Odd) (s : ℂ) :
   have hFG : F =ᶠ[𝓝 2] G := by filter_upwards [this] with t ht
     using completedLFunction_one_sub_of_one_lt_odd hΦ ht
   -- now apply the big hammer to finish
-  rw [← analyticOn_univ_iff_differentiable] at hF hG
+  rw [← analyticOnNhd_univ_iff_differentiable] at hF hG
   exact congr_fun (hF.eq_of_eventuallyEq hG hFG) s
 
 end signed
diff --git a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
index e7baa70d5b32b..ddec8ac7b3058 100644
--- a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
@@ -54,8 +54,6 @@ theorem not_injective_limitation_set : ¬ InjOn g (Iio (ord <| succ #α)) := by
   rw [mk_initialSeg_subtype, lift_lift, lift_le] at h
   exact not_le_of_lt (Order.lt_succ #α) h
 
-
-
 end Cardinal
 
 namespace OrdinalApprox
@@ -76,7 +74,8 @@ termination_by a
 decreasing_by exact h
 
 theorem lfpApprox_monotone : Monotone (lfpApprox f x) := by
-  unfold Monotone; intros a b h; unfold lfpApprox
+  intros a b h
+  rw [lfpApprox, lfpApprox]
   refine sSup_le_sSup ?h
   apply sup_le_sup_right
   simp only [exists_prop, Set.le_eq_subset, Set.setOf_subset_setOf, forall_exists_index, and_imp,
@@ -86,14 +85,14 @@ theorem lfpApprox_monotone : Monotone (lfpApprox f x) := by
   exact ⟨lt_of_lt_of_le h' h, rfl⟩
 
 theorem le_lfpApprox {a : Ordinal} : x ≤ lfpApprox f x a := by
-  unfold lfpApprox
+  rw [lfpApprox]
   apply le_sSup
   simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, true_or]
 
 theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
     lfpApprox f x (a+1) = f (lfpApprox f x a) := by
   apply le_antisymm
-  · conv => left; unfold lfpApprox
+  · conv => left; rw [lfpApprox]
     apply sSup_le
     simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.union_singleton,
       Set.mem_insert_iff, Set.mem_setOf_eq, forall_eq_or_imp, forall_exists_index, and_imp,
@@ -104,7 +103,7 @@ theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
       exact le_lfpApprox f x
     · intros a' h
       apply f.2; apply lfpApprox_monotone; exact h
-  · conv => right; unfold lfpApprox
+  · conv => right; rw [lfpApprox]
     apply le_sSup
     simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop]
     rw [Set.mem_union]
@@ -112,13 +111,46 @@ theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
     simp only [Set.mem_setOf_eq]
     use a
 
+theorem lfpApprox_mono_left : Monotone (lfpApprox : (α →o α) → _) := by
+  intro f g h x a
+  induction a using Ordinal.induction with
+  | h i ih =>
+    rw [lfpApprox, lfpApprox]
+    apply sSup_le
+    simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert,
+      forall_eq_or_imp, le_sup_left, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
+      true_and]
+    intro i' h_lt
+    apply le_sup_of_le_right
+    apply le_sSup_of_le
+    · use i'
+    · apply le_trans (h _)
+      simp only [OrderHom.toFun_eq_coe]
+      exact g.monotone (ih i' h_lt)
+
+theorem lfpApprox_mono_mid : Monotone (lfpApprox f) := by
+  intro x₁ x₂ h a
+  induction a using Ordinal.induction with
+  | h i ih =>
+    rw [lfpApprox, lfpApprox]
+    apply sSup_le
+    simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert,
+      forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
+    constructor
+    · exact le_sup_of_le_left h
+    · intro i' h_i'
+      apply le_sup_of_le_right
+      apply le_sSup_of_le
+      · use i'
+      · exact f.monotone (ih i' h_i')
+
 /-- The approximations of the least fixed point stabilize at a fixed point of `f` -/
 theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_ab : a ≤ b)
     (h : lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a := by
   rw [mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
-  · conv => left; unfold lfpApprox
+  · conv => left; rw [lfpApprox]
     apply sSup_le
     simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq,
       forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
@@ -178,7 +210,7 @@ theorem lfpApprox_le_of_mem_fixedPoints {a : α}
     (h_a : a ∈ fixedPoints f) (h_le_init : x ≤ a) (i : Ordinal) : lfpApprox f x i ≤ a := by
   induction i using Ordinal.induction with
   | h i IH =>
-    unfold lfpApprox
+    rw [lfpApprox]
     apply sSup_le
     simp only [exists_prop]
     intro y h_y
@@ -187,8 +219,7 @@ theorem lfpApprox_le_of_mem_fixedPoints {a : α}
     | inl h_y =>
       let ⟨j, h_j_lt, h_j⟩ := h_y
       rw [← h_j, ← h_a]
-      apply f.monotone'
-      exact IH j h_j_lt
+      exact f.monotone' (IH j h_j_lt)
     | inr h_y =>
       rw [h_y]
       exact h_le_init
@@ -234,6 +265,13 @@ theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) :
     gfpApprox f x (a+1) = f (gfpApprox f x a) :=
   lfpApprox_add_one (OrderHom.dual f) x h a
 
+theorem gfpApprox_mono_left : Monotone (gfpApprox : (α →o α) → _) := by
+  intro f g h
+  have : OrderHom.dual g ≤ OrderHom.dual f := h
+  exact lfpApprox_mono_left this
+
+theorem gfpApprox_mono_mid : Monotone (gfpApprox f) :=
+  fun _ _ h => lfpApprox_mono_mid (OrderHom.dual f) h
 
 /-- The approximations of the greatest fixed point stabilize at a fixed point of `f` -/
 theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : f x ≤ x) (h_ab : a ≤ b)
diff --git a/Mathlib/Topology/MetricSpace/Algebra.lean b/Mathlib/Topology/MetricSpace/Algebra.lean
index c2d744b24f070..724512392f31b 100644
--- a/Mathlib/Topology/MetricSpace/Algebra.lean
+++ b/Mathlib/Topology/MetricSpace/Algebra.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import Mathlib.Topology.Algebra.MulAction
+import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.MetricSpace.Lipschitz
 
 /-!
@@ -143,6 +144,11 @@ instance (priority := 100) BoundedSMul.continuousSMul : ContinuousSMul α β whe
           gcongr
       _ < ε := hδε
 
+instance (priority := 100) BoundedSMul.toUniformContinuousConstSMul :
+    UniformContinuousConstSMul α β :=
+  ⟨fun c => ((lipschitzWith_iff_dist_le_mul (K := nndist c 0)).2 fun _ _ =>
+    dist_smul_pair c _ _).uniformContinuous⟩
+
 -- this instance could be deduced from `NormedSpace.boundedSMul`, but we prove it separately
 -- here so that it is available earlier in the hierarchy
 instance Real.boundedSMul : BoundedSMul ℝ ℝ where
diff --git a/Mathlib/Topology/MetricSpace/Completion.lean b/Mathlib/Topology/MetricSpace/Completion.lean
index 1ffdfa1fba1b7..97c5f07d31c6e 100644
--- a/Mathlib/Topology/MetricSpace/Completion.lean
+++ b/Mathlib/Topology/MetricSpace/Completion.lean
@@ -6,6 +6,8 @@ Authors: Sébastien Gouëzel
 import Mathlib.Topology.UniformSpace.Completion
 import Mathlib.Topology.MetricSpace.Isometry
 import Mathlib.Topology.MetricSpace.Lipschitz
+import Mathlib.Topology.MetricSpace.Algebra
+import Mathlib.Topology.Algebra.GroupCompletion
 import Mathlib.Topology.Instances.Real
 
 /-!
@@ -168,6 +170,27 @@ theorem coe_isometry : Isometry ((↑) : α → Completion α) :=
 protected theorem edist_eq (x y : α) : edist (x : Completion α) y = edist x y :=
   coe_isometry x y
 
+instance {M} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [BoundedSMul M α] :
+    BoundedSMul M (Completion α) where
+  dist_smul_pair' c x₁ x₂ := by
+    induction x₁, x₂ using induction_on₂ with
+    | hp =>
+      exact isClosed_le
+        ((continuous_fst.const_smul _).dist (continuous_snd.const_smul _))
+        (continuous_const.mul (continuous_fst.dist continuous_snd))
+    | ih x₁ x₂ =>
+      rw [← coe_smul, ← coe_smul, Completion.dist_eq,  Completion.dist_eq]
+      exact dist_smul_pair c x₁ x₂
+  dist_pair_smul' c₁ c₂ x := by
+    induction x using induction_on with
+    | hp =>
+      exact isClosed_le
+        ((continuous_const_smul _).dist (continuous_const_smul _))
+        (continuous_const.mul (continuous_id.dist continuous_const))
+    | ih x =>
+      rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq]
+      exact dist_pair_smul c₁ c₂ x
+
 end UniformSpace.Completion
 
 open UniformSpace Completion NNReal
diff --git a/docs/overview.yaml b/docs/overview.yaml
index be28612dbf810..e1d21817d53b5 100644
--- a/docs/overview.yaml
+++ b/docs/overview.yaml
@@ -352,7 +352,7 @@ Analysis:
     Liouville theorem: 'Differentiable.apply_eq_apply_of_bounded'
     maximum modulus principle: 'Complex.eventually_eq_of_isLocalMax_norm'
     principle of isolated zeros: 'AnalyticAt.eventually_eq_zero_or_eventually_ne_zero'
-    principle of analytic continuation: 'AnalyticOn.eqOn_of_preconnected_of_frequently_eq'
+    principle of analytic continuation: 'AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq'
     analyticity of holomorphic functions: 'DifferentiableOn.analyticAt'
     Schwarz lemma: 'Complex.abs_le_abs_of_mapsTo_ball_self'
     removable singularity: 'Complex.differentiableOn_update_limUnder_insert_of_isLittleO'
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
index 21619980559e5..f1113456868a1 100644
--- a/docs/undergrad.yaml
+++ b/docs/undergrad.yaml
@@ -387,7 +387,7 @@ Single Variable Complex Analysis:
     Cauchy formulas: 'Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable'
     analyticity of a holomorphic function: 'DifferentiableOn.analyticAt'
     principle of isolated zeros: 'AnalyticAt.eventually_eq_zero_or_eventually_ne_zero'
-    principle of analytic continuation: 'AnalyticOn.eqOn_of_preconnected_of_frequently_eq'
+    principle of analytic continuation: 'AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq'
     maximum principle: 'Complex.eventually_eq_of_isLocalMax_norm'
     isolated singularities: ''
     Laurent series: ''
diff --git a/lake-manifest.json b/lake-manifest.json
index 0cedc34894a16..f82a37b5c0c11 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d5e1c81277e960372c94f19172440e39b3c5980",
+   "rev": "c57ab80c8dd20b345b29c81c446c78a6b3677d20",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/scripts/create-adaptation-pr.sh b/scripts/create-adaptation-pr.sh
index 2e7d69f7916d8..4fb326cfac9d6 100755
--- a/scripts/create-adaptation-pr.sh
+++ b/scripts/create-adaptation-pr.sh
@@ -21,9 +21,10 @@ AUTO="no"
 usage() {
   echo "Usage: $0 <BUMPVERSION> <NIGHTLYDATE>"
   echo "       or"
-  echo "       $0 --bumpversion=<BUMPVERSION> --nightlydate=<NIGHTLYDATE> [--auto=<yes|no>]"
+  echo "       $0 --bumpversion=<BUMPVERSION> --nightlydate=<NIGHTLYDATE> --nightlysha=<SHA> [--auto=<yes|no>]"
   echo "BUMPVERSION: The upcoming release that we are targeting, e.g., 'v4.10.0'"
   echo "NIGHTLYDATE: The date of the nightly toolchain currently used on 'nightly-testing'"
+  echo "NIGHTLYSHA: The SHA of the nightly toolchain that we want to adapt to"
   echo "AUTO: Optional flag to specify automatic mode, default is 'no'"
   exit 1
 }
@@ -43,6 +44,10 @@ elif [ $# -ge 2 ]; then
         NIGHTLYDATE="${arg#*=}"
         shift
         ;;
+      --nightlysha=*)
+        NIGHTLYSHA="${arg#*=}"
+        shift
+        ;;
       --auto=*)
         AUTO="${arg#*=}"
         shift
@@ -148,15 +153,14 @@ echo
 echo "### [auto] create a new branch 'bump/nightly-$NIGHTLYDATE' and merge the latest changes from 'origin/nightly-testing'"
 
 git checkout -b "bump/nightly-$NIGHTLYDATE"
-git merge origin/nightly-testing || true # ignore error if there are conflicts
+git merge $NIGHTLYSHA || true # ignore error if there are conflicts
 
 # Check if there are merge conflicts
 if git diff --name-only --diff-filter=U | grep -q .; then
   echo
   echo "### [auto] Conflict resolution"
-  echo "### Automatically choosing 'lean-toolchain' and 'lake-manifest.json' from the newer branch"
-  echo "### In this case, the newer branch is 'origin/nightly-testing'"
-  git checkout origin/nightly-testing -- lean-toolchain lake-manifest.json
+  echo "### Automatically choosing 'lean-toolchain' and 'lake-manifest.json' from 'nightly-testing'"
+  git checkout $NIGHTLYSHA -- lean-toolchain lake-manifest.json
   git add lean-toolchain lake-manifest.json
 fi
 
@@ -172,6 +176,8 @@ if git diff --name-only --diff-filter=U | grep -q .; then
   echo
   echo "### [user] Conflict resolution"
   echo "We are merging the latest changes from 'origin/nightly-testing' into 'bump/nightly-$NIGHTLYDATE'"
+  echo "Specifically, we are merging the following version of 'origin/nightly-testing':"
+  echo "$NIGHTLYSHA"
   echo "There seem to be conflicts: please resolve them"
   echo ""
   echo "  1) Open `pwd` in a new terminal and run 'git status'"
diff --git a/scripts/no_lints_prime_decls.txt b/scripts/no_lints_prime_decls.txt
index 048a285c74a49..5a3fa4e0c5ec5 100644
--- a/scripts/no_lints_prime_decls.txt
+++ b/scripts/no_lints_prime_decls.txt
@@ -162,10 +162,10 @@ AlgHom.coe_restrictScalars'
 AlgHom.toAddMonoidHom'
 AlgHom.toMonoidHom'
 AlternatingMap.domCoprod.summand_mk''
-analyticOn_congr'
-AnalyticOn.congr'
-AnalyticOn.eval_continuousLinearMap'
-AnalyticOn.eval_linearMap'
+analyticOnNhd_congr'
+AnalyticOnNhd.congr'
+AnalyticOnNhd.eval_continuousLinearMap'
+AnalyticOnNhd.eval_linearMap'
 AntilipschitzWith.le_mul_nnnorm'
 AntilipschitzWith.le_mul_norm'
 AntilipschitzWith.to_rightInvOn'