chore: no noncomputable inside noncomputable section

Mathlib/Algebra/Category/AlgCat/Monoidal.lean

@@ -34,12 +34,12 @@ open scoped TensorProduct
 /-- Auxiliary definition used to fight a timeout when building
 `AlgCat.instMonoidalCategory`. -/
 @[simps!]
-noncomputable abbrev tensorObj (X Y : AlgCat.{u} R) : AlgCat.{u} R :=
+abbrev tensorObj (X Y : AlgCat.{u} R) : AlgCat.{u} R :=
   of R (X ⊗[R] Y)
 
 /-- Auxiliary definition used to fight a timeout when building
 `AlgCat.instMonoidalCategory`. -/
-noncomputable abbrev tensorHom {W X Y Z : AlgCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z) :
+abbrev tensorHom {W X Y Z : AlgCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z) :
     tensorObj W Y ⟶ tensorObj X Z :=
   ofHom <| Algebra.TensorProduct.map f.hom g.hom
 
@@ -93,7 +93,7 @@ theorem hom_inv_associator {M N K : AlgCat.{u} R} :
     (α_ M N K).inv.hom = (Algebra.TensorProduct.assoc R R R M N K).symm.toAlgHom :=
   rfl
 
-noncomputable instance instMonoidalCategory : MonoidalCategory (AlgCat.{u} R) :=
+instance instMonoidalCategory : MonoidalCategory (AlgCat.{u} R) :=
   Monoidal.induced
     (forget₂ (AlgCat R) (ModuleCat R))
     { μIso := fun _ _ => Iso.refl _

Mathlib/Algebra/Category/Grp/EpiMono.lean

@@ -148,7 +148,7 @@ instance : DecidableEq X' :=
 
 /-- Let `τ` be the permutation on `X'` exchanging `f.hom.range` and the point at infinity.
 -/
-noncomputable def tau : SX' :=
+def tau : SX' :=
   Equiv.swap (fromCoset ⟨↑f.hom.range, ⟨1, one_leftCoset _⟩⟩) ∞
 
 local notation "τ" => tau f

Mathlib/Algebra/Category/Grp/FilteredColimits.lean

@@ -48,7 +48,7 @@ In the following, we will show that this has the structure of a group.
 @[to_additive
   /-- The colimit of `F ⋙ forget₂ AddGrpCat AddMonCat` in the category `AddMonCat`.
   In the following, we will show that this has the structure of an additive group. -/]
-noncomputable abbrev G : MonCat :=
+abbrev G : MonCat :=
   MonCat.FilteredColimits.colimit.{v, u} (F ⋙ forget₂ GrpCat MonCat.{max v u})
 
 /-- The canonical projection into the colimit, as a quotient type. -/
@@ -109,7 +109,7 @@ theorem colimit_inv_mk_eq (x : Σ j, F.obj j) : (G.mk.{v, u} F x)⁻¹ = G.mk F
   rfl
 
 @[to_additive]
-noncomputable instance colimitGroup : Group (G.{v, u} F) :=
+instance colimitGroup : Group (G.{v, u} F) :=
   { colimitInv.{v, u} F, (G.{v, u} F).str with
     inv_mul_cancel := fun x => by
       refine Quot.inductionOn x ?_; clear x; intro x
@@ -120,12 +120,12 @@ noncomputable instance colimitGroup : Group (G.{v, u} F) :=
 
 /-- The bundled group giving the filtered colimit of a diagram. -/
 @[to_additive /-- The bundled additive group giving the filtered colimit of a diagram. -/]
-noncomputable def colimit : GrpCat.{max v u} :=
+def colimit : GrpCat.{max v u} :=
   GrpCat.of (G.{v, u} F)
 
 /-- The cocone over the proposed colimit group. -/
 @[to_additive /-- The cocone over the proposed colimit additive group. -/]
-noncomputable def colimitCocone : Cocone F where
+def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι.app J := GrpCat.ofHom ((MonCat.FilteredColimits.colimitCocone
     (F ⋙ forget₂ GrpCat MonCat)).ι.app J).hom
@@ -134,20 +134,20 @@ noncomputable def colimitCocone : Cocone F where
 
 /-- The proposed colimit cocone is a colimit in `GrpCat`. -/
 @[to_additive /-- The proposed colimit cocone is a colimit in `AddGroup`. -/]
-noncomputable def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) :=
+def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) :=
   isColimitOfReflects (forget₂ _ MonCat)
     (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ GrpCat MonCat))
 
 @[to_additive forget₂AddMon_preservesFilteredColimits]
