Merge master into nightly-testing

.github/workflows/lean4checker.yml

@@ -70,7 +70,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.12.0-rc1
+          git checkout v4.13.0-rc3
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

Mathlib.lean

@@ -4744,7 +4744,7 @@ import Mathlib.Topology.MetricSpace.ThickenedIndicator
 import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Topology.MetricSpace.Ultra.Basic
 import Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
-import Mathlib.Topology.MetricSpace.Ultra.TotallyDisconnected
+import Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
 import Mathlib.Topology.Metrizable.Basic
 import Mathlib.Topology.Metrizable.ContinuousMap
 import Mathlib.Topology.Metrizable.Uniformity

Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean

@@ -680,16 +680,14 @@ theorem toCharTwoJNeZeroNF_spec (ha₁ : W.a₁ ≠ 0) :
   · field_simp [toCharTwoJNeZeroNF]
     linear_combination (W.a₁ ^ 4 * W.a₃ ^ 2 + W.a₁ ^ 5 * W.a₃ * W.a₂) * CharP.cast_eq_zero F 2
 
-variable [DecidableEq F]
-
 /-- For a `WeierstrassCurve` defined over a field of characteristic = 2,
 there is an explicit change of variables of it to `WeierstrassCurve.IsCharTwoNF`, that is,
 $Y^2 + XY = X^3 + a_2X^2 + a_6$ (`WeierstrassCurve.IsCharTwoJNeZeroNF`) or
 $Y^2 + a_3Y = X^3 + a_4X + a_6$ (`WeierstrassCurve.IsCharTwoJEqZeroNF`). -/
-def toCharTwoNF : VariableChange F :=
+def toCharTwoNF [DecidableEq F] : VariableChange F :=
   if ha₁ : W.a₁ = 0 then W.toCharTwoJEqZeroNF else W.toCharTwoJNeZeroNF ha₁
 
-instance toCharTwoNF_spec : (W.variableChange W.toCharTwoNF).IsCharTwoNF := by
+instance toCharTwoNF_spec [DecidableEq F] : (W.variableChange W.toCharTwoNF).IsCharTwoNF := by
   by_cases ha₁ : W.a₁ = 0
   · rw [toCharTwoNF, dif_pos ha₁]
     haveI := W.toCharTwoJEqZeroNF_spec ha₁
@@ -699,8 +697,9 @@ instance toCharTwoNF_spec : (W.variableChange W.toCharTwoNF).IsCharTwoNF := by
     infer_instance
 
 theorem exists_variableChange_isCharTwoNF :
-    ∃ C : VariableChange F, (W.variableChange C).IsCharTwoNF :=
-  ⟨_, W.toCharTwoNF_spec⟩
+    ∃ C : VariableChange F, (W.variableChange C).IsCharTwoNF := by
+  classical
+  exact ⟨_, W.toCharTwoNF_spec⟩
 
 end VariableChange
 

Mathlib/Tactic/FunProp/RefinedDiscrTree.lean

