chore (AlgebraicGeometry.StructureSheaf): clean up some instances (#7473

)

We replace a few `show X from inferInstance` with `inferInstanceAs` which reduces some `let_fun`'s in the resulting term. We also align the names with casing convention.

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -79,18 +79,18 @@ def Localizations (P : PrimeSpectrum.Top R) : Type u :=
 #align algebraic_geometry.structure_sheaf.localizations AlgebraicGeometry.StructureSheaf.Localizations
 
 -- Porting note : can't derive `CommRingCat`
-instance CommRingLocalizations (P : PrimeSpectrum.Top R) : CommRing <| Localizations R P :=
-  show CommRing <| Localization.AtPrime P.asIdeal from inferInstance
+instance commRingLocalizations (P : PrimeSpectrum.Top R) : CommRing <| Localizations R P :=
+  inferInstanceAs <| CommRing <| Localization.AtPrime P.asIdeal
 
 -- Porting note : can't derive `LocalRing`
-instance LocalRingLocalizations (P : PrimeSpectrum.Top R) : LocalRing <| Localizations R P :=
-  show LocalRing <| Localization.AtPrime P.asIdeal from inferInstance
+instance localRingLocalizations (P : PrimeSpectrum.Top R) : LocalRing <| Localizations R P :=
+  inferInstanceAs <| LocalRing <| Localization.AtPrime P.asIdeal
 
 instance (P : PrimeSpectrum.Top R) : Inhabited (Localizations R P) :=
   ⟨1⟩
 
 instance (U : Opens (PrimeSpectrum.Top R)) (x : U) : Algebra R (Localizations R x) :=
-  show Algebra R (Localization.AtPrime x.1.asIdeal) from inferInstance
+  inferInstanceAs <| Algebra R (Localization.AtPrime x.1.asIdeal)
 
 instance (U : Opens (PrimeSpectrum.Top R)) (x : U) :
     IsLocalization.AtPrime (Localizations R x) (x : PrimeSpectrum.Top R).asIdeal :=