perf: shortcut instances for Semiring (#39719)

This PR adds shortcut instances that make sure synthesis using `Semiring` doesn't go through the other ring-like classes. This matches the new definition of `Semiring`.

Author: JovanGerb

Mathlib/Algebra/Ring/Defs.lean

@@ -146,6 +146,12 @@ class Semiring (α : Type u) extends AddCommMonoid α, MonoidWithZero α, NonUni
 /-- A `Ring` is a `Semiring` with negation making it an additive group. -/
 class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
 
+-- Add some short-cut instances to avoid going through the less used ring type classes.
+instance [Semiring α] : Distrib α := inferInstance
+instance [Semiring α] : MulZeroClass α := inferInstance
+instance [Semiring α] : MulZeroOneClass α := inferInstance
+attribute [instance] Semiring.toMonoid
+
 /-!
 ### Semirings
 -/

Mathlib/Algebra/Ring/Ext.lean

@@ -339,8 +339,10 @@ theorem toNonUnitalRing_injective :
 
 theorem toNonAssocRing_injective :
     Function.Injective (@toNonAssocRing R) := by
-  intro _ _ _
-  ext <;> congr
+  intro _ _ h
+  ext x y
+  · exact congrArg (·.toAdd.add x y) h
+  · exact congrArg (·.toMul.mul x y) h
 
 theorem toSemiring_injective :
     Function.Injective (@toSemiring R) := by

Mathlib/Analysis/Quaternion.lean

@@ -32,7 +32,7 @@ The following notation is available with `open Quaternion` or `open scoped Quate
 quaternion, normed ring, normed space, normed algebra
 -/
 
-@[expose] public section
+@[expose] public noncomputable section
 
 
 @[inherit_doc] scoped[Quaternion] notation "ℍ" => Quaternion ℝ
@@ -50,7 +50,7 @@ theorem inner_self (a : ℍ) : ⟪a, a⟫ = normSq a :=
 theorem inner_def (a b : ℍ) : ⟪a, b⟫ = (a * star b).re :=
   rfl
 
-noncomputable instance : NormedAddCommGroup ℍ :=
+instance : NormedAddCommGroup ℍ :=
   @InnerProductSpace.Core.toNormedAddCommGroup ℝ ℍ _ _ _
     { toInner := inferInstance
       conj_inner_symm := fun x y => by simp [inner_def, mul_comm]
@@ -59,7 +59,7 @@ noncomputable instance : NormedAddCommGroup ℍ :=
       add_left := fun x y z => by simp only [inner_def, add_mul, re_add]
       smul_left := fun x y r => by simp [inner_def] }
 
-noncomputable instance : InnerProductSpace ℝ ℍ :=
+instance : InnerProductSpace ℝ ℍ :=
   InnerProductSpace.ofCore _
 
 theorem normSq_eq_norm_mul_self (a : ℍ) : normSq a = ‖a‖ * ‖a‖ := by
@@ -84,11 +84,11 @@ theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖ := by
 theorem nnnorm_star (a : ℍ) : ‖star a‖₊ = ‖a‖₊ :=
   Subtype.ext <| norm_star a
 
-noncomputable instance : NormedDivisionRing ℍ where
+instance : NormedDivisionRing ℍ where
   dist_eq _ _ := rfl
   norm_mul _ _ := by simp_rw [norm_eq_sqrt_real_inner, inner_self]; simp
 
-noncomputable instance : NormedAlgebra ℝ ℍ where
+instance : NormedAlgebra ℝ ℍ where
   norm_smul_le := norm_smul_le
   toAlgebra := Quaternion.algebra
 
@@ -139,7 +139,7 @@ theorem coeComplex_coe (r : ℝ) : ((r : ℂ) : ℍ) = r :=
   rfl
 
 /-- Coercion `ℂ →ₐ[ℝ] ℍ` as an algebra homomorphism. -/
-noncomputable def ofComplex : ℂ →ₐ[ℝ] ℍ where
+def ofComplex : ℂ →ₐ[ℝ] ℍ where
   toFun := (↑)
   map_one' := rfl
   map_zero' := rfl
@@ -159,7 +159,7 @@ lemma norm_toLp_equivTuple (x : ℍ) : ‖WithLp.toLp 2 (equivTuple ℝ x)‖ =
 
 /-- `QuaternionAlgebra.linearEquivTuple` as a `LinearIsometryEquiv`. -/
 @[simps apply symm_apply]
-noncomputable def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
+def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
   { (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (0 : ℝ) (-1 : ℝ)).trans
       (WithLp.linearEquiv 2 ℝ (Fin 4 → ℝ)).symm with
     toFun := fun a => !₂[a.1, a.2, a.3, a.4]

Mathlib/RingTheory/EuclideanDomain.lean

@@ -76,7 +76,7 @@ def gcdMonoid (R) [EuclideanDomain R] [DecidableEq R] : GCDMonoid R where
   gcd_dvd_left := gcd_dvd_left
   gcd_dvd_right := gcd_dvd_right
   dvd_gcd := dvd_gcd
-  gcd_mul_lcm a b := by rw [EuclideanDomain.gcd_mul_lcm]
+  gcd_mul_lcm a b := by rw [EuclideanDomain.gcd_mul_lcm]; rfl
   lcm_zero_left := lcm_zero_left
   lcm_zero_right := lcm_zero_right
 

Mathlib/Tactic/Ring/Basic.lean

@@ -357,8 +357,7 @@ theorem Nat.smul_eq_mul {n n' : ℕ} {r : R} (hr : n = r) (hn : n' = n) (a : R)
   subst_vars
   simp only [nsmul_eq_mul]
 
-omit [CommSemiring R] in
-theorem Int.smul_eq_mul {n n' : ℤ} {r : R} [CommRing R] (hr : n = r) (hn : n' = n) (a : R) :
+theorem Int.smul_eq_mul {R} {n n' : ℤ} {r : R} [CommRing R] (hr : n = r) (hn : n' = n) (a : R) :
     n' • a = r * a := by
   subst_vars
   simp only [zsmul_eq_mul]

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

@@ -317,10 +317,10 @@ theorem tprod_one_add [T2Space α] (h : Summable (∏ i ∈ ·, f i)) :
   HasProd.tprod_eq <| hasProd_one_add_of_hasSum_prod h.hasSum
 
 section Ordered
-variable [LinearOrder ι] [LocallyFiniteOrderBot ι] [T2Space α]
+variable [LinearOrder ι] [LocallyFiniteOrderBot ι]
 
 /-- The infinite version of `Finset.prod_one_add_ordered`. -/
-theorem tprod_one_add_ordered [ContinuousAdd α]
+theorem tprod_one_add_ordered [T2Space α] [ContinuousAdd α]
     (hsum : Summable fun i ↦ f i * ∏ j ∈ Iio i, (1 + f j))
     (hprod : Multipliable (1 + f ·)) :
     ∏' i, (1 + f i) = 1 + ∑' i, f i * ∏ j ∈ Iio i, (1 + f j) := by
@@ -339,9 +339,9 @@ theorem tprod_one_add_ordered [ContinuousAdd α]
   congr
   grind
 
-omit [CommSemiring α] in
 /-- The infinite version of `Finset.prod_one_sub_ordered`. -/
-theorem tprod_one_sub_ordered [CommRing α] [IsTopologicalAddGroup α]
+theorem tprod_one_sub_ordered {α : Type*} {f : ι → α}
+    [CommRing α] [TopologicalSpace α] [T2Space α] [IsTopologicalAddGroup α]
     (hsum : Summable fun i ↦ f i * ∏ j ∈ Iio i, (1 - f j))
     (hprod : Multipliable (1 - f ·)) :
     ∏' i, (1 - f i) = 1 - ∑' i, f i * ∏ j ∈ Iio i, (1 - f j) := by

MathlibTest/hintAll.lean

@@ -203,9 +203,6 @@ info: Try these:
   [apply] norm_num
   Remaining subgoals:
   ⊢ a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁
-  [apply] ring_nf
-  Remaining subgoals:
-  ⊢ a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁
   [apply] abel_nf
   Remaining subgoals:
   ⊢ a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