@@ -449,7 +449,7 @@ partial def reduce (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
 /-- Repeatedly apply reduce while stripping lambda binders and introducing their variables -/
 @[specialize]
 partial def lambdaTelescopeReduce {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
-    [Inhabited α] (e : Expr) (fvars : List FVarId) (config : WhnfCoreConfig)
+    [Nonempty α] (e : Expr) (fvars : List FVarId) (config : WhnfCoreConfig)
     (k : Expr → List FVarId → m α) : m α := do
   match ← reduce e config with
   | .lam n d b bi =>

Mathlib/Topology/Clopen.lean

@@ -102,6 +102,10 @@ theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s)
   rintro x ⟨hx₁, hx₂⟩
   exact ⟨hx₁, by simpa [not_mem_of_mem_compl hx₂] using cover hx₁⟩
 
+theorem isClopen_of_disjoint_cover_open {a b : Set X} (cover : univ ⊆ a ∪ b)
+    (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen a :=
+  univ_inter a ▸ isClopen_inter_of_disjoint_cover_clopen isClopen_univ cover ha hb hab
+
 @[simp]
 theorem isClopen_discrete [DiscreteTopology X] (s : Set X) : IsClopen s :=
   ⟨isClosed_discrete _, isOpen_discrete _⟩

Mathlib/Topology/Connected/TotallyDisconnected.lean

@@ -195,7 +195,7 @@ alias IsTotallySeparated.isTotallyDisconnected := isTotallyDisconnected_of_isTot
 
 /-- A space is totally separated if any two points can be separated by two disjoint open sets
 covering the whole space. -/
-class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where
+@[mk_iff] class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where
   /-- The universal set `Set.univ` in a totally separated space is totally separated. -/
   isTotallySeparated_univ : IsTotallySeparated (univ : Set α)
 
@@ -210,15 +210,19 @@ instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type*) [Topol
   ⟨fun _ _ b _ h => ⟨{b}ᶜ, {b}, isOpen_discrete _, isOpen_discrete _, h, rfl,
     (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩
 
+theorem totallySeparatedSpace_iff_exists_isClopen {α : Type*} [TopologicalSpace α] :
+    TotallySeparatedSpace α ↔ ∀ x y : α, x ≠ y → ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
+  simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]
+  refine forall₃_congr fun x y _ ↦
+    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩
+  · exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
+      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩
+  · exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩
+
 theorem exists_isClopen_of_totally_separated {α : Type*} [TopologicalSpace α]
     [TotallySeparatedSpace α] {x y : α} (hxy : x ≠ y) :
-    ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
-  obtain ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ :=
-    TotallySeparatedSpace.isTotallySeparated_univ (Set.mem_univ x) (Set.mem_univ y) hxy
-  have hU := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
-  rw [univ_inter _] at hU
-  rw [← Set.subset_compl_iff_disjoint_right, subset_compl_comm] at disj
-  exact ⟨U, hU, Ux, disj Vy⟩
+    ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ :=
+  totallySeparatedSpace_iff_exists_isClopen.mp ‹_› _ _ hxy
 
 end TotallySeparated
 
@@ -260,7 +264,6 @@ theorem Continuous.connectedComponentsLift_unique (h : Continuous f) (g : Connec
     (hg : g ∘ (↑) = f) : g = h.connectedComponentsLift :=
   connectedComponents_lift_unique' <| hg.trans h.connectedComponentsLift_comp_coe.symm
 
-
 instance ConnectedComponents.totallyDisconnectedSpace :
     TotallyDisconnectedSpace (ConnectedComponents α) := by
   rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]

Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky, David Loeffler
+-/
+import Mathlib.Topology.MetricSpace.Defs
+import Mathlib.Topology.MetricSpace.Ultra.Basic
+
+/-!
+# Ultrametric spaces are totally separated
+
+In a metric space with an ultrametric, the space is totally separated, hence totally disconnected.
+
+## Tags
+
+ultrametric, nonarchimedean, totally separated, totally disconnected
+-/
+open Metric IsUltrametricDist
+
+instance {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallySeparatedSpace X :=
+  totallySeparatedSpace_iff_exists_isClopen.mpr fun x y h ↦ by
+    obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)
+    refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩
+    · simp only [mem_ball, dist_self, hr]
+    · simp only [Set.mem_compl, mem_ball, dist_comm, not_lt, hr'.le]
+
+example {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallyDisconnectedSpace X :=
+  inferInstance

Mathlib/Util/Superscript.lean

@@ -95,7 +95,8 @@ partial def satisfyTokensFn (p : Char → Bool) (errorMsg : String) (many := tru
 variable {α : Type u} [Inhabited α] (as : Array α) (leftOfPartition : α → Bool) in
 /-- Given a predicate `leftOfPartition` which is true for indexes `< i` and false for `≥ i`,
 returns `i`, by binary search. -/
-@[specialize] partial def partitionPoint (lo := 0) (hi := as.size) : Nat :=
+@[specialize]
+def partitionPoint (lo := 0) (hi := as.size) : Nat :=
   if lo < hi then
     let m := (lo + hi)/2
     let a := as.get! m
@@ -104,6 +105,7 @@ returns `i`, by binary search. -/
     else
       partitionPoint lo m
   else lo
+  termination_by hi - lo
 
 /-- The core function for super/subscript parsing. It consists of three stages:
 

scripts/technical-debt-metrics.sh

@@ -53,6 +53,8 @@ printf '%s|%s\n' "$(grep -c 'docBlame' scripts/nolints.json)" "documentation nol
 printf '%s|%s\n' "$(git grep '^set_option linter.style.longFile [0-9]*' Mathlib | wc -l)" "large files"
 printf '%s|%s\n' "$(git grep "^open .*Classical" | grep -v " in$" -c)" "bare open (scoped) Classical"
 
+printf '%s|%s\n' "$(wc -l < scripts/no_lints_prime_decls.txt)" "exceptions for the docPrime linter"
+
 deprecatedFiles="$(git ls-files '**/Deprecated/*.lean' | xargs wc -l | sed 's=^ *==')"
 
 printf '%s|%s\n' "$(printf '%s' "${deprecatedFiles}" | wc -l)" "\`Deprecated\` files"