bump to nightly-2023-05-09-13

mathlib commit leanprover-community/mathlib@d4437c6

Mathbin/Algebra/BigOperators/Fin.lean

@@ -554,7 +554,7 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
           replace this := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
           rw [← Fin.snoc_init_self f]
           simp (config := { singlePass := true }) only [← Fin.snoc_init_self n]
-          simp_rw [Fin.snoc_cast_succ, Fin.init_snoc, Fin.snoc_last, Fin.snoc_init_self n]
+          simp_rw [Fin.snoc_castSucc, Fin.init_snoc, Fin.snoc_last, Fin.snoc_init_self n]
           exact this
         intro n nn f fn
         cases nn

Mathbin/CategoryTheory/Extensive.lean

@@ -495,7 +495,7 @@ def finitaryExtensiveTopAux (Z : TopCat.{u}) (f : Z ⟶ TopCat.of (Sum PUnit.{u
 
 instance : FinitaryExtensive TopCat.{u} :=
   by
-  rw [finitary_extensive_iff_of_is_terminal TopCat.{u} _ TopCat.isTerminalPunit _
+  rw [finitary_extensive_iff_of_is_terminal TopCat.{u} _ TopCat.isTerminalPUnit _
       (TopCat.binaryCofanIsColimit _ _)]
   apply
     binary_cofan.is_van_kampen_mk _ _ (fun X Y => TopCat.binaryCofanIsColimit X Y) _

Mathbin/CategoryTheory/Subobject/Basic.lean

@@ -1002,7 +1002,7 @@ section Exists
 
 variable [HasImages C]
 
-#print CategoryTheory.Subobject.exists_ /-
+#print CategoryTheory.Subobject.exists /-
 /-- The functor from subobjects of `X` to subobjects of `Y` given by
 sending the subobject `S` to its "image" under `f`, usually denoted $\exists_f$.
 For instance, when `C` is the category of types,
@@ -1011,15 +1011,15 @@ viewing `subobject X` as `set X` this is just `set.image f`.
 This functor is left adjoint to the `pullback f` functor (shown in `exists_pullback_adj`)
 provided both are defined, and generalises the `map f` functor, again provided it is defined.
 -/
-def exists_ (f : X ⟶ Y) : Subobject X ⥤ Subobject Y :=
-  lower (MonoOver.exists_ f)
-#align category_theory.subobject.exists CategoryTheory.Subobject.exists_
+def exists (f : X ⟶ Y) : Subobject X ⥤ Subobject Y :=
+  lower (MonoOver.exists f)
+#align category_theory.subobject.exists CategoryTheory.Subobject.exists
 -/
 
 #print CategoryTheory.Subobject.exists_iso_map /-
 /-- When `f : X ⟶ Y` is a monomorphism, `exists f` agrees with `map f`.
 -/
-theorem exists_iso_map (f : X ⟶ Y) [Mono f] : exists_ f = map f :=
+theorem exists_iso_map (f : X ⟶ Y) [Mono f] : exists f = map f :=
   lower_iso _ _ (MonoOver.existsIsoMap f)
 #align category_theory.subobject.exists_iso_map CategoryTheory.Subobject.exists_iso_map
 -/
@@ -1028,7 +1028,7 @@ theorem exists_iso_map (f : X ⟶ Y) [Mono f] : exists_ f = map f :=
 /-- `exists f : subobject X ⥤ subobject Y` is
 left adjoint to `pullback f : subobject Y ⥤ subobject X`.
 -/
-def existsPullbackAdj (f : X ⟶ Y) [HasPullbacks C] : exists_ f ⊣ pullback f :=
+def existsPullbackAdj (f : X ⟶ Y) [HasPullbacks C] : exists f ⊣ pullback f :=
   lowerAdjunction (MonoOver.existsPullbackAdj f)
 #align category_theory.subobject.exists_pullback_adj CategoryTheory.Subobject.existsPullbackAdj
 -/

Mathbin/CategoryTheory/Subobject/FactorThru.lean

@@ -266,21 +266,21 @@ theorem factorThru_zero [HasZeroMorphisms C] {X Y : C} {P : Subobject Y}
     (h : P.Factors (0 : X ⟶ Y)) : P.factorThru 0 h = 0 := by simp
 #align category_theory.subobject.factor_thru_zero CategoryTheory.Subobject.factorThru_zero
 
-/- warning: category_theory.subobject.factor_thru_of_le -> CategoryTheory.Subobject.factorThru_ofLe is a dubious translation:
+/- warning: category_theory.subobject.factor_thru_of_le -> CategoryTheory.Subobject.factorThru_ofLE is a dubious translation:
 lean 3 declaration is
   forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] {Y : C} {Z : C} {P : CategoryTheory.Subobject.{u1, u2} C _inst_1 Y} {Q : CategoryTheory.Subobject.{u1, u2} C _inst_1 Y} {f : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) Z Y} (h : LE.le.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.toLE.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.Subobject.partialOrder.{u2, u1} C _inst_1 Y))) P Q) (w : CategoryTheory.Subobject.Factors.{u1, u2} C _inst_1 Z Y P f), Eq.{succ u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) Z ((fun (a : Type.{max u2 u1}) (b : Type.{u2}) [self : HasLiftT.{succ (max u2 u1), succ u2} a b] => self.0) (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (HasLiftT.mk.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (CoeTCₓ.coe.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (coeBase.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (CategoryTheory.Subobject.hasCoe.{u1, u2} C _inst_1 Y)))) Q)) (CategoryTheory.Subobject.factorThru.{u1, u2} C _inst_1 Z Y Q f (CategoryTheory.Subobject.factors_of_le.{u1, u2} C _inst_1 Y Z P Q f h w)) (CategoryTheory.CategoryStruct.comp.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1) Z ((fun (a : Type.{max u2 u1}) (b : Type.{u2}) [self : HasLiftT.{succ (max u2 u1), succ u2} a b] => self.0) (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (HasLiftT.mk.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (CoeTCₓ.coe.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (coeBase.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (CategoryTheory.Subobject.hasCoe.{u1, u2} C _inst_1 Y)))) P) ((fun (a : Type.{max u2 u1}) (b : Type.{u2}) [self : HasLiftT.{succ (max u2 u1), succ u2} a b] => self.0) (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (HasLiftT.mk.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (CoeTCₓ.coe.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (coeBase.{succ (max u2 u1), succ u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) C (CategoryTheory.Subobject.hasCoe.{u1, u2} C _inst_1 Y)))) Q) (CategoryTheory.Subobject.factorThru.{u1, u2} C _inst_1 Z Y P f w) (CategoryTheory.Subobject.ofLE.{u1, u2} C _inst_1 Y P Q h))
 but is expected to have type
   forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] {Y : C} {Z : C} {P : CategoryTheory.Subobject.{u1, u2} C _inst_1 Y} {Q : CategoryTheory.Subobject.{u1, u2} C _inst_1 Y} {f : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) Z Y} (h : LE.le.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.toLE.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 Y))) P Q) (w : CategoryTheory.Subobject.Factors.{u1, u2} C _inst_1 Z Y P f), Eq.{succ u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) Z (Prefunctor.obj.{max (succ u2) (succ u1), succ u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.Category.toCategoryStruct.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 Y))))) C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) (CategoryTheory.Functor.toPrefunctor.{max u2 u1, u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 Y))) C _inst_1 (CategoryTheory.Subobject.underlying.{u1, u2} C _inst_1 Y)) Q)) (CategoryTheory.Subobject.factorThru.{u1, u2} C _inst_1 Z Y Q f (CategoryTheory.Subobject.factors_of_le.{u1, u2} C _inst_1 Y Z P Q f h w)) (CategoryTheory.CategoryStruct.comp.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1) Z (Prefunctor.obj.{max (succ u2) (succ u1), succ u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.Category.toCategoryStruct.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 Y))))) C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) (CategoryTheory.Functor.toPrefunctor.{max u2 u1, u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 Y))) C _inst_1 (CategoryTheory.Subobject.underlying.{u1, u2} C _inst_1 Y)) P) (Prefunctor.obj.{max (succ u2) (succ u1), succ u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.Category.toCategoryStruct.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 Y))))) C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) (CategoryTheory.Functor.toPrefunctor.{max u2 u1, u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 Y) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 Y))) C _inst_1 (CategoryTheory.Subobject.underlying.{u1, u2} C _inst_1 Y)) Q) (CategoryTheory.Subobject.factorThru.{u1, u2} C _inst_1 Z Y P f w) (CategoryTheory.Subobject.ofLE.{u1, u2} C _inst_1 Y P Q h))
