feat: bump to v4.22.0-rc3 (#30)

* feat: bump to v4.21.0-rc3

Main difference: ChosenFiniteProducts is now CartesianMonoidalCategory.

* feat: bump to v4.22.0-rc2

* chore: obey unused simp arg linter

* chore: bump to Lean v4.22.0-rc3

* chore: banish `by rfl`

Author: Vtec234

Poly/Bifunctor/Basic.lean

@@ -27,15 +27,13 @@ scoped [CategoryTheory] infixr:80 " ⋙₂ " => Functor.comp₂
 @[simp]
 theorem comp_comp₂ {𝒟'' : Type*} [Category 𝒟'']
     (F : 𝒟'' ⥤ 𝒟') (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
-    (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := by
-  rfl
+    (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := rfl
 
 /-- Composition with `F,G` ordered like the arguments of `P` is considered `simp`ler. -/
 @[simp]
 theorem comp₂_comp {𝒞' : Type*} [Category 𝒞']
     (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
-    G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := by
-  rfl
+    G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := rfl
 
 @[simps!]
 def comp₂_iso {F₁ F₂ : 𝒟' ⥤ 𝒟} {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ}

Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean

@@ -17,8 +17,7 @@ variable {T : Type u₁} [Category.{v₁} T]
 namespace Over
 
 @[simp]
-theorem mk_eta {X : T} (U : Over X) : mk U.hom = U := by
-  rfl
+theorem mk_eta {X : T} (U : Over X) : mk U.hom = U := rfl
 
 /-- A variant of `homMk_comp` that can trigger in `simp`. -/
 @[simp]
@@ -30,8 +29,7 @@ lemma homMk_comp' {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_c
 @[simp]
 lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) :
     homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp =
-    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := by
-  rfl
+    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := rfl
 
 @[simp]
 lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) :=
@@ -57,8 +55,7 @@ lemma map_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
     ((Over.map Y.hom).map g).left = g.left := Over.map_map_left
 
 lemma map_homMk_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
-    map g = (Over.homMk g.left : Sigma Y Z ⟶ Sigma Y Z') := by
-  rfl
+    map g = (Over.homMk g.left : Sigma Y Z ⟶ Sigma Y Z') := rfl
 
 /-- The first projection of the sigma object. -/
 @[simps!]

Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sina Hazratpour
 -/
 import Mathlib.CategoryTheory.Comma.Over.Pullback
-import Mathlib.CategoryTheory.ChosenFiniteProducts
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
 import Mathlib.CategoryTheory.Monad.Products
 import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic
@@ -16,7 +16,9 @@ universe v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
 
-open Category Limits Comonad MonoidalCategory
+open Category Limits Comonad MonoidalCategory CartesianMonoidalCategory
+
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 variable {C : Type u₁} [Category.{v₁} C]
 
@@ -32,8 +34,7 @@ namespace Reindex
 variable [HasPullbacks C] {X : C}
 
 lemma hom {Y : Over X} {Z : Over X} :
-    (Reindex Y Z).hom = pullback.snd Z.hom Y.hom := by
-  rfl
+    (Reindex Y Z).hom = pullback.snd Z.hom Y.hom := rfl
 
 /-- `Reindex` is symmetric in its first and second arguments up to an isomorphism. -/
 def symmetryObjIso (Y Z : Over X) :
@@ -57,7 +58,7 @@ lemma symmetry_hom {Y Z : Over X} :
 def fstProj (Y Z : Over X) : Sigma Y (Reindex Y Z) ⟶ Y :=
   Over.homMk (pullback.snd Z.hom Y.hom) (by simp)
 
-lemma fstProj_sigma_fst (Y Z : Over X) : fstProj Y Z = Sigma.fst (Reindex Y Z) := by rfl
+lemma fstProj_sigma_fst (Y Z : Over X) : fstProj Y Z = Sigma.fst (Reindex Y Z) := rfl
 
 /-- The second projection out of the reindexed sigma object. -/
 def sndProj (Y Z : Over X) : Sigma Y (Reindex Y Z) ⟶ Z :=
@@ -87,7 +88,7 @@ end Reindex
 
 section BinaryProduct
 
-open ChosenFiniteProducts Sigma Reindex
+open Sigma Reindex
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -106,8 +107,6 @@ def isBinaryProductSigmaReindex (Y Z : Over X) :
     · exact congr_arg CommaMorphism.left (h ⟨ .right⟩)
     · exact congr_arg CommaMorphism.left (h ⟨ .left ⟩)
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-
 /-- The object `(Sigma Y) (Reindex Y Z)` is isomorphic to the binary product `Y × Z`
 in `Over X`. -/
 @[simps!]
@@ -122,12 +121,12 @@ def sigmaReindexIsoProdMk {Y : C} (f : Y ⟶ X) (Z : Over X) :
   sigmaReindexIsoProd (Over.mk f) _
 
 lemma sigmaReindexIsoProd_hom_comp_fst {Y Z : Over X} :
-    (sigmaReindexIsoProd Y Z).hom ≫ (fst Y Z) = (π_ Y Z) :=
+    (sigmaReindexIsoProd Y Z).hom ≫ fst Y Z = (π_ Y Z) :=
   IsLimit.conePointUniqueUpToIso_hom_comp
     (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.left⟩
 
 lemma sigmaReindexIsoProd_hom_comp_snd {Y Z : Over X} :
-    (sigmaReindexIsoProd Y Z).hom ≫ (snd Y Z) = (μ_ Y Z) :=
+    (sigmaReindexIsoProd Y Z).hom ≫ snd Y Z = (μ_ Y Z) :=
   IsLimit.conePointUniqueUpToIso_hom_comp
     (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.right⟩
 
@@ -137,10 +136,7 @@ end Over
 
 section TensorLeft
 
-open MonoidalCategory Over Functor ChosenFiniteProducts
-
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+open Over Functor
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -150,16 +146,16 @@ def Over.sigmaReindexNatIsoTensorLeft (Y : Over X) :
     (pullback Y.hom) ⋙ (map Y.hom) ≅ tensorLeft Y := by
   fapply NatIso.ofComponents
   · intro Z
-    simp only [const_obj_obj, Functor.id_obj, comp_obj, tensorLeft_obj, tensorObj, Over.pullback]
+    simp only [const_obj_obj, Functor.id_obj, comp_obj, Over.pullback]
     exact sigmaReindexIsoProd Y Z
   · intro Z Z' f
-    simp
+    dsimp
     ext1 <;> simp_rw [assoc]
-    · simp_rw [whiskerLeft_fst]
+    · rw [whiskerLeft_fst]
       iterate rw [sigmaReindexIsoProd_hom_comp_fst]
       ext
       simp
-    · simp_rw [whiskerLeft_snd]
+    · rw [whiskerLeft_snd]
       iterate rw [sigmaReindexIsoProd_hom_comp_snd, ← assoc, sigmaReindexIsoProd_hom_comp_snd]
       ext
       simp [Reindex.sndProj]
@@ -187,7 +183,7 @@ def equivOverTerminal [HasTerminal C] : Over (⊤_ C) ≌ C :=
 
 namespace Over
 
-open MonoidalCategory
+open CartesianMonoidalCategory
 
 variable {C}
 
@@ -201,15 +197,14 @@ lemma star_map [HasBinaryProducts C] {X : C} {Y Z : C} (f : Y ⟶ Z) :
 instance [HasBinaryProducts C]  (X : C) : (forget X).IsLeftAdjoint  :=
   ⟨_, ⟨forgetAdjStar X⟩⟩
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 lemma whiskerLeftProdMapId [HasFiniteLimits C] {X : C} {A A' : C} {g : A ⟶ A'} :
     X ◁ g = prod.map (𝟙 X) g := by
   ext
-  · simp only [ChosenFiniteProducts.whiskerLeft_fst]
+  · simp only [whiskerLeft_fst]
     exact (Category.comp_id _).symm.trans (prod.map_fst (𝟙 X) g).symm
-  · simp only [ChosenFiniteProducts.whiskerLeft_snd]
+  · simp only [whiskerLeft_snd]
     exact (prod.map_snd (𝟙 X) g).symm
 
 def starForgetIsoTensorLeft [HasFiniteLimits C] (X : C) :

Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean

@@ -21,49 +21,48 @@ universe v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
 
-open Category Limits MonoidalCategory CartesianClosed Adjunction Over
+open Category Limits MonoidalCategory CartesianMonoidalCategory CartesianClosed Adjunction Over
 
 variable {C : Type u₁} [Category.{v₁} C]
 
 attribute [local instance] hasBinaryProducts_of_hasTerminal_and_pullbacks
 attribute [local instance] hasFiniteProducts_of_has_binary_and_terminal
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 section
 
 variable [HasFiniteProducts C]
 
 /-- The isomorphism between `X ⨯ Y` and `X ⊗ Y` for objects `X` and `Y` in `C`.
 This is tautological by the definition of the cartesian monoidal structure on `C`.
-This isomorphism provides an interface between `prod.fst` and `ChosenFiniteProducts.fst`
+This isomorphism provides an interface between `prod.fst` and `CartesianMonoidalCategory.fst`
 as well as between `prod.map` and `tensorHom`. -/
 def prodIsoTensorObj (X Y : C) : X ⨯ Y ≅ X ⊗ Y := Iso.refl _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_inv_fst {X Y : C} :
-    (prodIsoTensorObj X Y).inv ≫ prod.fst = ChosenFiniteProducts.fst X Y :=
+    (prodIsoTensorObj X Y).inv ≫ prod.fst = fst X Y :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_inv_snd {X Y : C} :
-    (prodIsoTensorObj X Y).inv ≫ prod.snd = ChosenFiniteProducts.snd X Y :=
+    (prodIsoTensorObj X Y).inv ≫ prod.snd = snd X Y :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_hom_fst {X Y : C} :
-    (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.fst X Y = prod.fst :=
+    (prodIsoTensorObj X Y).hom ≫ fst X Y = prod.fst :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_hom_snd {X Y : C} :
-    (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.snd X Y = prod.snd :=
+    (prodIsoTensorObj X Y).hom ≫ snd X Y = prod.snd :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodMap_comp_prodIsoTensorObj_hom {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) :
-    prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ g) := by
-  apply ChosenFiniteProducts.hom_ext <;> simp
+    prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ₘ g) := by
+  apply hom_ext <;> simp
 
 end
 
@@ -73,7 +72,7 @@ variable (I : C) [Exponentiable I]
 
 /-- The first leg of a cospan constructing a pullback diagram in `C` used to define `sections` . -/
 def curryId : ⊤_ C ⟶ (I ⟹ I) :=
-  CartesianClosed.curry (ChosenFiniteProducts.fst I (⊤_ C))
+  CartesianClosed.curry (fst I (⊤_ C))
 
 variable {I}
 

Poly/ForMathlib/CategoryTheory/Elements.lean

@@ -22,7 +22,7 @@ theorem map_homMk_id {X : 𝒞} (a : F.obj X) (eq : F.map (𝟙 X) a = a) :
 theorem map_homMk_comp {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) eq :
     G.map (Y := ⟨Z, F.map g (F.map f a)⟩) (Subtype.mk (α := X ⟶ Z) (f ≫ g) eq) =
     G.map (X := ⟨X, a⟩) (Y := ⟨Y, F.map f a⟩) (Subtype.mk (α := X ⟶ Y) f rfl) ≫
-    G.map (Subtype.mk (α := Y ⟶ Z) g (by rfl)) := by
+    G.map (Subtype.mk (α := Y ⟶ Z) g (rfl)) := by
   set X : F.Elements := ⟨X, a⟩
   set Y : F.Elements := ⟨Y, F.map f a⟩
   set Z : F.Elements := ⟨Z, F.map g (F.map f a)⟩

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean

@@ -62,11 +62,12 @@ universe v u
 
 namespace CategoryTheory
 
-open CategoryTheory Category MonoidalCategory Limits Functor Adjunction Over
+open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits Functor Adjunction
+  Over
 
 variable {C : Type u} [Category.{v} C]
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 /-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I`
 has a right adjoint. -/
@@ -223,7 +224,7 @@ end HasPushforwards
 
 namespace CartesianClosedOver
 
-open Over Reindex IsIso ChosenFiniteProducts CartesianClosed HasPushforwards ExponentiableMorphism
+open Over Reindex IsIso CartesianClosed HasPushforwards ExponentiableMorphism
 
 variable {C} [HasFiniteWidePullbacks C] {I J : C} [CartesianClosed (Over J)]
 

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean

@@ -129,8 +129,6 @@ def paste : cartesian (pasteCell f u) := by
   · unfold pasteCell2
     apply cartesian.whiskerRight (cellLeftCartesian f u)
 
-#check pushforwardPullbackTwoSquare
-
 -- use `pushforwardPullbackTwoSquare` to construct this iso.
 def pentagonIso : map u ⋙ pushforward f ≅
   pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) := by

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean

@@ -22,7 +22,7 @@ abbrev Psh (C : Type u) [Category.{v} C] : Type (max u (v + 1)) := Cᵒᵖ ⥤ T
 
 variable {C : Type*} [SmallCategory C] [HasTerminal C]
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 instance cartesianClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) :
     CartesianClosed (Over P) :=

Poly/ForMathlib/CategoryTheory/NatTrans.lean

@@ -18,6 +18,8 @@ variable {K : Type*} [Category K] {D : Type*} [Category D]
 
 namespace NatTrans
 
+open Functor
+
 /-- A natural transformation is cartesian if every commutative square of the following form is
 a pullback.
 ```

Poly/ForMathlib/CategoryTheory/PartialProduct.lean

@@ -53,8 +53,7 @@ structure Fan where
   snd : pullback fst s ⟶ X
 
 theorem Fan.fst_mk {pt : C} (f : pt ⟶ B) (g : pullback f s ⟶ X) :
-    Fan.fst (Fan.mk f g) = f := by
-  rfl
+    Fan.fst (Fan.mk f g) = f := rfl
 
 variable {s X}
 
@@ -84,8 +83,7 @@ def pullbackMap {c' c : Fan s X} (f : c'.pt ⟶ c.pt)
   ((Over.pullback s).map (Over.homMk f (by aesop) : Over.mk (c'.fst) ⟶ Over.mk c.fst)).left
 
 theorem pullbackMap_comparison {P} {c : Fan s X} (f : P ⟶ c.pt) :
-    pullbackMap (c' := Fan.mk (f ≫ c.fst) (comparison f ≫ c.snd)) (c := c) f = comparison f := by
-  rfl
+    pullbackMap (c' := Fan.mk (f ≫ c.fst) (comparison f ≫ c.snd)) (c := c) f = comparison f := rfl
 
 /-- A map to the apex of a partial product cone induces a partial product cone by precomposition. -/
 @[simps]