chore: deprecate UniformSpace.Completion.Continuous.mul (#20145)

By adding a missing instance, this becomes just a really weird way to spell `Continuous.mul`.

Author: eric-wieser

Mathlib/Topology/Algebra/UniformRing.lean

@@ -65,63 +65,66 @@ theorem coe_mul (a b : α) : ((a * b : α) : Completion α) = a * b :=
 
 variable [UniformAddGroup α]
 
-theorem continuous_mul : Continuous fun p : Completion α × Completion α => p.1 * p.2 := by
-  let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
-  have : Continuous fun p : α × α => m p.1 p.2 := by
-    apply (continuous_coe α).comp _
-    simp only [AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft]
-    exact _root_.continuous_mul
-  have di : IsDenseInducing (toCompl : α → Completion α) := isDenseInducing_coe
-  convert di.extend_Z_bilin di this
-
-theorem Continuous.mul {β : Type*} [TopologicalSpace β] {f g : β → Completion α}
+instance : ContinuousMul (Completion α) where
+  continuous_mul := by
+    let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
+    have : Continuous fun p : α × α => m p.1 p.2 := (continuous_coe α).comp continuous_mul
+    have di : IsDenseInducing (toCompl : α → Completion α) := isDenseInducing_coe
+    exact (di.extend_Z_bilin di this :)
+
+@[deprecated _root_.continuous_mul (since := "2024-12-21")]
+protected theorem continuous_mul : Continuous fun p : Completion α × Completion α => p.1 * p.2 :=
+  _root_.continuous_mul
+
+@[deprecated _root_.Continuous.mul (since := "2024-12-21")]
+protected theorem Continuous.mul {β : Type*} [TopologicalSpace β] {f g : β → Completion α}
     (hf : Continuous f) (hg : Continuous g) : Continuous fun b => f b * g b :=
-  Continuous.comp continuous_mul (Continuous.prod_mk hf hg : _)
+  hf.mul hg
 
 instance ring : Ring (Completion α) :=
   { AddMonoidWithOne.unary, (inferInstanceAs (AddCommGroup (Completion α))),
       (inferInstanceAs (Mul (Completion α))), (inferInstanceAs (One (Completion α))) with
     zero_mul := fun a =>
       Completion.induction_on a
-        (isClosed_eq (Continuous.mul continuous_const continuous_id) continuous_const)
+        (isClosed_eq (continuous_const.mul continuous_id) continuous_const)
         fun a => by rw [← coe_zero, ← coe_mul, zero_mul]
     mul_zero := fun a =>
       Completion.induction_on a
-        (isClosed_eq (Continuous.mul continuous_id continuous_const) continuous_const)
+        (isClosed_eq (continuous_id.mul continuous_const) continuous_const)
         fun a => by rw [← coe_zero, ← coe_mul, mul_zero]
     one_mul := fun a =>
       Completion.induction_on a
-        (isClosed_eq (Continuous.mul continuous_const continuous_id) continuous_id) fun a => by
+        (isClosed_eq (continuous_const.mul continuous_id) continuous_id) fun a => by
         rw [← coe_one, ← coe_mul, one_mul]
     mul_one := fun a =>
       Completion.induction_on a
-        (isClosed_eq (Continuous.mul continuous_id continuous_const) continuous_id) fun a => by
+        (isClosed_eq (continuous_id.mul continuous_const) continuous_id) fun a => by
         rw [← coe_one, ← coe_mul, mul_one]
     mul_assoc := fun a b c =>
       Completion.induction_on₃ a b c
         (isClosed_eq
-          (Continuous.mul (Continuous.mul continuous_fst (continuous_fst.comp continuous_snd))
+          ((continuous_fst.mul (continuous_fst.comp continuous_snd)).mul
             (continuous_snd.comp continuous_snd))
-          (Continuous.mul continuous_fst
-            (Continuous.mul (continuous_fst.comp continuous_snd)
+          (continuous_fst.mul
+            ((continuous_fst.comp continuous_snd).mul
               (continuous_snd.comp continuous_snd))))
                 fun a b c => by rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
     left_distrib := fun a b c =>
       Completion.induction_on₃ a b c
         (isClosed_eq
-          (Continuous.mul continuous_fst
+          (continuous_fst.mul
             (Continuous.add (continuous_fst.comp continuous_snd)
               (continuous_snd.comp continuous_snd)))
-          (Continuous.add (Continuous.mul continuous_fst (continuous_fst.comp continuous_snd))
-            (Continuous.mul continuous_fst (continuous_snd.comp continuous_snd))))
+          (Continuous.add (continuous_fst.mul (continuous_fst.comp continuous_snd))
+            (continuous_fst.mul (continuous_snd.comp continuous_snd))))
         fun a b c => by rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
     right_distrib := fun a b c =>
       Completion.induction_on₃ a b c
         (isClosed_eq
-          (Continuous.mul (Continuous.add continuous_fst (continuous_fst.comp continuous_snd))
+          ((Continuous.add continuous_fst (continuous_fst.comp continuous_snd)).mul
             (continuous_snd.comp continuous_snd))
-          (Continuous.add (Continuous.mul continuous_fst (continuous_snd.comp continuous_snd))
-            (Continuous.mul (continuous_fst.comp continuous_snd)
+          (Continuous.add (continuous_fst.mul (continuous_snd.comp continuous_snd))
+            ((continuous_fst.comp continuous_snd).mul
               (continuous_snd.comp continuous_snd))))
         fun a b c => by rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_mul] }