Revert

Author: kim-em

Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

@@ -612,10 +612,7 @@ noncomputable section image
 
 open Limits
 
-variable {X Y : Scheme.{u}} (f : X.Hom Y)
-
-section
-variable (U : Y.affineOpens)
+variable {X Y : Scheme.{u}} (f : X.Hom Y) (U : Y.affineOpens)
 
 /-- The scheme theoretic image of a morphism. -/
 abbrev Hom.image : Scheme.{u} := f.ker.subscheme
@@ -701,8 +698,6 @@ lemma Hom.toImage_app_injective [QuasiCompact f] :
   exact (RingHom.lift_injective_of_ker_le_ideal _ _ (by simp)).comp
     (f.ker.subschemeObjIso U).commRingCatIsoToRingEquiv.injective
 
-end
-
 lemma Hom.stalkFunctor_toImage_injective [QuasiCompact f] (x) :
     Function.Injective ((TopCat.Presheaf.stalkFunctor _ x).map f.toImage.c) := by
   apply TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis

Mathlib/CategoryTheory/Functor/Functorial.lean

@@ -50,8 +50,6 @@ instance (F : C ⥤ D) : Functorial.{v₁, v₂} F.obj :=
 theorem map_functorial_obj (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) : map F.obj f = F.map f :=
   rfl
 
-attribute [grind] id
-
 instance functorial_id : Functorial.{v₁, v₁} (id : C → C) where map f := f
 
 section

Mathlib/CategoryTheory/Iso.lean

@@ -208,7 +208,7 @@ theorem hom_eq_inv (α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom =
   rw [← symm_inv, inv_eq_inv α.symm β, eq_comm]
   rfl
 
-attribute [grind] Function.LeftInverse Function.RightInverse
+attribute [local grind] Function.LeftInverse Function.RightInverse
 
 /-- The bijection `(Z ⟶ X) ≃ (Z ⟶ Y)` induced by `α : X ≅ Y`. -/
 @[simps]