chore: add a computable shortcut for AddCommMonoid ℂ and NonUnitalCommRing ℂ (leanprover-community#40163)

We already do this for the `Module` instance as of leanprover-community#29609.

Also adds some `delta%`s to very slightly reduce term size.

Author: eric-wieser

Mathlib/Analysis/Complex/Basic.lean

@@ -45,9 +45,13 @@ We also register the fact that `ℂ` is an `RCLike` field.
 
 assert_not_exists Absorbs
 
+namespace Complex
+
 /-- A shortcut instance to ensure computability; otherwise we get the noncomputable instance
 `Complex.instNormedField.toNormedModule.toModule`. -/
-instance Complex.instModuleSelf : Module ℂ ℂ := delta% inferInstance
+instance instModuleSelf : Module ℂ ℂ := delta% inferInstance
+
+end Complex
 
 noncomputable section
 

Mathlib/Data/Complex/Basic.lean

@@ -389,19 +389,34 @@ instance commRing : CommRing ℂ :=
     mul_one := by intros; ext <;> simp
     mul_comm := by intros; ext <;> simp <;> ring }
 
+section computable_shortcuts
+
 /-- This shortcut instance ensures we do not find `Ring` via the noncomputable `Complex.field`
 instance. -/
-instance : Ring ℂ := by infer_instance
+instance : Ring ℂ :=
+  delta% inferInstance
+
+/-- This shortcut instance ensures we do not find `NonUnitalCommRing` via the noncomputable
+`instCommCStarAlgebraComplex` instance. -/
+instance : NonUnitalCommRing ℂ :=
+  delta% inferInstance
 
 /-- This shortcut instance ensures we do not find `CommSemiring` via the noncomputable
 `Complex.field` instance. -/
 instance : CommSemiring ℂ :=
-  inferInstance
+  delta% inferInstance
 
 /-- This shortcut instance ensures we do not find `Semiring` via the noncomputable
 `Complex.field` instance. -/
 instance : Semiring ℂ :=
-  inferInstance
+  delta% inferInstance
+
+/-- This shortcut instance ensures we do not find `AddCommMonoid` via the noncomputable
+`Complex.instNormedField` instance. -/
+instance : AddCommMonoid ℂ :=
+  delta% inferInstance
+
+end computable_shortcuts
 
 /-- The "real part" map, considered as an additive group homomorphism. -/
 def reAddGroupHom : ℂ →+ ℝ where

MathlibTest/Instances/ComputableShortcuts.lean

@@ -0,0 +1,37 @@
+/-
+This test must import everything to make the noncomputable instances which we don't want available.
+-/
+import Mathlib
+
+/-!
+# Tests that basic algebraic typeclasses are computable
+
+Frequently mathlib will have instances of the form
+```
+instance : FooAndBar X := ...
+
+-- in a later file
+noncomputable instance : VeryNoncomputableFoo X := ...
+```
+which means that `Foo X` will sometimes be synthesized noncomputably even though a computable
+version is available.
+
+TODO: test this more exhaustively.
+-/
+
+macro "#guard_computable" t:term : command =>
+  `(#guard_msgs (drop info) in #eval $t)
+
+section Real
+
+#guard_computable LinearMap.mul ℝ ℝ 2 3
+#guard_computable LinearEquiv.neg ℝ (2 : ℝ)
+
+end Real
+
+section Complex
+
+#guard_computable LinearMap.mul ℂ ℂ 2 3
+#guard_computable LinearEquiv.neg ℂ (2 : ℂ)
+
+end Complex