-noncomputable instance forget₂Mon_preservesFilteredColimits :
+instance forget₂Mon_preservesFilteredColimits :
     PreservesFilteredColimits.{u} (forget₂ GrpCat.{u} MonCat.{u}) where
       preserves_filtered_colimits x hx1 _ :=
       letI : Category.{u, u} x := hx1
       ⟨fun {F} => preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F)
           (MonCat.FilteredColimits.colimitCoconeIsColimit.{u, u} _)⟩
 
 @[to_additive]
-noncomputable instance forget_preservesFilteredColimits :
+instance forget_preservesFilteredColimits :
     PreservesFilteredColimits (forget GrpCat.{u}) :=
   Limits.comp_preservesFilteredColimits (forget₂ GrpCat MonCat) (forget MonCat.{u})
 
@@ -169,24 +169,24 @@ In the following, we will show that this has the structure of a _commutative_ gr
 @[to_additive
   /-- The colimit of `F ⋙ forget₂ AddCommGrpCat AddGrpCat` in the category `AddGrpCat`.
   In the following, we will show that this has the structure of a _commutative_ additive group. -/]
-noncomputable abbrev G : GrpCat.{max v u} :=
+abbrev G : GrpCat.{max v u} :=
   GrpCat.FilteredColimits.colimit.{v, u} (F ⋙ forget₂ CommGrpCat.{max v u} GrpCat.{max v u})
 
 @[to_additive]
-noncomputable instance colimitCommGroup : CommGroup.{max v u} (G.{v, u} F) :=
+instance colimitCommGroup : CommGroup.{max v u} (G.{v, u} F) :=
   { (G F).str,
     CommMonCat.FilteredColimits.colimitCommMonoid
       (F ⋙ forget₂ CommGrpCat CommMonCat.{max v u}) with }
 
 /-- The bundled commutative group giving the filtered colimit of a diagram. -/
 @[to_additive
 /-- The bundled additive commutative group giving the filtered colimit of a diagram. -/]
-noncomputable def colimit : CommGrpCat :=
+def colimit : CommGrpCat :=
   CommGrpCat.of (G.{v, u} F)
 
 /-- The cocone over the proposed colimit commutative group. -/
 @[to_additive /-- The cocone over the proposed colimit additive commutative group. -/]
-noncomputable def colimitCocone : Cocone F where
+def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι.app J := CommGrpCat.ofHom
     ((GrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommGrpCat GrpCat)).ι.app J).hom
@@ -195,12 +195,12 @@ noncomputable def colimitCocone : Cocone F where
 
 /-- The proposed colimit cocone is a colimit in `CommGrpCat`. -/
 @[to_additive /-- The proposed colimit cocone is a colimit in `AddCommGroup`. -/]
-noncomputable def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) :=
+def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) :=
   isColimitOfReflects (forget₂ _ GrpCat)
     (GrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ CommGrpCat GrpCat))
 
 @[to_additive]
-noncomputable instance forget₂Group_preservesFilteredColimits :
+instance forget₂Group_preservesFilteredColimits :
     PreservesFilteredColimits (forget₂ CommGrpCat GrpCat.{u}) where
   preserves_filtered_colimits J hJ1 _ :=
     letI : Category J := hJ1
@@ -210,7 +210,7 @@ noncomputable instance forget₂Group_preservesFilteredColimits :
             (F ⋙ forget₂ CommGrpCat GrpCat.{u})) }
 
 @[to_additive]
-noncomputable instance forget_preservesFilteredColimits :
+instance forget_preservesFilteredColimits :
     PreservesFilteredColimits (forget CommGrpCat.{u}) :=
   Limits.comp_preservesFilteredColimits (forget₂ CommGrpCat GrpCat) (forget GrpCat.{u})
 

Mathlib/Algebra/Category/Grp/Limits.lean

@@ -67,7 +67,7 @@ section
 variable [Small.{u} (Functor.sections (F ⋙ forget GrpCat))]
 
 @[to_additive]
-noncomputable instance limitGroup :
+instance limitGroup :
     Group (Types.Small.limitCone.{v, u} (F ⋙ forget GrpCat.{u})).pt :=
   inferInstanceAs <| Group (Shrink (F ⋙ forget GrpCat.{u}).sections)
 
@@ -83,7 +83,7 @@ the existing limit. -/
 
 All we need to do is notice that the limit point has an `AddGroup` instance available, and then
 reuse the existing limit. -/]
