chore: avoid dsimp; infer_instance (leanprover-community#37288)

This PR cleans up a bunch of instances using `inferInstanceAs` and `deriving`.

It seems that when in a `noncomputable section`, derived instances will always be `noncomputable`, while manual instances can still end up being computable. So this PR also adds some now transitively required `noncomputable` annotations.

Author: JovanGerb

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -539,12 +539,9 @@ section
 
 variable {A : AddCommGrpCat} (φ : R →+* End A)
 
-instance : AddCommGroup (mkOfSMul' φ) := by
-  dsimp only [mkOfSMul']
-  infer_instance
+instance : AddCommGroup (mkOfSMul' φ) :=
+  inferInstanceAs <| AddCommGroup A
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : SMul R (mkOfSMul' φ) := ⟨fun r (x : A) => (show A ⟶ A from φ r) x⟩
 
 @[simp]

Mathlib/Algebra/Category/MonCat/Colimits.lean

@@ -118,10 +118,7 @@ instance colimitSetoid : Setoid (Prequotient F) where
 -/
 def ColimitType : Type v :=
   Quotient (colimitSetoid F)
-
-instance : Inhabited (ColimitType F) := by
-  dsimp [ColimitType]
-  infer_instance
+deriving Inhabited
 
 instance monoidColimitType : Monoid (ColimitType F) where
   one := Quotient.mk _ one

Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

@@ -58,7 +58,7 @@ instance should be obtained at the beginning of the proof, using the term
 
 -/
 
-@[expose] public section
+@[expose] public noncomputable section
 
 assert_not_exists TwoSidedIdeal
 
@@ -85,13 +85,10 @@ variable [HasDerivedCategory.{w} C]
 
 /-- The derived category of an abelian category. -/
 def DerivedCategory : Type (max u v) := HomologicalComplexUpToQuasiIso C (ComplexShape.up ℤ)
+deriving Category
 
 namespace DerivedCategory
 
-instance : Category.{w} (DerivedCategory C) := by
-  dsimp [DerivedCategory]
-  infer_instance
-
 variable {C}
 
 /-- The localization functor `CochainComplex C ℤ ⥤ DerivedCategory C`. -/
@@ -127,7 +124,7 @@ instance : Qh.IsLocalization (HomotopyCategory.subcategoryAcyclic C).trW := by
   rw [← HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W]
   infer_instance
 
-noncomputable instance : Preadditive (DerivedCategory C) :=
+instance : Preadditive (DerivedCategory C) :=
   Localization.preadditive Qh (HomotopyCategory.subcategoryAcyclic C).trW
 
 instance : (Qh (C := C)).Additive :=
@@ -136,16 +133,16 @@ instance : (Qh (C := C)).Additive :=
 instance : (Q (C := C)).Additive :=
   Functor.additive_of_iso (quotientCompQhIso C)
 
-noncomputable instance : HasZeroObject (DerivedCategory C) :=
+instance : HasZeroObject (DerivedCategory C) :=
   Q.hasZeroObject_of_additive
 
-noncomputable instance : HasShift (DerivedCategory C) ℤ :=
+instance : HasShift (DerivedCategory C) ℤ :=
   HasShift.localized Qh (HomotopyCategory.subcategoryAcyclic C).trW ℤ
 
-noncomputable instance : (Qh (C := C)).CommShift ℤ :=
+instance : (Qh (C := C)).CommShift ℤ :=
   Functor.CommShift.localized Qh (HomotopyCategory.subcategoryAcyclic C).trW ℤ
 
-noncomputable instance : (Q (C := C)).CommShift ℤ :=
+instance : (Q (C := C)).CommShift ℤ :=
   Functor.CommShift.ofIso (quotientCompQhIso C) ℤ
 
 instance : NatTrans.CommShift (quotientCompQhIso C).hom ℤ :=
@@ -156,15 +153,15 @@ instance (n : ℤ) : (shiftFunctor (DerivedCategory C) n).Additive := by
     Qh (HomotopyCategory.subcategoryAcyclic C).trW]
   exact Functor.additive_of_iso (Qh.commShiftIso n)
 
-noncomputable instance : Pretriangulated (DerivedCategory C) :=
+instance : Pretriangulated (DerivedCategory C) :=
   Triangulated.Localization.pretriangulated
     Qh (HomotopyCategory.subcategoryAcyclic C).trW
 
 instance : (Qh (C := C)).IsTriangulated :=
   Triangulated.Localization.isTriangulated_functor
     Qh (HomotopyCategory.subcategoryAcyclic C).trW
 
-noncomputable instance : IsTriangulated (DerivedCategory C) :=
+instance : IsTriangulated (DerivedCategory C) :=
   Triangulated.Localization.isTriangulated
     Qh (HomotopyCategory.subcategoryAcyclic C).trW
 
@@ -223,12 +220,12 @@ end
 
 /-- The single functors `C ⥤ DerivedCategory C` for all `n : ℤ` along with
 their compatibilities with shifts. -/
-noncomputable def singleFunctors : SingleFunctors C (DerivedCategory C) ℤ :=
+def singleFunctors : SingleFunctors C (DerivedCategory C) ℤ :=
   (HomotopyCategory.singleFunctors C).postcomp Qh
 
 /-- The shift functor `C ⥤ DerivedCategory C` which sends `X : C` to the
 single cochain complex with `X` sitting in degree `n : ℤ`. -/
-noncomputable abbrev singleFunctor (n : ℤ) := (singleFunctors C).functor n
+abbrev singleFunctor (n : ℤ) := (singleFunctors C).functor n
 
 instance (n : ℤ) : (singleFunctor C n).Additive := by
   dsimp [singleFunctor, singleFunctors]
@@ -242,13 +239,13 @@ instance (n : ℤ) : (singleFunctor C n).Additive := by
 /-- The isomorphism
 `DerivedCategory.singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh` given
 by the definition of `DerivedCategory.singleFunctors`. -/
-noncomputable def singleFunctorsPostcompQhIso :
+def singleFunctorsPostcompQhIso :
     singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh :=
   Iso.refl _
 
 /-- The isomorphism
 `DerivedCategory.singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q`. -/
-noncomputable def singleFunctorsPostcompQIso :
+def singleFunctorsPostcompQIso :
     singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q :=
   (SingleFunctors.postcompFunctor C ℤ (Qh : _ ⥤ DerivedCategory C)).mapIso
     (HomotopyCategory.singleFunctorsPostcompQuotientIso C) ≪≫
@@ -273,7 +270,7 @@ lemma singleFunctorsPostcompQIso_inv_hom (n : ℤ) :
   rfl
 
 /-- The isomorphism `singleFunctor C n ≅ CochainComplex.singleFunctor C n ⋙ Q`. -/
-noncomputable def singleFunctorIsoCompQ (n : ℤ) :
+def singleFunctorIsoCompQ (n : ℤ) :
     singleFunctor C n ≅ CochainComplex.singleFunctor C n ⋙ Q := Iso.refl _
 
 lemma isIso_Q_map_iff_quasiIso {K L : CochainComplex C ℤ} (φ : K ⟶ L) :

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -66,15 +66,10 @@ variable (F G)
 of a family of morphisms `F.X p ⟶ G.X q` whenever `p + n = q`, i.e. for all
 triplets in `HomComplex.Triplet n`. -/
 def Cochain := ∀ (T : Triplet n), F.X T.p ⟶ G.X T.q
+deriving AddCommGroup
 
-instance : AddCommGroup (Cochain F G n) := by
-  dsimp only [Cochain]
-  infer_instance
-
-set_option backward.isDefEq.respectTransparency false in
-instance : Module R (Cochain F G n) := by
-  dsimp only [Cochain]
-  infer_instance
+instance : Module R (Cochain F G n) :=
+  inferInstanceAs <| Module R (∀ _, _)
 
 namespace Cochain
 

Mathlib/Algebra/Module/Presentation/Basic.lean

@@ -38,7 +38,7 @@ generators and relations.
 
 -/
 
-@[expose] public section
+@[expose] public noncomputable section
 
 assert_not_exists Cardinal
 
@@ -68,16 +68,10 @@ variable {A} (relations : Relations.{w₀, w₁} A)
 This is the quotient of the free `A`-module on `relations.G` by the submodule generated by
 the given relations. -/
 def Quotient := (relations.G →₀ A) ⧸ Submodule.span A (Set.range relations.relation)
-
-noncomputable instance : AddCommGroup relations.Quotient := by
-  dsimp only [Quotient]; infer_instance
-
-set_option backward.isDefEq.respectTransparency false in
-noncomputable instance : Module A relations.Quotient := by
-  dsimp only [Quotient]; infer_instance
+deriving AddCommGroup, Module A
 
 /-- The canonical (surjective) linear map `(relations.G →₀ A) →ₗ[A] relations.Quotient`. -/
-noncomputable def toQuotient : (relations.G →₀ A) →ₗ[A] relations.Quotient := Submodule.mkQ _
+def toQuotient : (relations.G →₀ A) →ₗ[A] relations.Quotient := Submodule.mkQ _
 
 variable {relations} in
 @[ext]
@@ -105,7 +99,7 @@ lemma toQuotient_relation (r : relations.R) :
 
 /-- The linear map `(relations.R →₀ A) →ₗ[A] (relations.G →₀ A)` corresponding to the relations
 given by `relations : Relations A`. -/
-noncomputable def map : (relations.R →₀ A) →ₗ[A] (relations.G →₀ A) :=
+def map : (relations.R →₀ A) →ₗ[A] (relations.G →₀ A) :=
   Finsupp.linearCombination _ relations.relation
 
 @[simp]
@@ -146,7 +140,7 @@ variable (solution : relations.Solution M)
 
 /-- Given `relations : Relations A` and a solution in `relations.Solution M`, this is
 the linear map `(relations.G →₀ A) →ₗ[A] M` canonically associated to the solution. -/
-noncomputable def π : (relations.G →₀ A) →ₗ[A] M := Finsupp.linearCombination _ solution.var
+def π : (relations.G →₀ A) →ₗ[A] M := Finsupp.linearCombination _ solution.var
 
 @[simp]
 lemma π_single (g : relations.G) :
@@ -175,7 +169,7 @@ lemma span_relation_le_ker_π :
 
 /-- Given `relations : Relations A` and `solution : relations.Solution M`, this is
 the canonical linear map `relations.Quotient →ₗ[A] M` from the module. -/
-noncomputable def fromQuotient : relations.Quotient →ₗ[A] M :=
+def fromQuotient : relations.Quotient →ₗ[A] M :=
   Submodule.liftQ _ solution.π solution.span_relation_le_ker_π
 
 @[simp]
@@ -222,7 +216,7 @@ for `relations.Solution M` for which the data is given as
 a linear map `π : (relations.G →₀ A) →ₗ[A] M`. (See also `ofπ'` for an alternate
 vanishing criterion.) -/
 @[simps -isSimp]
-noncomputable def ofπ : relations.Solution M where
+def ofπ : relations.Solution M where
   var g := π (Finsupp.single g 1)
   linearCombination_var_relation r := by
     have : π = Finsupp.linearCombination _ (fun g ↦ π (Finsupp.single g 1)) := by ext; simp
@@ -241,7 +235,7 @@ variable (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π.comp relations.map
 /-- Variant of `ofπ` where the vanishing condition is expressed in terms
 of a composition of linear maps. -/
 @[simps! -isSimp]
-noncomputable def ofπ' : relations.Solution M :=
+def ofπ' : relations.Solution M :=
   ofπ π (fun r ↦ by
     simpa using DFunLike.congr_fun hπ (Finsupp.single r 1))
 
@@ -298,7 +292,7 @@ include h
 /-- When `M` admits a presentation by generators and relations given
 by `solution : relations.Solutions M`, this is the associated linear equivalence
 `relations.Quotient ≃ₗ[A] M`. -/
-noncomputable def linearEquiv : relations.Quotient ≃ₗ[A] M := LinearEquiv.ofBijective _ h.bijective
+def linearEquiv : relations.Quotient ≃ₗ[A] M := LinearEquiv.ofBijective _ h.bijective
 
 @[simp]
 lemma linearEquiv_apply (x : relations.Quotient) :
@@ -324,7 +318,7 @@ variable {N : Type v'} [AddCommGroup N] [Module A N]
 
 /-- If `M` admits a presentation by generators and relations, and we have a solution of the
 same equations in a module `N`, then this is the canonical induced linear map `M →ₗ[A] N`. -/
-noncomputable def desc (s : relations.Solution N) : M →ₗ[A] N :=
+def desc (s : relations.Solution N) : M →ₗ[A] N :=
   s.fromQuotient.comp h.linearEquiv.symm.toLinearMap
 
 @[simp]
@@ -358,7 +352,7 @@ lemma postcomp_injective {f f' : M →ₗ[A] N}
 linear maps from `M` can be (naturally) identified to the solutions of
 certain linear equations. -/
 @[simps]
-noncomputable def linearMapEquiv : (M →ₗ[A] N) ≃ relations.Solution N where
+def linearMapEquiv : (M →ₗ[A] N) ≃ relations.Solution N where
   toFun f := solution.postcomp f
   invFun s := h.desc s
   left_inv f := h.postcomp_injective (by simp)
@@ -370,7 +364,7 @@ variable {solution' : relations.Solution N} (h' : solution'.IsPresentation)
 
 /-- Uniqueness (up to a unique linear equivalence) of the module defined
 by generators and relations. -/
-noncomputable def uniq : M ≃ₗ[A] N := LinearEquiv.ofLinear
+def uniq : M ≃ₗ[A] N := LinearEquiv.ofLinear
   (h.desc solution') (h'.desc solution)
     (h'.postcomp_injective (by simp))
     (h.postcomp_injective (by simp))
@@ -407,7 +401,7 @@ variable (relations)
 /-- Given `relations : Relations A`, this is the obvious solution to `relations`
 in the quotient `relations.Quotient`. -/
 @[simps!]
-noncomputable def ofQuotient : relations.Solution relations.Quotient :=
+def ofQuotient : relations.Solution relations.Quotient :=
   ofπ relations.toQuotient (by simp)
 
 @[simp]

Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

@@ -395,9 +395,8 @@ def Augmented :=
   Comma (𝟭 (SimplicialObject C)) (const C)
 
 @[simps!]
-instance : Category (Augmented C) := by
-  dsimp only [Augmented]
-  infer_instance
+instance : Category (Augmented C) :=
+  inferInstanceAs <| Category (Comma _ _)
 
 variable {C}
 
@@ -692,10 +691,7 @@ def whiskering (D : Type*) [Category* D] : (C ⥤ D) ⥤ CosimplicialObject C 
 /-- Truncated cosimplicial objects. -/
 def Truncated (n : ℕ) :=
   SimplexCategory.Truncated n ⥤ C
-
-instance {n : ℕ} : Category (Truncated C n) := by
-  dsimp [Truncated]
-  infer_instance
+deriving Category
 
 variable {C}
 
@@ -772,9 +768,8 @@ def Augmented :=
   Comma (const C) (𝟭 (CosimplicialObject C))
 
 @[simps!]
-instance : Category (Augmented C) := by
-  dsimp only [Augmented]
-  infer_instance
+instance : Category (Augmented C) :=
+  inferInstanceAs <| Category (Comma _ _)
 
 variable {C}
 

Mathlib/CategoryTheory/Action.lean

@@ -47,10 +47,7 @@ from x to y is a scalar taking x to y. Due to implementation details, the object
 of this category is not equal to X, but is in bijection with X. -/
 def ActionCategory :=
   (actionAsFunctor M X).Elements
-
-instance : Category (ActionCategory M X) := by
-  dsimp only [ActionCategory]
-  infer_instance
+deriving Category
 
 namespace ActionCategory
 

Mathlib/CategoryTheory/Action/Monoidal.lean

@@ -125,8 +125,8 @@ instance FunctorCategoryEquivalence.functorMonoidal :
     (Action.functorCategoryEquivalence V G).symm).inverse.Monoidal
 
 instance functorCategoryEquivalenceFunctorMonoidal :
-    (functorCategoryEquivalence V G).functor.Monoidal := by
-  dsimp only [functorCategoryEquivalence_functor]; infer_instance
+    (functorCategoryEquivalence V G).functor.Monoidal :=
+  inferInstanceAs FunctorCategoryEquivalence.functor.Monoidal
 
 /-- Upgrading the functor `(SingleObj G ⥤ V) ⥤ Action V G` to a monoidal functor. -/
 instance FunctorCategoryEquivalence.inverseMonoidal :
@@ -135,8 +135,8 @@ instance FunctorCategoryEquivalence.inverseMonoidal :
     (Action.functorCategoryEquivalence V G).symm).functor.Monoidal
 
 instance functorCategoryEquivalenceInverseMonoidal :
-    (functorCategoryEquivalence V G).inverse.Monoidal := by
-  dsimp only [functorCategoryEquivalence_inverse]; infer_instance
+    (functorCategoryEquivalence V G).inverse.Monoidal :=
+  inferInstanceAs FunctorCategoryEquivalence.inverse.Monoidal
 
 @[simp]
 lemma FunctorCategoryEquivalence.functor_ε :

Mathlib/CategoryTheory/Linear/Basic.lean

@@ -79,10 +79,8 @@ section End
 
 variable {R : Type w}
 
-set_option backward.isDefEq.respectTransparency false in
-instance [Semiring R] [Linear R C] (X : C) : Module R (End X) := by
-  dsimp [End]
-  infer_instance
+instance [Semiring R] [Linear R C] (X : C) : Module R (End X) :=
+  inferInstanceAs <| Module R (X ⟶ X)
 
 instance [CommSemiring R] [Linear R C] (X : C) : Algebra R (End X) :=
   Algebra.ofModule (fun _ _ _ => comp_smul _ _ _ _ _ _) fun _ _ _ => smul_comp _ _ _ _ _ _

Mathlib/CategoryTheory/Localization/Construction.lean

@@ -96,10 +96,7 @@ open Localization.Construction
 in `W : MorphismProperty C` -/
 def Localization :=
   CategoryTheory.Quotient (Localization.Construction.relations W)
-
-instance : Category (Localization W) := by
-  dsimp only [Localization]
-  infer_instance
+deriving Category
 
 /-- The obvious functor `C ⥤ W.Localization` -/
 def Q : C ⥤ W.Localization where