bump to nightly-2023-05-03-04

mathlib commit leanprover-community/mathlib@36b8aa6

Mathbin/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -319,7 +319,7 @@ theorem id_eq_path_refl (x : FundamentalGroupoid X) : 𝟙 x = ⟦Path.refl x⟧
 
 /-- The functor sending a topological space `X` to its fundamental groupoid.
 -/
-def fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.GroupoidCat
+def fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd
     where
   obj X := { α := FundamentalGroupoid X }
   map X Y f :=

Mathbin/AlgebraicTopology/FundamentalGroupoid/Product.lean

@@ -75,7 +75,7 @@ def piToPiTop : (∀ i, πₓ (X i)) ⥤ πₓ (TopCat.of (∀ i, X i))
 of the induced projections. This shows that `fundamental_groupoid_functor` preserves products.
 -/
 @[simps]
-def piIso : CategoryTheory.GroupoidCat.of (∀ i : I, πₓ (X i)) ≅ πₓ (TopCat.of (∀ i, X i))
+def piIso : CategoryTheory.Grpd.of (∀ i : I, πₓ (X i)) ≅ πₓ (TopCat.of (∀ i, X i))
     where
   Hom := piToPiTop X
   inv := CategoryTheory.Functor.pi' (proj X)
@@ -112,8 +112,7 @@ theorem coneDiscreteComp_obj_mapCone :
 
 /-- This is `pi_iso.inv` as a cone morphism (in fact, isomorphism) -/
 def piTopToPiCone :
-    Limits.Fan.mk (πₓ (TopCat.of (∀ i, X i))) (proj X) ⟶
-      GroupoidCat.piLimitFan fun i : I => πₓ (X i)
+    Limits.Fan.mk (πₓ (TopCat.of (∀ i, X i))) (proj X) ⟶ Grpd.piLimitFan fun i : I => πₓ (X i)
     where Hom := CategoryTheory.Functor.pi' (proj X)
 #align fundamental_groupoid_functor.pi_Top_to_pi_cone FundamentalGroupoidFunctor.piTopToPiCone
 
@@ -192,7 +191,7 @@ theorem prodToProdTop_map {x₀ x₁ : πₓ A} {y₀ y₁ : πₓ B} (p₀ : x
 of the induced left and right projections.
 -/
 @[simps]
-def prodIso : CategoryTheory.GroupoidCat.of (πₓ A × πₓ B) ≅ πₓ (TopCat.of (A × B))
+def prodIso : CategoryTheory.Grpd.of (πₓ A × πₓ B) ≅ πₓ (TopCat.of (A × B))
     where
   Hom := prodToProdTop A B
   inv := (projLeft A B).prod' (projRight A B)

Mathbin/Analysis/Convex/Complex.lean

@@ -19,34 +19,82 @@ are all convex over ℝ.
 -/
 
 
+/- warning: convex_halfspace_re_lt -> convex_halfspace_re_lt is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.hasLt (Complex.re c) r))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.instLTReal (Complex.re c) r))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_re_lt convex_halfspace_re_ltₓ'. -/
 theorem convex_halfspace_re_lt (r : ℝ) : Convex ℝ { c : ℂ | c.re < r } :=
   convex_halfspace_lt (IsLinearMap.mk Complex.add_re Complex.smul_re) _
 #align convex_halfspace_re_lt convex_halfspace_re_lt
 
+/- warning: convex_halfspace_re_le -> convex_halfspace_re_le is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.hasLe (Complex.re c) r))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.instLEReal (Complex.re c) r))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_re_le convex_halfspace_re_leₓ'. -/
 theorem convex_halfspace_re_le (r : ℝ) : Convex ℝ { c : ℂ | c.re ≤ r } :=
   convex_halfspace_le (IsLinearMap.mk Complex.add_re Complex.smul_re) _
 #align convex_halfspace_re_le convex_halfspace_re_le
 