-noncomputable instance Forget₂.createsLimit :
+instance Forget₂.createsLimit :
     CreatesLimit F (forget₂ GrpCat.{u} MonCat.{u}) :=
   -- Porting note: need to add `forget₂ GrpCat MonCat` reflects isomorphism
   letI : (forget₂ GrpCat.{u} MonCat.{u}).ReflectsIsomorphisms :=
@@ -111,14 +111,14 @@ noncomputable instance Forget₂.createsLimit :
 (Generally, you'll just want to use `limit F`.) -/
 @[to_additive /-- A choice of limit cone for a functor into `GrpCat`.
   (Generally, you'll just want to use `limit F`.) -/]
-noncomputable def limitCone : Cone F :=
+def limitCone : Cone F :=
   liftLimit (limit.isLimit (F ⋙ forget₂ GrpCat.{u} MonCat.{u}))
 
 /-- The chosen cone is a limit cone.
 (Generally, you'll just want to use `limit.cone F`.) -/
 @[to_additive /-- The chosen cone is a limit cone.
 (Generally, you'll just want to use `limit.cone F`.) -/]
-noncomputable def limitConeIsLimit : IsLimit (limitCone F) :=
+def limitConeIsLimit : IsLimit (limitCone F) :=
   liftedLimitIsLimit _
 
 /-- If `(F ⋙ forget GrpCat).sections` is `u`-small, `F` has a limit. -/
@@ -196,21 +196,21 @@ instance forget_preservesLimits : PreservesLimits (forget GrpCat.{u}) :=
   GrpCat.forget_preservesLimitsOfSize.{u, u}
 
 @[to_additive]
-noncomputable instance forget_createsLimit :
+instance forget_createsLimit :
     CreatesLimit F (forget GrpCat.{u}) := by
   set e : forget₂ GrpCat.{u} MonCat.{u} ⋙ forget MonCat.{u} ≅ forget GrpCat.{u} := Iso.refl _
   exact createsLimitOfNatIso e
 
 @[to_additive]
-noncomputable instance forget_createsLimitsOfShape :
+instance forget_createsLimitsOfShape :
     CreatesLimitsOfShape J (forget GrpCat.{u}) where
   CreatesLimit := inferInstance
 
 /-- The forgetful functor from groups to types creates all limits.
 -/
 @[to_additive
 /-- The forgetful functor from additive groups to types creates all limits. -/]
-noncomputable instance forget_createsLimitsOfSize :
+instance forget_createsLimitsOfSize :
     CreatesLimitsOfSize.{w, v} (forget GrpCat.{u}) where
   CreatesLimitsOfShape := inferInstance
 end GrpCat
@@ -224,7 +224,7 @@ instance commGroupObj (j) : CommGroup ((F ⋙ forget CommGrpCat).obj j) :=
   inferInstanceAs <| CommGroup (F.obj j)
 
 @[to_additive]
-noncomputable instance limitCommGroup
+instance limitCommGroup
     [Small.{u} (Functor.sections (F ⋙ forget CommGrpCat))] :
     CommGroup (Types.Small.limitCone.{v, u} (F ⋙ forget CommGrpCat.{u})).pt :=
   letI : CommGroup (F ⋙ forget CommGrpCat.{u}).sections :=
@@ -245,7 +245,7 @@ and then reuse the existing limit.
 
 All we need to do is notice that the limit point has an `AddCommGroup` instance available,
 and then reuse the existing limit. -/]
-noncomputable instance Forget₂.createsLimit :
+instance Forget₂.createsLimit :
     CreatesLimit F (forget₂ CommGrpCat GrpCat.{u}) :=
   createsLimitOfReflectsIso (fun c hc => by
     have : HasLimit _ := ⟨_, hc⟩
@@ -276,7 +276,7 @@ variable [Small.{u} (Functor.sections (F ⋙ forget CommGrpCat))]
 @[to_additive
 /-- A choice of limit cone for a functor into `AddCommGrpCat`.
 (Generally, you'll just want to use `limit F`.) -/]
-noncomputable def limitCone : Cone F :=
+def limitCone : Cone F :=
   letI : Small.{u} (Functor.sections ((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat)) :=
     inferInstanceAs <| Small (Functor.sections (F ⋙ forget CommGrpCat))
   liftLimit (limit.isLimit (F ⋙ forget₂ CommGrpCat.{u} GrpCat.{u}))
@@ -286,7 +286,7 @@ noncomputable def limitCone : Cone F :=
 @[to_additive
 /-- The chosen cone is a limit cone.
 (Generally, you'll just want to use `limit.cone F`.) -/]
-noncomputable def limitConeIsLimit : IsLimit (limitCone.{v, u} F) :=
+def limitConeIsLimit : IsLimit (limitCone.{v, u} F) :=
   liftedLimitIsLimit _
 
 /-- If `(F ⋙ forget CommGrpCat).sections` is `u`-small, `F` has a limit. -/
@@ -359,7 +359,7 @@ instance forget₂Group_preservesLimits :
 /-- An auxiliary declaration to speed up typechecking. -/
 @[to_additive AddCommGrpCat.forget₂AddCommMon_preservesLimitsAux
 /-- An auxiliary declaration to speed up typechecking. -/]
-noncomputable def forget₂CommMon_preservesLimitsAux
+def forget₂CommMon_preservesLimitsAux
     [Small.{u} (F ⋙ forget CommGrpCat).sections] :
     IsLimit ((forget₂ CommGrpCat.{u} CommMonCat.{u}).mapCone (limitCone.{v, u} F)) :=
   letI : Small.{u} (Functor.sections ((F ⋙ forget₂ _ CommMonCat) ⋙ forget CommMonCat)) :=
@@ -407,30 +407,30 @@ types.) -/]
 instance forget_preservesLimitsOfSize :
     PreservesLimitsOfSize.{w, v} (forget CommGrpCat.{u}) := inferInstance
 
-noncomputable instance _root_.AddCommGrpCat.forget_preservesLimits :
+instance _root_.AddCommGrpCat.forget_preservesLimits :
     PreservesLimits (forget AddCommGrpCat.{u}) :=
   AddCommGrpCat.forget_preservesLimitsOfSize.{u, u}
 
 @[to_additive existing]
-noncomputable instance forget_preservesLimits : PreservesLimits (forget CommGrpCat.{u}) :=
+instance forget_preservesLimits : PreservesLimits (forget CommGrpCat.{u}) :=
   CommGrpCat.forget_preservesLimitsOfSize.{u, u}
 
 @[to_additive]
-noncomputable instance forget_createsLimit :
+instance forget_createsLimit :
     CreatesLimit F (forget CommGrpCat.{u}) := by
   set e : forget₂ CommGrpCat.{u} GrpCat.{u} ⋙ forget GrpCat.{u} ≅ forget CommGrpCat.{u} := .refl _
   exact createsLimitOfNatIso e
 
 @[to_additive]
-noncomputable instance forget_createsLimitsOfShape (J : Type v) [Category.{w} J] :
+instance forget_createsLimitsOfShape (J : Type v) [Category.{w} J] :
     CreatesLimitsOfShape J (forget CommGrpCat.{u}) where
   CreatesLimit := inferInstance
 
 /-- The forgetful functor from commutative groups to types creates all limits.
 -/
 @[to_additive
 /-- The forgetful functor from additive commutative groups to types creates all limits. -/]
-noncomputable instance forget_createsLimitsOfSize :
+instance forget_createsLimitsOfSize :
     CreatesLimitsOfSize.{w, v} (forget CommGrpCat.{u}) where
   CreatesLimitsOfShape := inferInstance
 

Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

@@ -129,7 +129,7 @@ def Presentation.isColimit {M : SheafOfModules.{u} R} (P : Presentation M) :
 set_option backward.defeqAttrib.useBackward true in
 /-- Mapping a presentation under an isomorphism. -/
 @[simps]
-noncomputable def Presentation.ofIsIso {M N : SheafOfModules.{u} R} (f : M ⟶ N) [IsIso f]
+def Presentation.ofIsIso {M N : SheafOfModules.{u} R} (f : M ⟶ N) [IsIso f]
     (σ : M.Presentation) : N.Presentation where
   generators := σ.generators.ofEpi f
   relations := σ.relations.ofEpi ((kernelCompMono _ f).symm.trans <| eqToIso (by simp)).hom
@@ -386,7 +386,7 @@ theorem Presentation.isQuasicoherent {M : SheafOfModules.{u} R} (P : Presentatio
 
 /-- Mapping quasicoherent data under an isomorphism. -/
 @[simps]
-noncomputable def QuasicoherentData.ofIsIso {M N : SheafOfModules.{u} R} (f : M ⟶ N) [IsIso f]
+def QuasicoherentData.ofIsIso {M N : SheafOfModules.{u} R} (f : M ⟶ N) [IsIso f]
     (σ : M.QuasicoherentData) : N.QuasicoherentData where
   I := σ.I
   X := σ.X