feat(CategoryTheory): Functors that preserve the terminal object are Final (leanprover-community#39994)

Co-authored-by: Brian-Nugent <bnugent@uw.edu>

Author: Brian-Nugent

Mathlib/CategoryTheory/Limits/Final.lean

@@ -940,6 +940,24 @@ lemma initial_fromPUnit_of_isInitial (hc : Limits.IsInitial c) : (fromPUnit c).I
       ⟨fun i j ↦ CostructuredArrow.obj_ext _ _ (by cat_disch) (hc.hom_ext _ _)⟩
     infer_instance
 
+instance [HasTerminal C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
+    [PreservesLimit (Functor.empty.{0} C) F] : F.Final :=
+  have : (fromPUnit.{0} (⊤_ C)).Final := final_fromPUnit_of_isTerminal terminalIsTerminal
+  have : (fromPUnit.{0} (F.obj (⊤_ C))).Final := final_fromPUnit_of_isTerminal
+    (terminalIsTerminal.isTerminalObj F (⊤_ C))
+  have : ((fromPUnit.{0} (⊤_ C)) ⋙ F).Final := final_of_natIso (F := fromPUnit.{0} (F.obj (⊤_ C)))
+    (Discrete.natIso (fun _ => Iso.refl _))
+  final_of_final_comp (fromPUnit.{0} (⊤_ C)) F
+
+instance [HasInitial C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
+    [PreservesColimit (Functor.empty.{0} C) F] : F.Initial :=
+  have : (fromPUnit.{0} (⊥_ C)).Initial := initial_fromPUnit_of_isInitial initialIsInitial
+  have : (fromPUnit.{0} (F.obj (⊥_ C))).Initial := initial_fromPUnit_of_isInitial
+    (initialIsInitial.isInitialObj F (⊥_ C))
+  have : ((fromPUnit.{0} (⊥_ C)) ⋙ F).Initial := initial_of_natIso
+    (F := fromPUnit.{0} (F.obj (⊥_ C))) (Discrete.natIso (fun _ => Iso.refl _))
+  initial_of_initial_comp (fromPUnit.{0} (⊥_ C)) F
+
 end
 
 section

Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean

@@ -98,7 +98,8 @@ lemma Presieve.isSheafFor_sigmaDesc_iff {ι : Type*} {X : ι → C} (f : ∀ i,
     dsimp [E]; infer_instance
   have : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F := by
     convert! Functor.Initial.preservesLimit_of_comp (Discrete.equivalence <| .sigmaPUnit _).inverse
-    assumption
+    · infer_instance
+    · assumption
   let equiv := (E.isLimitSigmaOfIsColimitEquiv hc hc' F).nonempty_congr
   rwa [isLimit_toPreOneHypercover_type_iff, isLimit_toPreOneHypercover_type_iff,
     presieve₀_sigmaOfIsColimit] at equiv