+/- warning: convex_halfspace_re_gt -> convex_halfspace_re_gt is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.hasLt r (Complex.re c)))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.instLTReal r (Complex.re c)))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_re_gt convex_halfspace_re_gtₓ'. -/
 theorem convex_halfspace_re_gt (r : ℝ) : Convex ℝ { c : ℂ | r < c.re } :=
   convex_halfspace_gt (IsLinearMap.mk Complex.add_re Complex.smul_re) _
 #align convex_halfspace_re_gt convex_halfspace_re_gt
 
+/- warning: convex_halfspace_re_ge -> convex_halfspace_re_ge is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.hasLe r (Complex.re c)))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.instLEReal r (Complex.re c)))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_re_ge convex_halfspace_re_geₓ'. -/
 theorem convex_halfspace_re_ge (r : ℝ) : Convex ℝ { c : ℂ | r ≤ c.re } :=
   convex_halfspace_ge (IsLinearMap.mk Complex.add_re Complex.smul_re) _
 #align convex_halfspace_re_ge convex_halfspace_re_ge
 
+/- warning: convex_halfspace_im_lt -> convex_halfspace_im_lt is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.hasLt (Complex.im c) r))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.instLTReal (Complex.im c) r))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_im_lt convex_halfspace_im_ltₓ'. -/
 theorem convex_halfspace_im_lt (r : ℝ) : Convex ℝ { c : ℂ | c.im < r } :=
   convex_halfspace_lt (IsLinearMap.mk Complex.add_im Complex.smul_im) _
 #align convex_halfspace_im_lt convex_halfspace_im_lt
 
+/- warning: convex_halfspace_im_le -> convex_halfspace_im_le is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.hasLe (Complex.im c) r))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.instLEReal (Complex.im c) r))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_im_le convex_halfspace_im_leₓ'. -/
 theorem convex_halfspace_im_le (r : ℝ) : Convex ℝ { c : ℂ | c.im ≤ r } :=
   convex_halfspace_le (IsLinearMap.mk Complex.add_im Complex.smul_im) _
 #align convex_halfspace_im_le convex_halfspace_im_le
 
+/- warning: convex_halfspace_im_gt -> convex_halfspace_im_gt is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.hasLt r (Complex.im c)))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LT.lt.{0} Real Real.instLTReal r (Complex.im c)))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_im_gt convex_halfspace_im_gtₓ'. -/
 theorem convex_halfspace_im_gt (r : ℝ) : Convex ℝ { c : ℂ | r < c.im } :=
   convex_halfspace_gt (IsLinearMap.mk Complex.add_im Complex.smul_im) _
 #align convex_halfspace_im_gt convex_halfspace_im_gt
 
+/- warning: convex_halfspace_im_ge -> convex_halfspace_im_ge is a dubious translation:
+lean 3 declaration is
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (AddCommGroup.toAddCommMonoid.{0} Complex Complex.addCommGroup) (Complex.hasSmul.{0} Real (Mul.toSMul.{0} Real Real.hasMul)) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.hasLe r (Complex.im c)))
+but is expected to have type
+  forall (r : Real), Convex.{0, 0} Real Complex Real.orderedSemiring (NonUnitalNonAssocSemiring.toAddCommMonoid.{0} Complex (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (NonAssocRing.toNonUnitalNonAssocRing.{0} Complex (Ring.toNonAssocRing.{0} Complex Complex.instRingComplex)))) (Complex.instSMulComplex.{0} Real (Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring (Algebra.id.{0} Real Real.instCommSemiringReal))) (setOf.{0} Complex (fun (c : Complex) => LE.le.{0} Real Real.instLEReal r (Complex.im c)))
+Case conversion may be inaccurate. Consider using '#align convex_halfspace_im_ge convex_halfspace_im_geₓ'. -/
 theorem convex_halfspace_im_ge (r : ℝ) : Convex ℝ { c : ℂ | r ≤ c.im } :=
   convex_halfspace_ge (IsLinearMap.mk Complex.add_im Complex.smul_im) _
 #align convex_halfspace_im_ge convex_halfspace_im_ge