add notes

chrisflav · chrisflav · commit d16e6d6e6c0f · 2024-12-12T18:28:19.000+01:00
diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean
@@ -282,7 +282,7 @@ instance equalizer_ι_is_local_ring_hom' (F : WalkingParallelPairᵒᵖ ⥤ Comm
         ⟨_, IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv⟩
         WalkingParallelPair.zero : _)
   erw [← this]
-  -- note: this was not needed before
+  -- note: this was not needed before https://github.com/leanprover-community/mathlib4/pull/19757
   haveI : IsLocalHom (limit.π (walkingParallelPairOpEquiv.functor ⋙ F) zero).hom := by
     infer_instance
   infer_instance
diff --git a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
@@ -124,6 +124,8 @@ theorem isUnit_res_toΓSpecMapBasicOpen : IsUnit (X.toToΓSpecMapBasicOpen r r)
 def toΓSpecCApp :
     (structureSheaf <| Γ.obj <| op X).val.obj (op <| basicOpen r) ⟶
       X.presheaf.obj (op <| X.toΓSpecMapBasicOpen r) :=
+  -- note: the explicit type annotations were not needed before
+  -- https://github.com/leanprover-community/mathlib4/pull/19757
   CommRingCat.ofHom  <|
     IsLocalization.Away.lift
       (R := Γ.obj (op X))
