bump to nightly-2023-08-18-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/LinearAlgebra/BilinearForm/TensorProduct.lean

@@ -52,14 +52,12 @@ def tensorDistrib : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm
 #align bilin_form.tensor_distrib BilinForm.tensorDistrib
 -/
 
-#print BilinForm.tensorDistrib_tmul /-
 @[simp]
 theorem tensorDistrib_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂)
     (m₁' : M₁) (m₂' : M₂) :
     tensorDistrib (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' :=
   rfl
-#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmul
--/
+#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ
 
 #print BilinForm.tmul /-
 /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/

Mathbin/MeasureTheory/Function/LpSpace.lean

@@ -933,14 +933,14 @@ theorem norm_indicatorConstLp' (hp_pos : p ≠ 0) (hμs_pos : μ s ≠ 0) :
 #align measure_theory.norm_indicator_const_Lp' MeasureTheory.norm_indicatorConstLp'
 -/
 
-#print MeasureTheory.indicatorConst_empty /-
+#print MeasureTheory.indicatorConstLp_empty /-
 @[simp]
-theorem indicatorConst_empty : indicatorConstLp p MeasurableSet.empty (by simp : μ ∅ ≠ ∞) c = 0 :=
+theorem indicatorConstLp_empty : indicatorConstLp p MeasurableSet.empty (by simp : μ ∅ ≠ ∞) c = 0 :=
   by
   rw [Lp.eq_zero_iff_ae_eq_zero]
   convert indicator_const_Lp_coe_fn
   simp [Set.indicator_empty']
-#align measure_theory.indicator_const_empty MeasureTheory.indicatorConst_empty
+#align measure_theory.indicator_const_empty MeasureTheory.indicatorConstLp_empty
 -/
 
 #print MeasureTheory.memℒp_add_of_disjoint /-

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "2d52e7090cb49f39d43b428c965208b96dda89f0",
+    "rev": "1419dd54a43fb3870f9dc358579cef35f55ac424",
     "name": "lean3port",
-    "inputRev?": "2d52e7090cb49f39d43b428c965208b96dda89f0"}},
+    "inputRev?": "1419dd54a43fb3870f9dc358579cef35f55ac424"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ae74c2e545c4f18cea002d8c25b12b0ed38d2fcf",
+    "rev": "fb232849b87afc525453e515a23a2677710a1739",
     "name": "mathlib",
-    "inputRev?": "ae74c2e545c4f18cea002d8c25b12b0ed38d2fcf"}},
+    "inputRev?": "fb232849b87afc525453e515a23a2677710a1739"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
@@ -40,6 +40,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8",
+    "rev": "8b864260672b21d964d79ecb2376e01d0eab9f5b",
     "name": "std",
     "inputRev?": "main"}}]}

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-08-18-07"
+def tag : String := "nightly-2023-08-18-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"2d52e7090cb49f39d43b428c965208b96dda89f0"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"1419dd54a43fb3870f9dc358579cef35f55ac424"
 
 @[default_target]
 lean_lib Mathbin where