bump to nightly-2023-05-29-00

mathlib commit leanprover-community/mathlib@917c3c0

Mathbin/Algebra/MonoidAlgebra/Grading.lean

@@ -67,12 +67,15 @@ theorem mem_gradeBy_iff (f : M → ι) (i : ι) (a : AddMonoidAlgebra R M) :
     a ∈ gradeBy R f i ↔ (a.support : Set M) ⊆ f ⁻¹' {i} := by rfl
 #align add_monoid_algebra.mem_grade_by_iff AddMonoidAlgebra.mem_gradeBy_iff
 
+#print AddMonoidAlgebra.mem_grade_iff /-
 theorem mem_grade_iff (m : M) (a : AddMonoidAlgebra R M) : a ∈ grade R m ↔ a.support ⊆ {m} :=
   by
   rw [← Finset.coe_subset, Finset.coe_singleton]
   rfl
 #align add_monoid_algebra.mem_grade_iff AddMonoidAlgebra.mem_grade_iff
+-/
 
+#print AddMonoidAlgebra.mem_grade_iff' /-
 theorem mem_grade_iff' (m : M) (a : AddMonoidAlgebra R M) :
     a ∈ grade R m ↔
       a ∈ ((Finsupp.lsingle m : R →ₗ[R] M →₀ R).range : Submodule R (AddMonoidAlgebra R M)) :=
@@ -82,6 +85,7 @@ theorem mem_grade_iff' (m : M) (a : AddMonoidAlgebra R M) :
   intro r
   constructor <;> exact Eq.symm
 #align add_monoid_algebra.mem_grade_iff' AddMonoidAlgebra.mem_grade_iff'
