chore(AlgebraicGeometry): minor cleanup (#13080)

Motivated by trying to clean up `CommRingCat` and friends, but this is a downstream fix that seems fine independently (and helpful later).

Mathlib/AlgebraicGeometry/Spec.lean

@@ -70,13 +70,14 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 theorem Spec.topMap_id (R : CommRingCat.{u}) : Spec.topMap (𝟙 R) = 𝟙 (Spec.topObj R) :=
-  PrimeSpectrum.comap_id
+  rfl
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.Top_map_id AlgebraicGeometry.Spec.topMap_id
 
+@[simp]
 theorem Spec.topMap_comp {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) :
     Spec.topMap (f ≫ g) = Spec.topMap g ≫ Spec.topMap f :=
-  PrimeSpectrum.comap_comp _ _
+  rfl
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.Top_map_comp AlgebraicGeometry.Spec.topMap_comp
 
@@ -88,8 +89,6 @@ set_option linter.uppercaseLean3 false in
 def Spec.toTop : CommRingCat.{u}ᵒᵖ ⥤ TopCat where
   obj R := Spec.topObj (unop R)
   map {R S} f := Spec.topMap f.unop
-  map_id R := by dsimp; rw [Spec.topMap_id]
-  map_comp {R S T} f g := by dsimp; rw [Spec.topMap_comp]
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.to_Top AlgebraicGeometry.Spec.toTop
 
@@ -120,11 +119,10 @@ set_option linter.uppercaseLean3 false in
 theorem Spec.sheafedSpaceMap_id {R : CommRingCat.{u}} :
     Spec.sheafedSpaceMap (𝟙 R) = 𝟙 (Spec.sheafedSpaceObj R) :=
   AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_id R) <| by
-    ext U
+    ext
     dsimp
-    erw [PresheafedSpace.id_c_app, comap_id]; swap
-    · rw [Spec.topMap_id, TopologicalSpace.Opens.map_id_obj_unop]
-    simp [eqToHom_map]
+    erw [comap_id (by simp)]
+    simp
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.SheafedSpace_map_id AlgebraicGeometry.Spec.sheafedSpaceMap_id
 

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -1188,7 +1188,7 @@ The comap of the identity is the identity. In this variant of the lemma, two ope
 `V` are given as arguments, together with a proof that `U = V`. This is useful when `U` and `V`
 are not definitionally equal.
 -/
-theorem comap_id (U V : Opens (PrimeSpectrum.Top R)) (hUV : U = V) :
+theorem comap_id {U V : Opens (PrimeSpectrum.Top R)} (hUV : U = V) :
     (comap (RingHom.id R) U V fun p hpV => by rwa [hUV, PrimeSpectrum.comap_id]) =
       eqToHom (show (structureSheaf R).1.obj (op U) = _ by rw [hUV]) :=
   by erw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]
@@ -1197,7 +1197,7 @@ theorem comap_id (U V : Opens (PrimeSpectrum.Top R)) (hUV : U = V) :
 @[simp]
 theorem comap_id' (U : Opens (PrimeSpectrum.Top R)) :
     (comap (RingHom.id R) U U fun p hpU => by rwa [PrimeSpectrum.comap_id]) = RingHom.id _ := by
-  rw [comap_id U U rfl]; rfl
+  rw [comap_id rfl]; rfl
 #align algebraic_geometry.structure_sheaf.comap_id' AlgebraicGeometry.StructureSheaf.comap_id'
 
 theorem comap_comp (f : R →+* S) (g : S →+* P) (U : Opens (PrimeSpectrum.Top R))

Mathlib/Geometry/RingedSpace/SheafedSpace.lean

@@ -143,8 +143,7 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 theorem id_c_app (X : SheafedSpace C) (U) :
-    (𝟙 X : X ⟶ X).c.app U = eqToHom (by aesop_cat) := by
-  aesop_cat
+    (𝟙 X : X ⟶ X).c.app U = 𝟙 _ := rfl
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.SheafedSpace.id_c_app AlgebraicGeometry.SheafedSpace.id_c_app