Update lean-toolchain for leanprover/lean4#11220

Author: leanprover-community-mathlib4-bot

Mathlib/NumberTheory/SumTwoSquares.lean

@@ -222,7 +222,7 @@ theorem Nat.eq_sq_add_sq_iff {n : ℕ} :
   refine eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩
   · have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
     have : q ∣ b → q ∈ b.primeFactors := by grind [mem_primeFactors]
-    grind [padicValNat.mul, padicValNat.pow,
+    grind (splits := 10) [padicValNat.mul, padicValNat.pow,
       padicValNat.eq_zero_of_not_dvd, mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one]
   · obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := sq_mul_squarefree_of_pos hn₀
     refine ⟨a, b, hab.symm, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hb

Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean

@@ -107,7 +107,7 @@ where `<option>` contains `maxHeartbeats`, then it returns
 
 Otherwise, it returns `none`.
 -/
-def getSetOptionMaxHeartbeatsComment : Syntax → Option (Name × Nat × Substring)
+def getSetOptionMaxHeartbeatsComment : Syntax → Option (Name × Nat × Substring.Raw)
   | stx@`(command|set_option $mh $n:num in $_) =>
     let opt := mh.getId
     if !opt.components.contains `maxHeartbeats then

Mathlib/Tactic/Linter/Header.lean

@@ -97,7 +97,7 @@ In conclusion, either the parsing is successful, and the linter can continue wit
 or the parsing is not successful and the linter will flag a missing module doc-string!
 -/
 def parseUpToHere (pos : String.Pos.Raw) (post : String := "") : CommandElabM Syntax := do
-  let upToHere : Substring := { str := (← getFileMap).source, startPos := ⟨0⟩, stopPos := pos }
+  let upToHere : Substring.Raw := { str := (← getFileMap).source, startPos := ⟨0⟩, stopPos := pos }
   -- Append a further string after the content of `upToHere`.
   Parser.testParseModule (← getEnv) "linter.style.header" (upToHere.toString ++ post)
 

Mathlib/Tactic/Linter/PPRoundtrip.lean

@@ -84,7 +84,7 @@ def posToShiftedPos (lths : Array Nat) (diff : Nat) : Nat := Id.run do
 
 /-- `zoomString str centre offset` returns the substring of `str` consisting of the `offset`
 characters around the `centre`th character. -/
-def zoomString (str : String) (centre offset : Nat) : Substring :=
+def zoomString (str : String) (centre offset : Nat) : Substring.Raw :=
   { str := str, startPos := ⟨centre - offset⟩, stopPos := ⟨centre + offset⟩ }
 
 /-- `capSourceInfo s p` "shortens" all end-position information in the `SourceInfo` `s` to be

Mathlib/Tactic/Simps/Basic.lean

@@ -507,7 +507,7 @@ This is checked by inspecting whether the first character of the remaining part
 
 We use this variant because the latter is often a different field with an auto-generated name.
 -/
-private def dropPrefixIfNotNumber? (s : String) (pre : String) : Option Substring := do
+private def dropPrefixIfNotNumber? (s : String) (pre : String) : Option Substring.Raw := do
   let ret ← s.dropPrefix? pre
   -- flag is true when the remaining part is nonempty and starts with a digit.
   let flag := ret.toString.toList.head?.elim false Char.isDigit

Mathlib/Tactic/ToExpr.lean

@@ -23,7 +23,7 @@ instance [ToLevel.{u}] : ToExpr PUnit.{u+1} where
   toTypeExpr := mkConst ``PUnit [toLevel.{u+1}]
 
 deriving instance ToExpr for String.Pos.Raw
-deriving instance ToExpr for Substring
+deriving instance ToExpr for Substring.Raw
 deriving instance ToExpr for SourceInfo
 deriving instance ToExpr for Syntax
 

Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

@@ -594,6 +594,10 @@ theorem isBounded_iff {s : Set α} :
   rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
     compl_compl]
 
+lemma boundedSpace_iff : BoundedSpace α ↔ ∃ C, ∀ a b : α, dist a b ≤ C := by
+  rw [← isBounded_univ, Metric.isBounded_iff]
+  simp
+
 theorem isBounded_iff_eventually {s : Set α} :
     IsBounded s ↔ ∀ᶠ C in atTop, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C :=
   isBounded_iff.trans
@@ -610,6 +614,13 @@ theorem isBounded_iff_nndist {s : Set α} :
   simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist,
     NNReal.coe_mk, exists_prop]
 
+lemma boundedSpace_iff_nndist : BoundedSpace α ↔ ∃ C, ∀ a b : α, nndist a b ≤ C := by
+  rw [← isBounded_univ, Metric.isBounded_iff_nndist]
+  simp
+
+lemma boundedSpace_iff_edist : BoundedSpace α ↔ ∃ C : ℝ≥0, ∀ a b : α, edist a b ≤ C := by
+  simp [Metric.boundedSpace_iff_nndist]
+
 theorem toUniformSpace_eq :
     ‹PseudoMetricSpace α›.toUniformSpace = .ofDist dist dist_self dist_comm dist_triangle :=
   UniformSpace.ext PseudoMetricSpace.uniformity_dist

Mathlib/Util/Superscript.lean

@@ -148,7 +148,7 @@ partial def scriptFnNoAntiquot (m : Mapping) (errorMsg : String) (p : ParserFn)
     if s.hasError then return s
     let rec
     /-- Applies the alignment mapping to a `Substring`. -/
-    alignSubstr : Substring → Substring
+    alignSubstr : Substring.Raw → Substring.Raw
       | ⟨_newStr, start, stop⟩ => c.substring (align start) (align stop),
     /-- Applies the alignment mapping to a `SourceInfo`. -/
     alignInfo : SourceInfo → SourceInfo

lake-manifest.json

@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
+   "rev": "9ca66a6f83caf151b447a9102554c8eccf33c70f",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.77",
+   "inputRev": "v0.0.80-pre1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68933c0ffa67a70297e5f7cd025708eac1e32b9f",
+   "rev": "f80f38d975a7e02e8e2f3b07c1e3b847dcd4e6ec",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "lean-pr-testing-11220",

lakefile.lean

@@ -9,7 +9,7 @@ open Lake DSL
 require "leanprover-community" / "batteries" @ git "lean-pr-testing-11220"
 require "leanprover-community" / "Qq" @ git "master"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
-require "leanprover-community" / "proofwidgets" @ git "v0.0.77" -- ProofWidgets should always be pinned to a specific version
+require "leanprover-community" / "proofwidgets" @ git "v0.0.80-pre1" -- ProofWidgets should always be pinned to a specific version
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets not up-to-date. \
     Please run `lake exe cache get` to fetch the latest ProofWidgets. \