bump to nightly-2023-07-23-03

mathlib commit leanprover-community/mathlib@8047de4

Archive/All.lean

@@ -53,5 +53,5 @@ import Archive.Wiedijk100Theorems.PerfectNumbers
 import Archive.Wiedijk100Theorems.SolutionOfCubic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 
-#align_import all from "leanprover-community/mathlib"@"8ea5598db6caeddde6cb734aa179cc2408dbd345"
+#align_import all from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
 

Counterexamples/All.lean

@@ -13,5 +13,5 @@ import Counterexamples.SeminormLatticeNotDistrib
 import Counterexamples.SorgenfreyLine
 import Counterexamples.ZeroDivisorsInAddMonoidAlgebras
 
-#align_import all from "leanprover-community/mathlib"@"8ea5598db6caeddde6cb734aa179cc2408dbd345"
+#align_import all from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
 

Mathbin/All.lean

@@ -3212,5 +3212,5 @@ import Mathbin.Topology.VectorBundle.Basic
 import Mathbin.Topology.VectorBundle.Constructions
 import Mathbin.Topology.VectorBundle.Hom
 
-#align_import all from "leanprover-community/mathlib"@"8ea5598db6caeddde6cb734aa179cc2408dbd345"
+#align_import all from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
 

Mathbin/Order/Irreducible.lean

@@ -6,11 +6,14 @@ Authors: Yaël Dillies
 import Mathbin.Data.Finset.Lattice
 import Mathbin.Data.Fintype.Card
 
-#align_import order.irreducible from "leanprover-community/mathlib"@"bf2428c9486c407ca38b5b3fb10b87dad0bc99fa"
+#align_import order.irreducible from "leanprover-community/mathlib"@"573eea921b01c49712ac02471911df0719297349"
 
 /-!
 # Irreducible and prime elements in an order
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines irreducible and prime elements in an order and shows that in a well-founded
 lattice every element decomposes as a supremum of irreducible elements.
 

Mathbin/Topology/MetricSpace/Basic.lean

@@ -8,7 +8,7 @@ import Mathbin.Topology.Algebra.Order.Compact
 import Mathbin.Topology.MetricSpace.EmetricSpace
 import Mathbin.Topology.Bornology.Constructions
 
-#align_import topology.metric_space.basic from "leanprover-community/mathlib"@"8000bbbe2e9d39b84edb993d88781f536a8a3fa8"
+#align_import topology.metric_space.basic from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
 
 /-!
 # Metric spaces
@@ -667,6 +667,15 @@ theorem ne_of_mem_sphere (h : y ∈ sphere x ε) (hε : ε ≠ 0) : y ≠ x := b
 #align metric.ne_of_mem_sphere Metric.ne_of_mem_sphere
 -/
 
+theorem nonneg_of_mem_sphere (hy : y ∈ sphere x ε) : 0 ≤ ε :=
+  dist_nonneg.trans_eq hy
+#align metric.nonneg_of_mem_sphere Metric.nonneg_of_mem_sphere
+
+@[simp]
+theorem sphere_eq_empty_of_neg (hε : ε < 0) : sphere x ε = ∅ :=
+  Set.eq_empty_iff_forall_not_mem.mpr fun y hy => (nonneg_of_mem_sphere hy).not_lt hε
+#align metric.sphere_eq_empty_of_neg Metric.sphere_eq_empty_of_neg
+
 #print Metric.sphere_eq_empty_of_subsingleton /-
 theorem sphere_eq_empty_of_subsingleton [Subsingleton α] (hε : ε ≠ 0) : sphere x ε = ∅ :=
   Set.eq_empty_iff_forall_not_mem.mpr fun y hy => ne_of_mem_sphere hy hε (Subsingleton.elim _ _)
@@ -699,6 +708,11 @@ theorem closedBall_eq_empty : closedBall x ε = ∅ ↔ ε < 0 := by
 #align metric.closed_ball_eq_empty Metric.closedBall_eq_empty
 -/
 
+/-- Closed balls and spheres coincide when the radius is non-positive -/
+theorem closedBall_eq_sphere_of_nonpos (hε : ε ≤ 0) : closedBall x ε = sphere x ε :=
+  Set.ext fun _ => (hε.trans dist_nonneg).le_iff_eq
+#align metric.closed_ball_eq_sphere_of_nonpos Metric.closedBall_eq_sphere_of_nonpos
+
 #print Metric.ball_subset_closedBall /-
 theorem ball_subset_closedBall : ball x ε ⊆ closedBall x ε := fun y (hy : _ < _) => le_of_lt hy
 #align metric.ball_subset_closed_ball Metric.ball_subset_closedBall
@@ -2351,6 +2365,22 @@ theorem closedBall_prod_same (x : α) (y : β) (r : ℝ) :
 #align closed_ball_prod_same closedBall_prod_same
 -/
 
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+theorem sphere_prod (x : α × β) (r : ℝ) :
+    sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r :=
+  by
+  obtain hr | rfl | hr := lt_trichotomy r 0
+  · simp [hr]
+  · cases x
+    simp_rw [← closed_ball_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
+  · ext ⟨x', y'⟩
+    simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq,
+      max_eq_iff]
+    refine' or_congr (and_congr_right _) ((and_comm' _ _).trans (and_congr_left _))
+    all_goals rintro rfl; rfl
+#align sphere_prod sphere_prod
+
 end Prod
 
 #print uniformContinuous_dist /-
