From e0face0fac2ca1e589c7d002f922c755167004cd Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Tue, 6 Jan 2026 17:50:00 +0100
Subject: [PATCH 1/2] cherry pick

---
 .../Normed/Operator/BoundedLinearMaps.lean    | 36 +++++++++++++++++--
 Mathlib/Topology/ContinuousOn.lean            |  3 +-
 2 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean b/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
index 42c28550f8218d..eb28346ec56903 100644
--- a/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
+++ b/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
@@ -456,16 +456,30 @@ theorem Continuous.clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F
     (hg : Continuous g) (hf : Continuous f) : Continuous fun x => (g x).comp (f x) :=
   (compL 𝕜 E F G).continuous₂.comp₂ hg hf
 
+@[fun_prop]
 theorem ContinuousOn.clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
     {s : Set X} (hg : ContinuousOn g s) (hf : ContinuousOn f s) :
     ContinuousOn (fun x => (g x).comp (f x)) s :=
   (compL 𝕜 E F G).continuous₂.comp_continuousOn (hg.prodMk hf)
 
+@[fun_prop]
+theorem ContinuousAt.clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
+    {x : X} (hg : ContinuousAt g x) (hf : ContinuousAt f x) :
+    ContinuousAt (fun x => (g x).comp (f x)) x :=
+  (compL 𝕜 E F G).continuous₂.continuousAt.comp (hg.prodMk hf)
+
+@[fun_prop]
+theorem ContinuousWithinAt.clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
+    {s : Set X} {x : X} (hg : ContinuousWithinAt g s x) (hf : ContinuousWithinAt f s x) :
+    ContinuousWithinAt (fun x => (g x).comp (f x)) s x :=
+  (compL 𝕜 E F G).continuous₂.continuousAt.comp_continuousWithinAt (hg.prodMk hf)
+
 @[continuity, fun_prop]
 theorem Continuous.clm_apply {f : X → E →L[𝕜] F} {g : X → E}
     (hf : Continuous f) (hg : Continuous g) : Continuous (fun x ↦ f x (g x)) :=
   isBoundedBilinearMap_apply.continuous.comp₂ hf hg
 
+@[fun_prop]
 theorem ContinuousOn.clm_apply {f : X → E →L[𝕜] F} {g : X → E}
     {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
     ContinuousOn (fun x ↦ f x (g x)) s :=
@@ -482,19 +496,37 @@ theorem ContinuousWithinAt.clm_apply {X} [TopologicalSpace X] {f : X → E →L[
     ContinuousWithinAt (fun x ↦ f x (g x)) s x :=
   isBoundedBilinearMap_apply.continuous.continuousAt.comp_continuousWithinAt (hf.prodMk hg)
 
+@[fun_prop]
+theorem ContinuousWithinAt.continuousLinearMapCoprod
+    {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G} {s : Set X} {x : X}
+    (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
+    ContinuousWithinAt (fun x => (f x).coprod (g x)) s x := by
+  simp only [← comp_fst_add_comp_snd]
+  fun_prop
+
+@[fun_prop]
+theorem ContinuousAt.continuousLinearMapCoprod
+    {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G} {x : X}
+    (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
+    ContinuousAt (fun x => (f x).coprod (g x)) x := by
+  simp only [← comp_fst_add_comp_snd]
+  fun_prop
+
+@[fun_prop]
 theorem ContinuousOn.continuousLinearMapCoprod
     {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G} {s : Set X}
     (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
     ContinuousOn (fun x => (f x).coprod (g x)) s := by
   simp only [← comp_fst_add_comp_snd]
-  exact (hf.clm_comp continuousOn_const).add (hg.clm_comp continuousOn_const)
+  fun_prop
 
+@[fun_prop]
 theorem Continuous.continuousLinearMapCoprod
     {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G}
     (hf : Continuous f) (hg : Continuous g) :
     Continuous (fun x => (f x).coprod (g x)) := by
   apply continuousOn_univ.mp
-  exact hf.continuousOn.continuousLinearMapCoprod hg.continuousOn
+  fun_prop
 
 end
 
diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean
index 4a068b01931212..75c74c6784ccf9 100644
--- a/Mathlib/Topology/ContinuousOn.lean
+++ b/Mathlib/Topology/ContinuousOn.lean
@@ -488,7 +488,7 @@ theorem ContinuousWithinAt.comp_of_mem_nhdsWithin_image_of_eq {g : β → γ} {t
     (hs : t ∈ 𝓝[f '' s] y) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x := by
   subst hy; exact hg.comp_of_mem_nhdsWithin_image hf hs
 
-theorem ContinuousAt.comp_continuousWithinAt {g : β → γ}
+@[fun_prop] theorem ContinuousAt.comp_continuousWithinAt {g : β → γ}
     (hg : ContinuousAt g (f x)) (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (g ∘ f) s x :=
   hg.continuousWithinAt.comp hf (mapsTo_univ _ _)
 
@@ -729,6 +729,7 @@ theorem continuousOn_apply {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSp
 theorem continuousOn_const {s : Set α} {c : β} : ContinuousOn (fun _ => c) s :=
   continuous_const.continuousOn
 
+@[fun_prop]
 theorem continuousWithinAt_const {b : β} {s : Set α} {x : α} :
     ContinuousWithinAt (fun _ : α => b) s x :=
   continuous_const.continuousWithinAt

From 63345b0a6b8102c8fcabf3c36e34d9d1bd72133f Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Wed, 7 Jan 2026 13:26:03 +0100
Subject: [PATCH 2/2] fix

---
 Mathlib/Topology/Algebra/Monoid/Defs.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Monoid/Defs.lean b/Mathlib/Topology/Algebra/Monoid/Defs.lean
index 3e16842739e7c7..b8b777d10d83c7 100644
--- a/Mathlib/Topology/Algebra/Monoid/Defs.lean
+++ b/Mathlib/Topology/Algebra/Monoid/Defs.lean
@@ -72,7 +72,7 @@ theorem Continuous.mul (hf : Continuous f) (hg : Continuous g) :
     Continuous fun x => f x * g x :=
   continuous_mul.comp₂ hf hg
 
-@[to_additive]
+@[to_additive (attr := fun_prop)]
 theorem ContinuousWithinAt.mul (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
     ContinuousWithinAt (fun x => f x * g x) s x :=
   Filter.Tendsto.mul hf hg