feat: finish forward port of #18877 (#5011)

leanprover-community/mathlib#18877

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -5,7 +5,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Fréd
   Heather Macbeth
 
 ! This file was ported from Lean 3 source module topology.algebra.module.basic
-! leanprover-community/mathlib commit f430769b562e0cedef59ee1ed968d67e0e0c86ba
+! leanprover-community/mathlib commit e354e865255654389cc46e6032160238df2e0f40
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1154,6 +1154,19 @@ theorem range_coprod [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃]
   LinearMap.range_coprod _ _
 #align continuous_linear_map.range_coprod ContinuousLinearMap.range_coprod
 
+theorem comp_fst_add_comp_snd [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃] (f : M₁ →L[R₁] M₃)
+    (g : M₂ →L[R₁] M₃) :
+    f.comp (ContinuousLinearMap.fst R₁ M₁ M₂) + g.comp (ContinuousLinearMap.snd R₁ M₁ M₂) =
+      f.coprod g :=
+  rfl
+#align continuous_linear_map.comp_fst_add_comp_snd ContinuousLinearMap.comp_fst_add_comp_snd
+
+theorem coprod_inl_inr [ContinuousAdd M₁] [ContinuousAdd M'₁] :
+    (ContinuousLinearMap.inl R₁ M₁ M'₁).coprod (ContinuousLinearMap.inr R₁ M₁ M'₁) =
+      ContinuousLinearMap.id R₁ (M₁ × M'₁) :=
+  by apply coe_injective; apply LinearMap.coprod_inl_inr
+#align continuous_linear_map.coprod_inl_inr ContinuousLinearMap.coprod_inl_inr
+
 section
 
 variable {R S : Type _} [Semiring R] [Semiring S] [Module R M₁] [Module R M₂] [Module R S]

Mathlib/Topology/Basic.lean

@@ -1990,14 +1990,14 @@ Another better solution is to reformulate composition lemmas to have the followi
 `ContinuousAt g y → ContinuousAt f x → f x = y → ContinuousAt (g ∘ f) x`.
 This is even useful if the proof of `f x = y` is `rfl`.
 The reason that this works better is because the type of `hg` doesn't mention `f`.
-Only after elaborating the two `continuous_at` arguments, Lean will try to unify `f x` with `y`,
+Only after elaborating the two `ContinuousAt` arguments, Lean will try to unify `f x` with `y`,
 which is often easy after having chosen the correct functions for `f` and `g`.
 Here is an example that shows the difference:
 ```
 example [TopologicalSpace α] [TopologicalSpace β] {x₀ : α} (f : α → α → β)
     (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) :
     ContinuousAt (fun x ↦ f x x) x₀ :=
-  -- hf.comp x₀ (continuousAt_id.prod continuousAt_id) -- type mismatch
+  -- hf.comp (continuousAt_id.prod continuousAt_id) -- type mismatch
   -- hf.comp_of_eq (continuousAt_id.prod continuousAt_id) rfl -- works
 ```
 -/

test/Continuity.lean

@@ -62,3 +62,11 @@ example (f : C(X × Y, Z)) (a : X) : Continuous (Function.curry f a) := --by con
   f.continuous.comp (continuous_const.prod_mk continuous_id)
 
 end basic
+
+/-! Some tests of the `comp_of_eq` lemmas -/
+
+example {α β : Type _} [TopologicalSpace α] [TopologicalSpace β] {x₀ : α} (f : α → α → β)
+  (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) :
+  ContinuousAt (λ x ↦ f x x) x₀ := by
+  fail_if_success { exact hf.comp (continuousAt_id.prod continuousAt_id) }
+  exact hf.comp_of_eq (continuousAt_id.prod continuousAt_id) rfl