@@ -2692,12 +2722,27 @@ theorem nndist_pi_le_iff {f g : ∀ b, π b} {r : ℝ≥0} :
 #align nndist_pi_le_iff nndist_pi_le_iff
 -/
 
+theorem nndist_pi_lt_iff {f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) :
+    nndist f g < r ↔ ∀ b, nndist (f b) (g b) < r := by
+  simp [nndist_pi_def, Finset.sup_lt_iff (show ⊥ < r from hr)]
+#align nndist_pi_lt_iff nndist_pi_lt_iff
+
+theorem nndist_pi_eq_iff {f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) :
+    nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ b, nndist (f b) (g b) ≤ r :=
+  by
+  rw [eq_iff_le_not_lt, nndist_pi_lt_iff hr, nndist_pi_le_iff, not_forall, and_comm']
+  simp_rw [not_lt, and_congr_left_iff, le_antisymm_iff]
+  intro h
+  refine' exists_congr fun b => _
+  apply (and_iff_right <| h _).symm
+#align nndist_pi_eq_iff nndist_pi_eq_iff
+
 #print dist_pi_lt_iff /-
 theorem dist_pi_lt_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) :
     dist f g < r ↔ ∀ b, dist (f b) (g b) < r :=
   by
   lift r to ℝ≥0 using hr.le
-  simp [dist_pi_def, Finset.sup_lt_iff (show ⊥ < r from hr)]
+  exact nndist_pi_lt_iff hr
 #align dist_pi_lt_iff dist_pi_lt_iff
 -/
 
@@ -2710,6 +2755,13 @@ theorem dist_pi_le_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 ≤ r) :
 #align dist_pi_le_iff dist_pi_le_iff
 -/
 
+theorem dist_pi_eq_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) :
+    dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ b, dist (f b) (g b) ≤ r :=
+  by
+  lift r to ℝ≥0 using hr.le
+  simp_rw [← coe_nndist, NNReal.coe_eq, nndist_pi_eq_iff hr, NNReal.coe_le_coe]
+#align dist_pi_eq_iff dist_pi_eq_iff
+
 #print dist_pi_le_iff' /-
 theorem dist_pi_le_iff' [Nonempty β] {f g : ∀ b, π b} {r : ℝ} :
     dist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r :=
@@ -2796,6 +2848,25 @@ theorem closedBall_pi' [Nonempty β] (x : ∀ b, π b) (r : ℝ) :
 #align closed_ball_pi' closedBall_pi'
 -/
 
+/-- A sphere in a product space is a union of spheres on each component restricted to the closed
+ball. -/
+theorem sphere_pi (x : ∀ b, π b) {r : ℝ} (h : 0 < r ∨ Nonempty β) :
+    sphere x r = (⋃ i : β, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r :=
+  by
+  obtain hr | rfl | hr := lt_trichotomy r 0
+  · simp [hr]
+  · rw [closed_ball_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right_iff_subset]
+    letI := h.resolve_left (lt_irrefl _)
+    inhabit β
+    refine' subset_Union_of_subset default _
+    intro x hx
+    replace hx := hx.le
+    rw [dist_pi_le_iff le_rfl] at hx 
+    exact le_antisymm (hx default) dist_nonneg
+  · ext
+    simp [dist_pi_eq_iff hr, dist_pi_le_iff hr.le]
+#align sphere_pi sphere_pi
+
 #print Fin.nndist_insertNth_insertNth /-
 @[simp]
 theorem Fin.nndist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type _}

README.md

@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`8ea5598db6caeddde6cb734aa179cc2408dbd345`](https://github.com/leanprover-community/mathlib/commit/8ea5598db6caeddde6cb734aa179cc2408dbd345)
+Tracking mathlib commit: [`8047de4d911cdef39c2d646165eea972f7f9f539`](https://github.com/leanprover-community/mathlib/commit/8047de4d911cdef39c2d646165eea972f7f9f539)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "af3675b09c625aaf390b3874cbdac583a0186804",
+    "rev": "88288445cd671d5b4882844bc74595ce65f288e8",
     "name": "lean3port",
-    "inputRev?": "af3675b09c625aaf390b3874cbdac583a0186804"}},
+    "inputRev?": "88288445cd671d5b4882844bc74595ce65f288e8"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "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-07-23-01"
+def tag : String := "nightly-2023-07-23-03"
 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"@"af3675b09c625aaf390b3874cbdac583a0186804"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"88288445cd671d5b4882844bc74595ce65f288e8"
 
 @[default_target]
 lean_lib Mathbin where

upstream-rev

@@ -1 +1 @@
-8ea5598db6caeddde6cb734aa179cc2408dbd345
+8047de4d911cdef39c2d646165eea972f7f9f539