bump to nightly-2023-06-10-23

mathlib commit leanprover-community/mathlib@a3e83f0

Mathbin/CategoryTheory/Monoidal/Limits.lean

@@ -37,9 +37,11 @@ variable {J : Type v} [SmallCategory J]
 
 variable {C : Type u} [Category.{v} C] [HasLimits C]
 
+#print CategoryTheory.Limits.limitFunctorial /-
 instance limitFunctorial : Functorial fun F : J ⥤ C => limit F :=
   { Limits.lim with }
 #align category_theory.limits.limit_functorial CategoryTheory.Limits.limitFunctorial
+-/
 
 @[simp]
 theorem limitFunctorial_map {F G : J ⥤ C} (α : F ⟶ G) :
@@ -53,6 +55,7 @@ variable [MonoidalCategory.{v} C]
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print CategoryTheory.Limits.limitLaxMonoidal /-
 @[simps]
 instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F
     where
@@ -108,11 +111,14 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F
     slice_rhs 2 3 => rw [right_unitor_naturality]
     simp
 #align category_theory.limits.limit_lax_monoidal CategoryTheory.Limits.limitLaxMonoidal
+-/
 
+#print CategoryTheory.Limits.limLax /-
 /-- The limit functor `F ↦ limit F` bundled as a lax monoidal functor. -/
 def limLax : LaxMonoidalFunctor (J ⥤ C) C :=
   LaxMonoidalFunctor.of fun F : J ⥤ C => limit F
 #align category_theory.limits.lim_lax CategoryTheory.Limits.limLax
+-/
 
 @[simp]
 theorem limLax_obj (F : J ⥤ C) : limLax.obj F = limit F :=

Mathbin/Data/Polynomial/UnitTrinomial.lean

@@ -37,34 +37,42 @@ section Semiring
 
 variable {R : Type _} [Semiring R] (k m n : ℕ) (u v w : R)
 
+#print Polynomial.trinomial /-
 /-- Shorthand for a trinomial -/
 noncomputable def trinomial :=
   C u * X ^ k + C v * X ^ m + C w * X ^ n
 #align polynomial.trinomial Polynomial.trinomial
+-/
 
 theorem trinomial_def : trinomial k m n u v w = C u * X ^ k + C v * X ^ m + C w * X ^ n :=
   rfl
 #align polynomial.trinomial_def Polynomial.trinomial_def
 
 variable {k m n u v w}
 
+#print Polynomial.trinomial_leading_coeff' /-
 theorem trinomial_leading_coeff' (hkm : k < m) (hmn : m < n) :
     (trinomial k m n u v w).coeff n = w := by
   rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
     if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
 #align polynomial.trinomial_leading_coeff' Polynomial.trinomial_leading_coeff'
+-/
 
+#print Polynomial.trinomial_middle_coeff /-
 theorem trinomial_middle_coeff (hkm : k < m) (hmn : m < n) : (trinomial k m n u v w).coeff m = v :=
   by
   rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
     if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]
 #align polynomial.trinomial_middle_coeff Polynomial.trinomial_middle_coeff
+-/
 
+#print Polynomial.trinomial_trailing_coeff' /-
 theorem trinomial_trailing_coeff' (hkm : k < m) (hmn : m < n) :
     (trinomial k m n u v w).coeff k = u := by
   rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
     if_pos rfl, if_neg hkm.ne, if_neg (hkm.trans hmn).Ne, add_zero, add_zero]
 #align polynomial.trinomial_trailing_coeff' Polynomial.trinomial_trailing_coeff'
+-/
 
 theorem trinomial_natDegree (hkm : k < m) (hmn : m < n) (hw : w ≠ 0) :
     (trinomial k m n u v w).natDegree = n :=
@@ -106,12 +114,14 @@ theorem trinomial_trailingCoeff (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) :
   rw [trailing_coeff, trinomial_nat_trailing_degree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]
 #align polynomial.trinomial_trailing_coeff Polynomial.trinomial_trailingCoeff
 
+#print Polynomial.trinomial_monic /-
 theorem trinomial_monic (hkm : k < m) (hmn : m < n) : (trinomial k m n u v 1).Monic :=
   by
   cases' subsingleton_or_nontrivial R with h h
   · apply Subsingleton.elim
   · exact trinomial_leading_coeff hkm hmn one_ne_zero
 #align polynomial.trinomial_monic Polynomial.trinomial_monic
+-/
 
 theorem trinomial_mirror (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hw : w ≠ 0) :
     (trinomial k m n u v w).mirror = trinomial k (n - m + k) n w v u := by

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "9364104ff3c0e1586d318f07472dbd567ae462fe",
+    "rev": "04e79d197f13f2ab3cffb0360c18155f34468832",
     "name": "lean3port",
-    "inputRev?": "9364104ff3c0e1586d318f07472dbd567ae462fe"}},
+    "inputRev?": "04e79d197f13f2ab3cffb0360c18155f34468832"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "69dc66afc376c286dbf9d8fed5445e952f86bb53",
+    "rev": "5a919533f110b7d76410134a237ee374f24eaaad",
     "name": "mathlib",
-    "inputRev?": "69dc66afc376c286dbf9d8fed5445e952f86bb53"}},
+    "inputRev?": "5a919533f110b7d76410134a237ee374f24eaaad"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-06-10-21"
+def tag : String := "nightly-2023-06-10-23"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"9364104ff3c0e1586d318f07472dbd567ae462fe"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"04e79d197f13f2ab3cffb0360c18155f34468832"
 
 @[default_target]
 lean_lib Mathbin where