+-/
 
 theorem grade_eq_lsingle_range (m : M) : grade R m = (Finsupp.lsingle m : R →ₗ[R] M →₀ R).range :=
   Submodule.ext (mem_grade_iff' R m)
@@ -221,9 +225,11 @@ theorem GradesBy.decompose_single (m : M) (r : R) :
   decomposeAux_single _ _ _
 #align add_monoid_algebra.grades_by.decompose_single AddMonoidAlgebra.GradesBy.decompose_single
 
+#print AddMonoidAlgebra.grade.gradedAlgebra /-
 instance grade.gradedAlgebra : GradedAlgebra (grade R : ι → Submodule _ _) :=
   AddMonoidAlgebra.gradeBy.gradedAlgebra (AddMonoidHom.id _)
 #align add_monoid_algebra.grade.graded_algebra AddMonoidAlgebra.grade.gradedAlgebra
+-/
 
 -- Lean can't find this later without us repeating it
 instance grade.decomposition : DirectSum.Decomposition (grade R : ι → Submodule _ _) := by

Mathbin/Analysis/Calculus/Deriv/Prod.lean

@@ -57,25 +57,33 @@ variable {G : Type w} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 
 variable {f₂ : 𝕜 → G} {f₂' : G}
 
+#print HasDerivAtFilter.prod /-
 theorem HasDerivAtFilter.prod (hf₁ : HasDerivAtFilter f₁ f₁' x L)
     (hf₂ : HasDerivAtFilter f₂ f₂' x L) : HasDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁', f₂') x L :=
   hf₁.Prod hf₂
 #align has_deriv_at_filter.prod HasDerivAtFilter.prod
+-/
 
+#print HasDerivWithinAt.prod /-
 theorem HasDerivWithinAt.prod (hf₁ : HasDerivWithinAt f₁ f₁' s x)
     (hf₂ : HasDerivWithinAt f₂ f₂' s x) : HasDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') s x :=
   hf₁.Prod hf₂
 #align has_deriv_within_at.prod HasDerivWithinAt.prod
+-/
 
+#print HasDerivAt.prod /-
 theorem HasDerivAt.prod (hf₁ : HasDerivAt f₁ f₁' x) (hf₂ : HasDerivAt f₂ f₂' x) :
     HasDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x :=
   hf₁.Prod hf₂
 #align has_deriv_at.prod HasDerivAt.prod
+-/
 
+#print HasStrictDerivAt.prod /-
 theorem HasStrictDerivAt.prod (hf₁ : HasStrictDerivAt f₁ f₁' x) (hf₂ : HasStrictDerivAt f₂ f₂' x) :
     HasStrictDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x :=
   hf₁.Prod hf₂
 #align has_strict_deriv_at.prod HasStrictDerivAt.prod
+-/
 
 end CartesianProduct
 

Mathbin/Data/Set/Intervals/ProjIcc.lean

@@ -167,13 +167,13 @@ theorem IccExtend_of_mem (f : Icc a b → β) (hx : x ∈ Icc a b) : IccExtend h
 #align set.Icc_extend_of_mem Set.IccExtend_of_mem
 
 @[simp]
-theorem Icc_extend_coe (f : Icc a b → β) (x : Icc a b) : IccExtend h f x = f x :=
+theorem IccExtend_val (f : Icc a b → β) (x : Icc a b) : IccExtend h f x = f x :=
   congr_arg f <| projIcc_val h x
-#align set.Icc_extend_coe Set.Icc_extend_coe
+#align set.Icc_extend_coe Set.IccExtend_val
 
 /-- If `f : α → β` is a constant both on $(-∞, a]$ and on $[b, +∞)$, then the extension of this
 function from $[a, b]$ to the whole line is equal to the original function. -/
-theorem iccExtend_eq_self (f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀ x, b < x → f x = f b) :
+theorem IccExtend_eq_self (f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀ x, b < x → f x = f b) :
     IccExtend h (f ∘ coe) = f := by
   ext x
   cases' lt_or_le x a with hxa hax
@@ -182,7 +182,7 @@ theorem iccExtend_eq_self (f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀
     · lift x to Icc a b using ⟨hax, hxb⟩
       rw [Icc_extend_coe]
     · simp [Icc_extend_of_right_le _ _ hbx.le, hb x hbx]
-#align set.Icc_extend_eq_self Set.iccExtend_eq_self
+#align set.Icc_extend_eq_self Set.IccExtend_eq_self
 
 end Set
 

Mathbin/MeasureTheory/Function/SimpleFuncDenseLp.lean

@@ -308,7 +308,7 @@ theorem exists_forall_norm_le (f : α →ₛ F) : ∃ C, ∀ x, ‖f x‖ ≤ C
 #align measure_theory.simple_func.exists_forall_norm_le MeasureTheory.SimpleFunc.exists_forall_norm_le
 
 theorem memℒp_zero (f : α →ₛ E) (μ : Measure α) : Memℒp f 0 μ :=
-  memℒp_zero_iff_aEStronglyMeasurable.mpr f.AEStronglyMeasurable
+  memℒp_zero_iff_aestronglyMeasurable.mpr f.AEStronglyMeasurable
 #align measure_theory.simple_func.mem_ℒp_zero MeasureTheory.SimpleFunc.memℒp_zero
 
 theorem memℒp_top (f : α →ₛ E) (μ : Measure α) : Memℒp f ∞ μ :=

Mathbin/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -1920,11 +1920,11 @@ theorem aestronglyMeasurable_const_smul_iff (c : G) :
   ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul' c⁻¹, fun h => h.const_smul c⟩
 #align ae_strongly_measurable_const_smul_iff aestronglyMeasurable_const_smul_iff
 
-theorem IsUnit.aEStronglyMeasurable_const_smul_iff {c : M} (hc : IsUnit c) :
+theorem IsUnit.aestronglyMeasurable_const_smul_iff {c : M} (hc : IsUnit c) :
     AEStronglyMeasurable (fun x => c • f x) μ ↔ AEStronglyMeasurable f μ :=
   let ⟨u, hu⟩ := hc
   hu ▸ aestronglyMeasurable_const_smul_iff u
-#align is_unit.ae_strongly_measurable_const_smul_iff IsUnit.aEStronglyMeasurable_const_smul_iff
+#align is_unit.ae_strongly_measurable_const_smul_iff IsUnit.aestronglyMeasurable_const_smul_iff
 
 theorem aestronglyMeasurable_const_smul_iff₀ {c : G₀} (hc : c ≠ 0) :
     AEStronglyMeasurable (fun x => c • f x) μ ↔ AEStronglyMeasurable f μ :=

Mathbin/Topology/Homotopy/Basic.lean

@@ -194,7 +194,7 @@ theorem extend_apply_of_one_le (F : Homotopy f₀ f₁) {t : ℝ} (ht : 1 ≤ t)
 
 @[simp]
 theorem extend_apply_coe (F : Homotopy f₀ f₁) (t : I) (x : X) : F.extend t x = F (t, x) :=
-  ContinuousMap.congr_fun (Set.Icc_extend_coe (zero_le_one' ℝ) F.curry t) x
+  ContinuousMap.congr_fun (Set.IccExtend_val (zero_le_one' ℝ) F.curry t) x
 #align continuous_map.homotopy.extend_apply_coe ContinuousMap.Homotopy.extend_apply_coe
 
 @[simp]

Mathbin/Topology/PathConnected.lean

@@ -288,7 +288,7 @@ theorem extend_one : γ.extend 1 = y := by simp
 @[simp]
 theorem extend_extends' {X : Type _} [TopologicalSpace X] {a b : X} (γ : Path a b)
     (t : (Icc 0 1 : Set ℝ)) : γ.extend t = γ t :=
-  Icc_extend_coe _ γ t
+  IccExtend_val _ γ t
 #align path.extend_extends' Path.extend_extends'
 
 #print Path.extend_range /-

Mathbin/Topology/Separation.lean

@@ -1592,11 +1592,13 @@ theorem Continuous.closedEmbedding [CompactSpace α] [T2Space β] {f : α → β
 #align continuous.closed_embedding Continuous.closedEmbedding
 -/
 
+#print QuotientMap.of_surjective_continuous /-
 /-- A surjective continuous map from a compact space to a Hausdorff space is a quotient map. -/
 theorem QuotientMap.of_surjective_continuous [CompactSpace α] [T2Space β] {f : α → β}
     (hsurj : Surjective f) (hcont : Continuous f) : QuotientMap f :=
   hcont.IsClosedMap.to_quotientMap hcont hsurj
 #align quotient_map.of_surjective_continuous QuotientMap.of_surjective_continuous
+-/
 
 section
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "bfba4b488b1bcc2230b173c4e61d9049342c42a6",
+    "rev": "52949e686fe7d17c68a3b3a859ef113b90069d6c",
     "name": "lean3port",
-    "inputRev?": "bfba4b488b1bcc2230b173c4e61d9049342c42a6"}},
+    "inputRev?": "52949e686fe7d17c68a3b3a859ef113b90069d6c"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "b7597898e5628c388bd2e33fca61e5229836f83c",
+    "rev": "e7643d6ca5137dc5a70caed6a972d462ccfff2d7",
     "name": "mathlib",
-    "inputRev?": "b7597898e5628c388bd2e33fca61e5229836f83c"}},
+    "inputRev?": "e7643d6ca5137dc5a70caed6a972d462ccfff2d7"}},
   {"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-28-22"
+def tag : String := "nightly-2023-05-29-00"
 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"@"bfba4b488b1bcc2230b173c4e61d9049342c42a6"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"52949e686fe7d17c68a3b3a859ef113b90069d6c"
 
 @[default_target]
 lean_lib Mathbin where