chore: add links to porting notes (#5111)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
leanprover-community · Jun 25, 2023 · 5448d1d · 5448d1d
1 parent 5138c7b
commit 5448d1d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/Mathlib/AlgebraicGeometry/Spec.lean b/Mathlib/AlgebraicGeometry/Spec.lean
@@ -346,6 +346,7 @@ theorem Spec_map_localization_isIso (R : CommRingCat) (M : Submonoid R)
         (Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap R (Localization M))).op) x) := by
   erw [← localRingHom_comp_stalkIso]
   -- Porting note: replaced `apply (config := { instances := false })`.
+  -- See https://github.com/leanprover/lean4/issues/2273
   refine @IsIso.comp_isIso _ _ _ _ _ _ _ _ (?_)
   refine @IsIso.comp_isIso _ _ _ _ _ _ _ (?_) _
   /- I do not know why this is defeq to the goal, but I'm happy to accept that it is. -/

diff --git a/Mathlib/Topology/Sheaves/Operations.lean b/Mathlib/Topology/Sheaves/Operations.lean
@@ -118,7 +118,8 @@ noncomputable def toTotalQuotientPresheaf : F ⟶ F.totalQuotientPresheaf :=
 instance : Epi (toTotalQuotientPresheaf F) := epi_toLocalizationPresheaf _
 
 instance (F : X.Sheaf CommRingCat.{w}) : Mono F.presheaf.toTotalQuotientPresheaf := by
-  -- Porting note : was an `apply (config := { synthAssignedInstances := false })`
+  -- Porting note : was an `apply (config := { instances := false })`
+  -- See https://github.com/leanprover/lean4/issues/2273
   suffices : ∀ (U : (Opens ↑X)ᵒᵖ), Mono (F.presheaf.toTotalQuotientPresheaf.app U)
   . apply NatTrans.mono_of_mono_app
   intro U