chore: spell results using PreservesFiniteProducts (#24293)

I believe these were written before `PreservesFiniteProducts` was a thing.

Take the opportunity to make anonymous dot notation available.

From Toric

Author: YaelDillies

Mathlib/Algebra/Category/Ring/Under/Limits.lean

@@ -92,16 +92,12 @@ instance (J : Type u) [Finite J] (f : J → Under R) :
   have hc : IsLimit c := Under.piFanIsLimit f
   preservesLimit_of_preserves_limit_cone hc (piFanTensorProductIsLimit f)
 
-instance (J : Type) [Finite J] :
-    PreservesLimitsOfShape (Discrete J) (tensorProd R S) :=
-  let J' : Type u := ULift.{u} J
-  have : PreservesLimitsOfShape (Discrete J') (tensorProd R S) :=
-    preservesLimitsOfShape_of_discrete (tensorProd R S)
-  let e : Discrete J' ≌ Discrete J := Discrete.equivalence Equiv.ulift
-  preservesLimitsOfShape_of_equiv e (R.tensorProd S)
-
 instance : PreservesFiniteProducts (tensorProd R S) where
-  preserves J := { }
+  preserves n :=
+    let J : Type u := ULift.{u} (Fin n)
+    have : PreservesLimitsOfShape (Discrete J) (tensorProd R S) :=
+      preservesLimitsOfShape_of_discrete (tensorProd R S)
+    preservesLimitsOfShape_of_equiv (Discrete.equivalence Equiv.ulift) (R.tensorProd S)
 
 end Pi
 

Mathlib/CategoryTheory/Closed/Cartesian.lean

@@ -364,7 +364,7 @@ along the `prodComparison` isomorphism.
 -/
 noncomputable def cartesianClosedOfEquiv (e : C ≌ D) [CartesianClosed C] : CartesianClosed D :=
   letI := e.inverse.monoidalOfChosenFiniteProducts
-  MonoidalClosed.ofEquiv (e.inverse) e.symm.toAdjunction
+  MonoidalClosed.ofEquiv e.inverse e.symm.toAdjunction
 
 end Functor
 

Mathlib/CategoryTheory/Closed/Ideal.lean

@@ -302,11 +302,13 @@ lemma preservesBinaryProducts_of_exponentialIdeal :
 /--
 If a reflective subcategory is an exponential ideal, then the reflector preserves finite products.
 -/
-lemma preservesFiniteProducts_of_exponentialIdeal (J : Type) [Finite J] :
-    PreservesLimitsOfShape (Discrete J) (reflector i) := by
-  letI := preservesBinaryProducts_of_exponentialIdeal i
-  letI : PreservesLimitsOfShape _ (reflector i) := leftAdjoint_preservesTerminal_of_reflective.{0} i
-  apply preservesFiniteProducts_of_preserves_binary_and_terminal (reflector i) J
+lemma Limits.PreservesFiniteProducts._of_exponentialIdeal : PreservesFiniteProducts (reflector i) :=
+  have := preservesBinaryProducts_of_exponentialIdeal i
+  have : PreservesLimitsOfShape _ (reflector i) := leftAdjoint_preservesTerminal_of_reflective.{0} i
+  .of_preserves_binary_and_terminal _
+
+@[deprecated (since := "2025-04-22")]
+alias preservesFiniteProducts_of_exponentialIdeal := PreservesFiniteProducts._of_exponentialIdeal
 
 end
 

Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

@@ -3,10 +3,9 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+import Mathlib.CategoryTheory.Limits.Preserves.Finite
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
-import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
-import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
 
 /-!
 # Constructing finite products from binary products and terminal.
@@ -145,22 +144,23 @@ lemma preservesFinOfPreservesBinaryAndTerminal :
       simp only [id_comp, ← F.map_comp]
       rfl
 
-/-- If `F` preserves the terminal object and binary products, then it preserves limits of shape
-`Discrete (Fin n)`.
--/
-lemma preservesShape_fin_of_preserves_binary_and_terminal (n : ℕ) :
-    PreservesLimitsOfShape (Discrete (Fin n)) F where
-  preservesLimit {K} := by
+/-- If `F` preserves the terminal object and binary products then it preserves finite products. -/
+lemma Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal :
+    PreservesFiniteProducts F where
+  preserves n := by
+    refine ⟨fun {K} ↦ ?_⟩
     let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _
     haveI := preservesFinOfPreservesBinaryAndTerminal F n fun n => K.obj ⟨n⟩
     apply preservesLimit_of_iso_diagram F that
 
-/-- If `F` preserves the terminal object and binary products then it preserves finite products. -/
-lemma preservesFiniteProducts_of_preserves_binary_and_terminal (J : Type*) [Finite J] :
-    PreservesLimitsOfShape (Discrete J) F :=
-  let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
-  have := preservesShape_fin_of_preserves_binary_and_terminal F n
-  preservesLimitsOfShape_of_equiv (Discrete.equivalence e).symm _
+@[deprecated (since := "2025-04-20")]
+alias preservesFiniteProducts_of_preserves_binary_and_terminal :=
+  PreservesFiniteProducts.of_preserves_binary_and_terminal
+
+@[deprecated PreservesFiniteProducts.of_preserves_binary_and_terminal (since := "2025-04-22")]
+lemma preservesShape_fin_of_preserves_binary_and_terminal (n : ℕ) :
+    PreservesLimitsOfShape (Discrete (Fin n)) F :=
+  have : PreservesFiniteProducts F := .of_preserves_binary_and_terminal _; inferInstance
 
 end Preserves
 

Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean

@@ -266,15 +266,13 @@ theorem hasFiniteLimits_of_hasTerminal_and_pullbacks [HasTerminal C] [HasPullbac
 lemma preservesFiniteLimits_of_preservesTerminal_and_pullbacks [HasTerminal C]
     [HasPullbacks C] (G : C ⥤ D) [PreservesLimitsOfShape (Discrete.{0} PEmpty) G]
     [PreservesLimitsOfShape WalkingCospan G] : PreservesFiniteLimits G := by
-  haveI : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
-  haveI : PreservesLimitsOfShape (Discrete WalkingPair) G :=
+  have : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
+  have : PreservesLimitsOfShape (Discrete WalkingPair) G :=
     preservesBinaryProducts_of_preservesTerminal_and_pullbacks G
-  haveI : PreservesLimitsOfShape WalkingParallelPair G :=
-      preservesEqualizers_of_preservesPullbacks_and_binaryProducts G
-  apply
-    @preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts _ _ _ _ _ _ G _ ?_
-  refine ⟨fun n ↦ ?_⟩
-  apply preservesFiniteProducts_of_preserves_binary_and_terminal G
+  have : PreservesLimitsOfShape WalkingParallelPair G :=
+    preservesEqualizers_of_preservesPullbacks_and_binaryProducts G
+  have : PreservesFiniteProducts G := .of_preserves_binary_and_terminal _
+  exact preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts G
 
 attribute [local instance] preservesFiniteLimits_of_preservesTerminal_and_pullbacks in
 /-- If a functor creates terminal objects and pullbacks, it creates finite limits.

Mathlib/CategoryTheory/Preadditive/LeftExact.lean

@@ -3,17 +3,18 @@ Copyright (c) 2022 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Jakob von Raumer
 -/
-import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
-import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
 import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 
 /-!
 # Left exactness of functors between preadditive categories
 
 We show that a functor is left exact in the sense that it preserves finite limits, if it
 preserves kernels. The dual result holds for right exact functors and cokernels.
+
 ## Main results
+
 * We first derive preservation of binary product in the lemma
   `preservesBinaryProductsOfPreservesKernels`,
 * then show the preservation of equalizers in `preservesEqualizerOfPreservesKernels`,
@@ -110,13 +111,12 @@ lemma preservesEqualizers_of_preservesKernels
 -/
 lemma preservesFiniteLimits_of_preservesKernels [HasFiniteProducts C] [HasEqualizers C]
     [HasZeroObject C] [HasZeroObject D] [∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F] :
-    PreservesFiniteLimits F := by
-  letI := preservesEqualizers_of_preservesKernels F
-  letI := preservesTerminalObject_of_preservesZeroMorphisms F
-  letI := preservesLimitsOfShape_pempty_of_preservesTerminal F
-  letI : PreservesFiniteProducts F :=
-    ⟨fun _ ↦ preservesFiniteProducts_of_preserves_binary_and_terminal F _⟩
-  exact preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts F
+    PreservesFiniteLimits F :=
+  have := preservesEqualizers_of_preservesKernels F
+  have := preservesTerminalObject_of_preservesZeroMorphisms F
+  have := preservesLimitsOfShape_pempty_of_preservesTerminal F
+  have : PreservesFiniteProducts F :=.of_preserves_binary_and_terminal F
+  preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts F
 
 end FiniteLimits