bump to nightly-2023-10-14-06

mathlib commit leanprover-community/mathlib@19c869e

Mathbin/Algebra/Lie/Submodule.lean

@@ -540,15 +540,13 @@ theorem sInf_coe (S : Set (LieSubmodule R L M)) : (↑(sInf S) : Set M) = ⋂ s
 #align lie_submodule.Inf_coe LieSubmodule.sInf_coe
 -/
 
-#print LieSubmodule.sInf_glb /-
 theorem sInf_glb (S : Set (LieSubmodule R L M)) : IsGLB S (sInf S) :=
   by
   have h : ∀ N N' : LieSubmodule R L M, (N : Set M) ≤ N' ↔ N ≤ N' := by intros; rfl
   apply IsGLB.of_image h
   simp only [Inf_coe]
   exact isGLB_biInf
 #align lie_submodule.Inf_glb LieSubmodule.sInf_glb
--/
 
 /-- The set of Lie submodules of a Lie module form a complete lattice.
 

Mathbin/Data/Num/Bitwise.lean

@@ -132,13 +132,13 @@ end PosNum
 
 namespace Num
 
-#print Num.lor /-
+#print OrOp.or /-
 /-- Bitwise "or" for `num`. -/
-def lor : Num → Num → Num
+def or : Num → Num → Num
   | 0, q => q
   | p, 0 => p
   | Pos p, Pos q => pos (p.lor' q)
-#align num.lor Num.lor
+#align num.lor OrOp.or
 -/
 
 #print Num.land /-

Mathbin/Data/Num/Lemmas.lean

@@ -1165,7 +1165,7 @@ theorem bitwise'_to_nat {f : Num → Num → Num} {g : Bool → Bool → Bool} (
 
 #print Num.lor'_to_nat /-
 @[simp, norm_cast]
-theorem lor'_to_nat : ∀ m n, (lor m n : ℕ) = Nat.lor' m n := by
+theorem lor'_to_nat : ∀ m n, (or m n : ℕ) = Nat.lor' m n := by
   apply bitwise_to_nat fun x y => Pos (PosNum.lor x y) <;> intros <;> try cases a <;>
       try cases b <;>
     rfl

Mathbin/MeasureTheory/Constructions/Prod/Integral.lean

@@ -350,15 +350,16 @@ theorem Integrable.integral_norm_prod_right [SigmaFinite μ] ⦃f : α × β →
 #align measure_theory.integrable.integral_norm_prod_right MeasureTheory.Integrable.integral_norm_prod_right
 -/
 
-#print MeasureTheory.integrable_prod_mul /-
-theorem integrable_prod_mul {L : Type _} [IsROrC L] {f : α → L} {g : β → L} (hf : Integrable f μ)
-    (hg : Integrable g ν) : Integrable (fun z : α × β => f z.1 * g z.2) (μ.Prod ν) :=
+#print MeasureTheory.Integrable.prod_mul /-
+theorem MeasureTheory.Integrable.prod_mul {L : Type _} [IsROrC L] {f : α → L} {g : β → L}
+    (hf : Integrable f μ) (hg : Integrable g ν) :
+    Integrable (fun z : α × β => f z.1 * g z.2) (μ.Prod ν) :=
   by
   refine' (integrable_prod_iff _).2 ⟨_, _⟩
   · exact hf.1.fst.mul hg.1.snd
   · exact eventually_of_forall fun x => hg.const_mul (f x)
   · simpa only [norm_mul, integral_mul_left] using hf.norm.mul_const _
-#align measure_theory.integrable_prod_mul MeasureTheory.integrable_prod_mul
+#align measure_theory.integrable_prod_mul MeasureTheory.Integrable.prod_mul
 -/
 
 end

lake-manifest.json

@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "2f4952a4441d938c67e0f40b8a90a85c28c509a8",
+    "rev": "16237a8e73e5b2178e456a6335608fbca53ed4d1",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "2f4952a4441d938c67e0f40b8a90a85c28c509a8",
+    "inputRev?": "16237a8e73e5b2178e456a6335608fbca53ed4d1",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "644ffcede0f3d1da4b7cfc97215cd7ab5e071696",
+    "rev": "c98e6b7f0f028f7958b90fe156a7756f9b7a1939",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "644ffcede0f3d1da4b7cfc97215cd7ab5e071696",
+    "inputRev?": "c98e6b7f0f028f7958b90fe156a7756f9b7a1939",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",

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-10-13-06"
+def tag : String := "nightly-2023-10-14-06"
 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"@"2f4952a4441d938c67e0f40b8a90a85c28c509a8"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"16237a8e73e5b2178e456a6335608fbca53ed4d1"
 
 @[default_target]
 lean_lib Mathbin where