chore: use inferInstanceAs in analysis (leanprover-community#37272)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Analysis/CStarAlgebra/Basic.lean

@@ -312,9 +312,9 @@ end starₗᵢ
 
 namespace StarSubalgebra
 
-instance toNormedAlgebra {𝕜 A : Type*} [NormedField 𝕜] [StarRing 𝕜] [SeminormedRing A] [StarRing A]
-    [NormedAlgebra 𝕜 A] [StarModule 𝕜 A] (S : StarSubalgebra 𝕜 A) : NormedAlgebra 𝕜 S :=
-  NormedAlgebra.induced 𝕜 S A S.subtype
+example {𝕜 A : Type*} [NormedField 𝕜] [StarRing 𝕜] [SeminormedRing A] [StarRing A]
+    [NormedAlgebra 𝕜 A] [StarModule 𝕜 A] (S : StarSubalgebra 𝕜 A) :
+    NormedAlgebra 𝕜 S := by infer_instance
 
 instance to_cstarRing {R A} [CommRing R] [StarRing R] [NormedRing A] [StarRing A] [CStarRing A]
     [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) : CStarRing S where

Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

@@ -725,7 +725,8 @@ instance instUniformSpace : UniformSpace (CStarMatrix m n A) :=
   inferInstanceAs <| UniformSpace (Matrix m n A)
 
 -- TODO: we are missing `Bornology (Matrix m n A)`
-instance instBornology : Bornology (CStarMatrix m n A) := Pi.instBornology
+instance instBornology : Bornology (CStarMatrix m n A) :=
+  inferInstanceAs <| Bornology (m → n → A)
 
 instance instCompleteSpace : CompleteSpace (CStarMatrix m n A) :=
   inferInstanceAs <| CompleteSpace (Matrix m n A)

Mathlib/Analysis/Normed/Field/UnitBall.lean

@@ -36,15 +36,15 @@ def Subsemigroup.unitBall (𝕜 : Type*) [NonUnitalSeminormedRing 𝕜] : Subsem
     exact (norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)
 
 instance Metric.unitBall.instSemigroup [NonUnitalSeminormedRing 𝕜] : Semigroup (ball (0 : 𝕜) 1) :=
-  MulMemClass.toSemigroup (Subsemigroup.unitBall 𝕜)
+  inferInstanceAs <| Semigroup (Subsemigroup.unitBall 𝕜)
 
 instance Metric.unitBall.instContinuousMul [NonUnitalSeminormedRing 𝕜] :
     ContinuousMul (ball (0 : 𝕜) 1) :=
   (Subsemigroup.unitBall 𝕜).continuousMul
 
 instance Metric.unitBall.instCommSemigroup [SeminormedCommRing 𝕜] :
     CommSemigroup (ball (0 : 𝕜) 1) :=
-  MulMemClass.toCommSemigroup (Subsemigroup.unitBall 𝕜)
+  inferInstanceAs <| CommSemigroup (Subsemigroup.unitBall 𝕜)
 
 instance Metric.unitBall.instHasDistribNeg [NonUnitalSeminormedRing 𝕜] :
     HasDistribNeg (ball (0 : 𝕜) 1) :=
@@ -97,7 +97,7 @@ def Subsemigroup.unitClosedBall (𝕜 : Type*) [NonUnitalSeminormedRing 𝕜] :
 
 instance Metric.unitClosedBall.instSemigroup [NonUnitalSeminormedRing 𝕜] :
     Semigroup (closedBall (0 : 𝕜) 1) :=
-  MulMemClass.toSemigroup (Subsemigroup.unitClosedBall 𝕜)
+  inferInstanceAs <| Semigroup (Subsemigroup.unitClosedBall 𝕜)
 
 instance Metric.unitClosedBall.instHasDistribNeg [NonUnitalSeminormedRing 𝕜] :
     HasDistribNeg (closedBall (0 : 𝕜) 1) :=
@@ -139,11 +139,11 @@ def Submonoid.unitClosedBall (𝕜 : Type*) [SeminormedRing 𝕜] [NormOneClass
 
 instance Metric.unitClosedBall.instMonoid [SeminormedRing 𝕜] [NormOneClass 𝕜] :
     Monoid (closedBall (0 : 𝕜) 1) :=
-  SubmonoidClass.toMonoid (Submonoid.unitClosedBall 𝕜)
+  inferInstanceAs <| Monoid (Submonoid.unitClosedBall 𝕜)
 
 instance Metric.unitClosedBall.instCommMonoid [SeminormedCommRing 𝕜] [NormOneClass 𝕜] :
     CommMonoid (closedBall (0 : 𝕜) 1) :=
-  SubmonoidClass.toCommMonoid (Submonoid.unitClosedBall 𝕜)
+  inferInstanceAs <| CommMonoid (Submonoid.unitClosedBall 𝕜)
 
 @[simp, norm_cast]
 protected theorem Metric.unitClosedBall.coe_one [SeminormedRing 𝕜] [NormOneClass 𝕜] :
@@ -211,11 +211,11 @@ theorem Metric.unitSphere.coe_zpow [NormedDivisionRing 𝕜] (x : sphere (0 : 
 
 instance Metric.unitSphere.instMonoid [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
     Monoid (sphere (0 : 𝕜) 1) :=
-  SubmonoidClass.toMonoid (Submonoid.unitSphere 𝕜)
+  inferInstanceAs <| Monoid (Submonoid.unitSphere 𝕜)
 
 instance Metric.unitSphere.instCommMonoid [SeminormedCommRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
     CommMonoid (sphere (0 : 𝕜) 1) :=
-  SubmonoidClass.toCommMonoid (Submonoid.unitSphere 𝕜)
+  inferInstanceAs <| CommMonoid (Submonoid.unitSphere 𝕜)
 
 @[simp, norm_cast]
 protected theorem Metric.unitSphere.coe_one [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
@@ -247,7 +247,7 @@ theorem unitSphereToUnits_injective [NormedDivisionRing 𝕜] :
   Subtype.ext <| by convert congr_arg Units.val h
 
 instance Metric.unitSphere.instGroup [NormedDivisionRing 𝕜] : Group (sphere (0 : 𝕜) 1) :=
-  unitSphereToUnits_injective.group (unitSphereToUnits 𝕜) (Units.ext rfl)
+  fast_instance% unitSphereToUnits_injective.group (unitSphereToUnits 𝕜) (Units.ext rfl)
     (fun _x _y => Units.ext rfl)
     (fun _x => Units.ext rfl) (fun _x _y => Units.ext <| div_eq_mul_inv _ _)
     (fun x n => Units.ext (Units.val_pow_eq_pow_val (unitSphereToUnits 𝕜 x) n).symm) fun x n =>

Mathlib/Analysis/Normed/Lp/lpSpace.lean

@@ -792,7 +792,7 @@ def _root_.lpInftySubring : Subring (PreLp B) :=
     mul_mem' := Memℓp.infty_mul }
 
 instance inftyRing : Ring (lp B ∞) :=
-  (lpInftySubring B).toRing
+  inferInstanceAs <| Ring (lpInftySubring B)
 
 theorem _root_.Memℓp.infty_pow {f : ∀ i, B i} (hf : Memℓp f ∞) (n : ℕ) : Memℓp (f ^ n) ∞ :=
   (lpInftySubring B).pow_mem hf n
@@ -841,12 +841,8 @@ section Algebra
 variable {I : Type*} {B : I → Type*}
 variable [NormedField 𝕜] [∀ i, NormedRing (B i)] [∀ i, NormedAlgebra 𝕜 (B i)]
 
-/-- A variant of `Pi.algebra` that lean can't find otherwise. -/
-instance _root_.Pi.algebraOfNormedAlgebra : Algebra 𝕜 (∀ i, B i) :=
-  @Pi.algebra I 𝕜 B _ _ fun _ => NormedAlgebra.toAlgebra
-
 instance _root_.PreLp.algebra : Algebra 𝕜 (PreLp B) :=
-  Pi.algebraOfNormedAlgebra
+  inferInstanceAs <| Algebra 𝕜 (∀ i, B i)
 
 variable [∀ i, NormOneClass (B i)]
 
@@ -865,8 +861,10 @@ def _root_.lpInftySubalgebra : Subalgebra 𝕜 (PreLp B) :=
 
 variable {𝕜 B}
 
-instance inftyNormedAlgebra : NormedAlgebra 𝕜 (lp B ∞) :=
-  { (lpInftySubalgebra 𝕜 B).algebra, (lp.instNormedSpace : NormedSpace 𝕜 (lp B ∞)) with }
+instance : Algebra 𝕜 (lp B ∞) := inferInstanceAs <| Algebra 𝕜 (lpInftySubalgebra 𝕜 B)
+
+instance inftyNormedAlgebra : NormedAlgebra 𝕜 (lp B ∞) where
+  norm_smul_le := norm_smul_le
 
 end Algebra
 

Mathlib/Analysis/Normed/Module/Basic.lean

@@ -402,7 +402,7 @@ abbrev NormedAlgebra.induced {F : Type*} (𝕜 R S : Type*) [NormedField 𝕜] [
 
 instance Subalgebra.toNormedAlgebra {𝕜 A : Type*} [SeminormedRing A] [NormedField 𝕜]
     [NormedAlgebra 𝕜 A] (S : Subalgebra 𝕜 A) : NormedAlgebra 𝕜 S :=
-  NormedAlgebra.induced 𝕜 S A S.val
+  fast_instance% NormedAlgebra.induced 𝕜 S A S.val
 
 section SubalgebraClass
 
@@ -490,7 +490,7 @@ theorem NormedSpace.restrictScalars_eq {E : Type*} [SeminormedAddCommGroup E]
 /-- If `E` is a normed space over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
 `RestrictScalars.module` is additionally a `NormedSpace`. -/
 instance RestrictScalars.normedSpace : NormedSpace 𝕜 (RestrictScalars 𝕜 𝕜' E) :=
-  NormedSpace.restrictScalars 𝕜 𝕜' E
+  fast_instance% NormedSpace.restrictScalars 𝕜 𝕜' E
 
 -- If you think you need this, consider instead reproducing `RestrictScalars.lsmul`
 -- appropriately modified here.
@@ -526,7 +526,7 @@ def NormedAlgebra.restrictScalars : NormedAlgebra 𝕜 E :=
 /-- If `E` is a normed algebra over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
 `RestrictScalars.module` is additionally a `NormedAlgebra`. -/
 instance RestrictScalars.normedAlgebra : NormedAlgebra 𝕜 (RestrictScalars 𝕜 𝕜' E) :=
-  NormedAlgebra.restrictScalars 𝕜 𝕜' E
+  fast_instance% NormedAlgebra.restrictScalars 𝕜 𝕜' E
 
 -- If you think you need this, consider instead reproducing `RestrictScalars.lsmul`
 -- appropriately modified here.