-Case conversion may be inaccurate. Consider using '#align category_theory.subobject.factor_thru_of_le CategoryTheory.Subobject.factorThru_ofLeₓ'. -/
+Case conversion may be inaccurate. Consider using '#align category_theory.subobject.factor_thru_of_le CategoryTheory.Subobject.factorThru_ofLEₓ'. -/
 -- `h` is an explicit argument here so we can use
 -- `rw factor_thru_le h`, obtaining a subgoal `P.factors f`.
 -- (While the reverse direction looks plausible as a simp lemma, it seems to be unproductive.)
-theorem factorThru_ofLe {Y Z : C} {P Q : Subobject Y} {f : Z ⟶ Y} (h : P ≤ Q) (w : P.Factors f) :
+theorem factorThru_ofLE {Y Z : C} {P Q : Subobject Y} {f : Z ⟶ Y} (h : P ≤ Q) (w : P.Factors f) :
     Q.factorThru f (factors_of_le f h w) = P.factorThru f w ≫ ofLE P Q h :=
   by
   ext
   simp
-#align category_theory.subobject.factor_thru_of_le CategoryTheory.Subobject.factorThru_ofLe
+#align category_theory.subobject.factor_thru_of_le CategoryTheory.Subobject.factorThru_ofLE
 
 section Preadditive