From cbacc654281a03c6041d8e75e72364024f4052e6 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Wed, 10 Apr 2024 06:01:52 +0000
Subject: [PATCH] chore: future-proof proofs in Category/Ring/Limits (#11839)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

These proofs will become slow after https://github.com/leanprover/lean4/pull/3807, but with these changes there is no regression. 🤷‍♀️

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 Mathlib/Algebra/Category/Ring/Limits.lean | 37 +++++++++--------------
 1 file changed, 15 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Algebra/Category/Ring/Limits.lean b/Mathlib/Algebra/Category/Ring/Limits.lean
index 8824c11e69629..5e935859a453f 100644
--- a/Mathlib/Algebra/Category/Ring/Limits.lean
+++ b/Mathlib/Algebra/Category/Ring/Limits.lean
@@ -388,16 +388,16 @@ All we need to do is notice that the limit point has a `Ring` instance available
 and then reuse the existing limit.
 -/
 instance : CreatesLimit F (forget₂ RingCat.{u} SemiRingCat.{u}) :=
-  letI : ReflectsIsomorphisms (forget₂ RingCat SemiRingCat) :=
+  have : ReflectsIsomorphisms (forget₂ RingCat SemiRingCat) :=
     CategoryTheory.reflectsIsomorphisms_forget₂ _ _
-  letI : Small.{u} (Functor.sections ((F ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
+  have : Small.{u} (Functor.sections ((F ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
     inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
-  letI c : Cone F :=
+  let c : Cone F :=
   { pt := RingCat.of (Types.Small.limitCone (F ⋙ forget _)).pt
     π :=
-      { app := fun x => SemiRingCat.ofHom _
-        naturality := (SemiRingCat.HasLimits.limitCone
-          (F ⋙ forget₂ RingCat SemiRingCat.{u})).π.naturality } }
+      { app := fun x => ofHom <| SemiRingCat.limitπRingHom.{v, u} (F ⋙ forget₂ _ SemiRingCat) x
+        naturality := fun _ _ f => RingHom.coe_inj
+          ((Types.Small.limitCone (F ⋙ forget _)).π.naturality f) } }
   createsLimitOfReflectsIso fun c' t =>
     { liftedCone := c
       validLift := by apply IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit _) t
@@ -546,28 +546,21 @@ instance :
     but it seems this would introduce additional identity morphisms in `limit.π`.
     -/
     -- Porting note: need to add these instances manually
-    letI : ReflectsIsomorphisms (forget₂ CommRingCat.{u} RingCat.{u}) :=
+    have : ReflectsIsomorphisms (forget₂ CommRingCat.{u} RingCat.{u}) :=
       CategoryTheory.reflectsIsomorphisms_forget₂ _ _
-    letI : Small.{u}
-        (Functor.sections ((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat)) :=
+    have : Small.{u} (Functor.sections ((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat)) :=
       inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
-    letI : Small.{u}
-        (Functor.sections ((F ⋙ forget₂ _ RingCat ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
+    let F' := F ⋙ forget₂ CommRingCat.{u} RingCat.{u} ⋙ forget₂ RingCat.{u} SemiRingCat.{u}
+    have : Small.{u} (Functor.sections (F' ⋙ forget _)) :=
       inferInstanceAs <| Small.{u} (F ⋙ forget _).sections
-    letI c : Cone F :=
+    let c : Cone F :=
     { pt := CommRingCat.of (Types.Small.limitCone (F ⋙ forget _)).pt
       π :=
-        { app := fun x => ofHom <|
-              SemiRingCat.limitπRingHom.{v, u}
-                (F ⋙ forget₂ CommRingCat.{u} RingCat.{u} ⋙
-                  forget₂ RingCat.{u} SemiRingCat.{u}) x
+        { app := fun x => ofHom <| SemiRingCat.limitπRingHom.{v, u} F' x
           naturality :=
-            (SemiRingCat.HasLimits.limitCone.{v, u}
-                  (F ⋙
-                    forget₂ _ RingCat.{u} ⋙
-                      forget₂ _ SemiRingCat.{u})).π.naturality } }
-    createsLimitOfReflectsIso
-    fun _ t =>
+            fun _ _ f => RingHom.coe_inj
+              ((Types.Small.limitCone (F ⋙ forget _)).π.naturality f) } }
+    createsLimitOfReflectsIso fun _ t =>
     { liftedCone := c
       validLift := IsLimit.uniqueUpToIso (RingCat.limitConeIsLimit.{v, u} _) t
       makesLimit :=