bump to nightly-2023-05-10-16

mathlib commit leanprover-community/mathlib@cc5dd62

Mathbin/Computability/Halting.lean

@@ -129,9 +129,9 @@ theorem cond {c : α → Bool} {f : α →. σ} {g : α →. σ} (hc : Computabl
 theorem sum_cases {f : α → Sum β γ} {g : α → β →. σ} {h : α → γ →. σ} (hf : Computable f)
     (hg : Partrec₂ g) (hh : Partrec₂ h) : @Partrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
   option_some_iff.1 <|
-    (cond (sum_cases hf (const true).to₂ (const false).to₂)
-          (sum_cases_left hf (option_some_iff.2 hg).to₂ (const Option.none).to₂)
-          (sum_cases_right hf (const Option.none).to₂ (option_some_iff.2 hh).to₂)).of_eq
+    (cond (sum_casesOn hf (const true).to₂ (const false).to₂)
+          (sum_casesOn_left hf (option_some_iff.2 hg).to₂ (const Option.none).to₂)
+          (sum_casesOn_right hf (const Option.none).to₂ (option_some_iff.2 hh).to₂)).of_eq
       fun a => by cases f a <;> simp only [Bool.cond_true, Bool.cond_false]
 #align partrec.sum_cases Partrec.sum_cases
 

Mathbin/Computability/Reduce.lean

@@ -310,8 +310,8 @@ theorem disjoin_manyOneReducible {α β γ} [Primcodable α] [Primcodable β] [P
     {p : α → Prop} {q : β → Prop} {r : γ → Prop} : p ≤₀ r → q ≤₀ r → p ⊕' q ≤₀ r
   | ⟨f, c₁, h₁⟩, ⟨g, c₂, h₂⟩ =>
     ⟨Sum.elim f g,
-      Computable.id.sum_cases (c₁.comp Computable.snd).to₂ (c₂.comp Computable.snd).to₂, fun x => by
-      cases x <;> [apply h₁, apply h₂]⟩
+      Computable.id.sum_casesOn (c₁.comp Computable.snd).to₂ (c₂.comp Computable.snd).to₂, fun x =>
+      by cases x <;> [apply h₁, apply h₂]⟩
 #align disjoin_many_one_reducible disjoin_manyOneReducible
 
 theorem disjoin_le {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop}

Mathbin/MeasureTheory/Decomposition/UnsignedHahn.lean

@@ -35,6 +35,12 @@ namespace MeasureTheory
 
 variable {α : Type _} [MeasurableSpace α] {μ ν : Measure α}
 
+/- warning: measure_theory.hahn_decomposition -> MeasureTheory.hahn_decomposition is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} [_inst_1 : MeasurableSpace.{u1} α] {μ : MeasureTheory.Measure.{u1} α _inst_1} {ν : MeasureTheory.Measure.{u1} α _inst_1} [_inst_2 : MeasureTheory.FiniteMeasure.{u1} α _inst_1 μ] [_inst_3 : MeasureTheory.FiniteMeasure.{u1} α _inst_1 ν], Exists.{succ u1} (Set.{u1} α) (fun (s : Set.{u1} α) => And (MeasurableSet.{u1} α _inst_1 s) (And (forall (t : Set.{u1} α), (MeasurableSet.{u1} α _inst_1 t) -> (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t s) -> (LE.le.{0} ENNReal (Preorder.toLE.{0} ENNReal (PartialOrder.toPreorder.{0} ENNReal (CompleteSemilatticeInf.toPartialOrder.{0} ENNReal (CompleteLattice.toCompleteSemilatticeInf.{0} ENNReal (CompleteLinearOrder.toCompleteLattice.{0} ENNReal ENNReal.completeLinearOrder))))) (coeFn.{succ u1, succ u1} (MeasureTheory.Measure.{u1} α _inst_1) (fun (_x : MeasureTheory.Measure.{u1} α _inst_1) => (Set.{u1} α) -> ENNReal) (MeasureTheory.Measure.instCoeFun.{u1} α _inst_1) ν t) (coeFn.{succ u1, succ u1} (MeasureTheory.Measure.{u1} α _inst_1) (fun (_x : MeasureTheory.Measure.{u1} α _inst_1) => (Set.{u1} α) -> ENNReal) (MeasureTheory.Measure.instCoeFun.{u1} α _inst_1) μ t))) (forall (t : Set.{u1} α), (MeasurableSet.{u1} α _inst_1 t) -> (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) t (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.booleanAlgebra.{u1} α)) s)) -> (LE.le.{0} ENNReal (Preorder.toLE.{0} ENNReal (PartialOrder.toPreorder.{0} ENNReal (CompleteSemilatticeInf.toPartialOrder.{0} ENNReal (CompleteLattice.toCompleteSemilatticeInf.{0} ENNReal (CompleteLinearOrder.toCompleteLattice.{0} ENNReal ENNReal.completeLinearOrder))))) (coeFn.{succ u1, succ u1} (MeasureTheory.Measure.{u1} α _inst_1) (fun (_x : MeasureTheory.Measure.{u1} α _inst_1) => (Set.{u1} α) -> ENNReal) (MeasureTheory.Measure.instCoeFun.{u1} α _inst_1) μ t) (coeFn.{succ u1, succ u1} (MeasureTheory.Measure.{u1} α _inst_1) (fun (_x : MeasureTheory.Measure.{u1} α _inst_1) => (Set.{u1} α) -> ENNReal) (MeasureTheory.Measure.instCoeFun.{u1} α _inst_1) ν t)))))
+but is expected to have type
+  forall {α : Type.{u1}} [_inst_1 : MeasurableSpace.{u1} α] {μ : MeasureTheory.Measure.{u1} α _inst_1} {ν : MeasureTheory.Measure.{u1} α _inst_1} [_inst_2 : MeasureTheory.FiniteMeasure.{u1} α _inst_1 μ] [_inst_3 : MeasureTheory.FiniteMeasure.{u1} α _inst_1 ν], Exists.{succ u1} (Set.{u1} α) (fun (s : Set.{u1} α) => And (MeasurableSet.{u1} α _inst_1 s) (And (forall (t : Set.{u1} α), (MeasurableSet.{u1} α _inst_1 t) -> (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t s) -> (LE.le.{0} ENNReal (Preorder.toLE.{0} ENNReal (PartialOrder.toPreorder.{0} ENNReal (OmegaCompletePartialOrder.toPartialOrder.{0} ENNReal (CompleteLattice.instOmegaCompletePartialOrder.{0} ENNReal (CompleteLinearOrder.toCompleteLattice.{0} ENNReal ENNReal.instCompleteLinearOrderENNReal))))) (MeasureTheory.OuterMeasure.measureOf.{u1} α (MeasureTheory.Measure.toOuterMeasure.{u1} α _inst_1 ν) t) (MeasureTheory.OuterMeasure.measureOf.{u1} α (MeasureTheory.Measure.toOuterMeasure.{u1} α _inst_1 μ) t))) (forall (t : Set.{u1} α), (MeasurableSet.{u1} α _inst_1 t) -> (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) t (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.instBooleanAlgebraSet.{u1} α)) s)) -> (LE.le.{0} ENNReal (Preorder.toLE.{0} ENNReal (PartialOrder.toPreorder.{0} ENNReal (OmegaCompletePartialOrder.toPartialOrder.{0} ENNReal (CompleteLattice.instOmegaCompletePartialOrder.{0} ENNReal (CompleteLinearOrder.toCompleteLattice.{0} ENNReal ENNReal.instCompleteLinearOrderENNReal))))) (MeasureTheory.OuterMeasure.measureOf.{u1} α (MeasureTheory.Measure.toOuterMeasure.{u1} α _inst_1 μ) t) (MeasureTheory.OuterMeasure.measureOf.{u1} α (MeasureTheory.Measure.toOuterMeasure.{u1} α _inst_1 ν) t)))))
+Case conversion may be inaccurate. Consider using '#align measure_theory.hahn_decomposition MeasureTheory.hahn_decompositionₓ'. -/
 /-- **Hahn decomposition theorem** -/
 theorem hahn_decomposition [FiniteMeasure μ] [FiniteMeasure ν] :
     ∃ s,

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "b717570da0467f3f12c1da67e1812d015d9013e6",
+    "rev": "4d2e8d84e3631ed9882d72de5300a707f617ccba",
     "name": "lean3port",
-    "inputRev?": "b717570da0467f3f12c1da67e1812d015d9013e6"}},
+    "inputRev?": "4d2e8d84e3631ed9882d72de5300a707f617ccba"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ab8b90a8c18c410cf369537add98df0dc8f32207",
+    "rev": "48c42c3d75792ae246030cd978a64ff4effc696f",
     "name": "mathlib",
-    "inputRev?": "ab8b90a8c18c410cf369537add98df0dc8f32207"}},
+    "inputRev?": "48c42c3d75792ae246030cd978a64ff4effc696f"}},
   {"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-05-10-12"
+def tag : String := "nightly-2023-05-10-16"
 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"@"b717570da0467f3f12c1da67e1812d015d9013e6"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"4d2e8d84e3631ed9882d72de5300a707f617ccba"
 
 @[default_target]
 lean_lib Mathbin where