Merge branch 'bump/nightly-2025-11-22' into nightly-testing

Author: kim-em

Mathlib.lean

@@ -6289,6 +6289,7 @@ public import Mathlib.SetTheory.Surreal.Basic
 public import Mathlib.SetTheory.Surreal.Dyadic
 public import Mathlib.SetTheory.Surreal.Multiplication
 public import Mathlib.SetTheory.ZFC.Basic
+public import Mathlib.SetTheory.ZFC.Cardinal
 public import Mathlib.SetTheory.ZFC.Class
 public import Mathlib.SetTheory.ZFC.Ordinal
 public import Mathlib.SetTheory.ZFC.PSet

Mathlib/Data/Finset/Basic.lean

@@ -551,9 +551,13 @@ theorem choose_spec (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (
 theorem choose_mem (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l :=
   (choose_spec _ _ _).1
 
+grind_pattern choose_mem => choose p l hp
+
 theorem choose_property (hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp) :=
   (choose_spec _ _ _).2
 
+grind_pattern choose_property => choose p l hp
+
 end Choose
 
 end Finset

Mathlib/Logic/Basic.lean

@@ -727,6 +727,10 @@ protected noncomputable def byContradiction' {α : Sort*} (H : ¬(α → False))
 def choice_of_byContradiction' {α : Sort*} (contra : ¬(α → False) → α) : Nonempty α → α :=
   fun H ↦ contra H.elim
 
+-- This can be removed after https://github.com/leanprover/lean4/pull/11316
+-- arrives in a release candidate.
+grind_pattern Exists.choose_spec => P.choose
+
 @[simp] lemma choose_eq (a : α) : @Exists.choose _ (· = a) ⟨a, rfl⟩ = a := @choose_spec _ (· = a) _
 
 @[simp]

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -628,6 +628,9 @@ theorem mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x
     #(Subtype p) ≤ #(Subtype q) :=
   ⟨Embedding.subtypeMap (Embedding.refl α) h⟩
 
+theorem mk_le_mk_of_subset {α} {s t : Set α} (h : s ⊆ t) : #s ≤ #t :=
+  ⟨Set.embeddingOfSubset s t h⟩
+
 theorem mk_emptyCollection (α : Type u) : #(∅ : Set α) = 0 :=
   mk_eq_zero _
 
@@ -707,6 +710,10 @@ theorem mk_image_embedding_lift {β : Type v} (f : α ↪ β) (s : Set α) :
 theorem mk_image_embedding (f : α ↪ β) (s : Set α) : #(f '' s) = #s := by
   simpa using mk_image_embedding_lift f s
 
+theorem iSup_mk_le_mk_iUnion {α : Type u} {ι : Type v} {f : ι → Set α} :
+    ⨆ i, #(f i) ≤ #(⋃ i, f i) :=
+  ciSup_le' fun _ => mk_le_mk_of_subset (subset_iUnion _ _)
+
 theorem mk_iUnion_le_sum_mk {α ι : Type u} {f : ι → Set α} : #(⋃ i, f i) ≤ sum fun i => #(f i) :=
   calc
     #(⋃ i, f i) ≤ #(Σ i, f i) := mk_le_of_surjective (Set.sigmaToiUnion_surjective f)
@@ -808,9 +815,6 @@ theorem mk_sum_compl {α} (s : Set α) : #s + #(sᶜ : Set α) = #α := by
   classical
   exact mk_congr (Equiv.Set.sumCompl s)
 
-theorem mk_le_mk_of_subset {α} {s t : Set α} (h : s ⊆ t) : #s ≤ #t :=
-  ⟨Set.embeddingOfSubset s t h⟩
-
 theorem mk_le_iff_forall_finset_subset_card_le {α : Type u} {n : ℕ} {t : Set α} :
     #t ≤ n ↔ ∀ s : Finset α, (s : Set α) ⊆ t → s.card ≤ n := by
   refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩

Mathlib/SetTheory/ZFC/Basic.lean

@@ -600,6 +600,16 @@ lemma coe_sdiff (x y : ZFSet.{u}) : ↑(x \ y) = (↑x \ ↑y : Set ZFSet) := by
 
 @[deprecated (since := "2025-11-05")] alias toSet_sdiff := coe_sdiff
 
+@[simp] lemma inter_eq_left_of_subset (hxy : x ⊆ y) : x ∩ y = x := by ext; simpa using @hxy _
+@[simp] lemma inter_eq_right_of_subset (hyx : y ⊆ x) : x ∩ y = y := by ext; simpa using @hyx _
+
+/-- `ZFSet.powerset` is equivalent to `Set.powerset`. -/
+def powersetEquiv (x : ZFSet.{u}) : x.powerset ≃ 𝒫 (x : Set ZFSet) where
+  toFun y := ⟨y.1, Set.mem_powerset (mem_powerset.1 y.2)⟩
+  invFun s := ⟨x.sep (· ∈ s.1), mem_powerset.2 sep_subset⟩
+  left_inv := by simp +contextual [Function.LeftInverse]
+  right_inv := by simp +contextual [Function.LeftInverse, Function.RightInverse, Set.setOf_and]
+
 theorem mem_wf : @WellFounded ZFSet (· ∈ ·) :=
   (wellFounded_lift₂_iff (H := fun a b c d hx hy =>
     propext ((@Mem.congr_left a c hx).trans (@Mem.congr_right b d hy _)))).mpr PSet.mem_wf

Mathlib/SetTheory/ZFC/Cardinal.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2025 Dexin Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dexin Zhang
+-/
+module
+
+public import Mathlib.SetTheory.Cardinal.Basic
+public import Mathlib.SetTheory.ZFC.Basic
+
+/-!
+# Cardinalities of ZFC sets
+
+In this file, we define the cardinalities of ZFC sets as `ZFSet.{u} → Cardinal.{u}`.
+
+## Definitions
+
+* `ZFSet.card`: Cardinality of a ZFC set.
+-/
+
+@[expose] public section
+
+universe u v
+
+open Cardinal
+
+namespace ZFSet
+
+/-- The cardinality of a ZFC set. -/
+def card (x : ZFSet.{u}) : Cardinal.{u} := #(Shrink x)
+
+variable {x y : ZFSet.{u}}
+
+/-- `ZFSet.card x` is equal to the cardinality of `x` as a set of `ZFSet`s. -/
+theorem cardinalMk_coe_sort : #x = lift.{u + 1, u} (card x) := by
+  rw [card, lift_mk_shrink'']
+
+@[gcongr]
+theorem card_mono (h : x ⊆ y) : card x ≤ card y := by
+  simpa [cardinalMk_coe_sort] using mk_le_mk_of_subset (coe_subset_coe.2 h)
+
+@[simp]
+theorem card_empty : card ∅ = 0 := by
+  rw [← lift_inj, ← cardinalMk_coe_sort]
+  simp
+
+theorem card_insert_le : card (insert x y) ≤ card y + 1 := by
+  rw [← lift_le.{u + 1}]
+  simpa [← cardinalMk_coe_sort] using mk_insert_le
+
+theorem card_insert (h : x ∉ y) : card (insert x y) = card y + 1 := by
+  rw [← lift_inj.{u, u + 1}]
+  simpa [← cardinalMk_coe_sort] using mk_insert (SetLike.mem_coe.not.2 h)
+
+@[simp]
+theorem card_singleton : card {x} = 1 := by
+  simpa [notMem_singleton] using card_insert (notMem_empty x)
+
+theorem card_pair_of_ne (h : x ≠ y) : card {x, y} = 2 := by
+  convert card_insert (notMem_singleton.2 h)
+  rw [card_singleton, one_add_one_eq_two]
+
+theorem card_union_le : card (x ∪ y) ≤ card x + card y := by
+  rw [← lift_le.{u + 1}]
+  simpa [← cardinalMk_coe_sort] using mk_union_le (x : Set ZFSet) y
+
+@[simp]
+theorem card_powerset (x : ZFSet.{u}) : card (powerset x) = 2 ^ card x := by
+  rw [← lift_inj.{u, u + 1}]
+  simpa [← cardinalMk_coe_sort] using mk_congr (powersetEquiv x)
+
+theorem card_image_le {f : ZFSet → ZFSet} [Definable₁ f] :
+    card (image f x) ≤ card x := by
+  simpa [cardinalMk_coe_sort, ← coe_image, -mem_image] using mk_image_le (f := f) (s := x)
+
+theorem lift_card_range_le {α} [Small.{v, u} α] {f : α → ZFSet.{v}} :
+    lift.{u} (card (range f)) ≤ lift.{v} #α := by
+  rw [← lift_le.{max u (v + 1)}, lift_lift.{v}, lift_umax.{u, v + 1}]
+  simpa [cardinalMk_coe_sort, ← coe_range, -mem_range] using mk_range_le_lift (f := f)
+
+theorem iSup_card_le_card_iUnion {α} [Small.{v, u} α] {f : α → ZFSet.{v}} :
+    ⨆ i, card (f i) ≤ card (⋃ i, f i) := by
+  simpa [cardinalMk_coe_sort, ← coe_iUnion, ← lift_iSup (bddAbove_of_small _), -mem_iUnion] using
+    iSup_mk_le_mk_iUnion (f := SetLike.coe ∘ f)
+
+theorem lift_card_iUnion_le_sum_card {α} [Small.{v, u} α] {f : α → ZFSet.{v}} :
+    lift (card (⋃ i, f i)) ≤ sum fun i => card (f i) := by
+  rw [← lift_le.{max u (v + 1)}, lift_umax.{max u v, v + 1}]
+  simpa [cardinalMk_coe_sort, ← coe_iUnion, -mem_iUnion] using
+    mk_iUnion_le_sum_mk_lift (f := SetLike.coe ∘ f)
+
+end ZFSet

lakefile.lean

@@ -9,7 +9,7 @@ open Lake DSL
 require "leanprover-community" / "batteries" @ git "nightly-testing"
 require "leanprover-community" / "Qq" @ git "nightly-testing"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
-require "leanprover-community" / "proofwidgets" @ git "v0.0.82-pre1" -- ProofWidgets should always be pinned to a specific version
+require "leanprover-community" / "proofwidgets" @ git "v0.0.82" -- 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. \
@@ -186,9 +186,12 @@ post_update pkg do
     let toolchainVersion := match toolchainContent.trimAscii.copy.splitOn ":" with
       | [_, version] => version
       | _ => toolchainContent.trimAscii.copy  -- fallback to full content if format is unexpected
+    -- Lean.versionString does not start with a `v`, while the `lean-toolchain` file is flexible.
+    let toolchainVersion := (toolchainVersion.dropPrefix "v").copy
     if Lean.versionString ≠ toolchainVersion then
-      IO.println s!"Not running `lake exe cache get` yet, \
-        as the `lake` version does not match the toolchain version in the project.\n\
+      IO.println s!"Not running `lake exe cache get` yet, as \
+        the `lake` version ({Lean.versionString}) does not match \
+        the toolchain version ({toolchainVersion}) in the project.\n\
         You should run `lake exe cache get` manually."
       return
     let exeFile ← runBuild cache.fetch

scripts/nolints.json

@@ -146,7 +146,6 @@
  ["docBlame", "HomogeneousLocalization.NumDenSameDeg.num"],
  ["docBlame", "HomologicalComplex.Hom.f"],
  ["docBlame", "Ideal.Filtration.N"],
- ["docBlame", "IntermediateField.delabAdjoinNotation.delabInsertArray"],
  ["docBlame", "IsDedekindDomain.HeightOneSpectrum.asIdeal"],
  ["docBlame", "Lean.Export.Alloc"],
  ["docBlame", "Lean.Export.Entry"],
@@ -227,21 +226,6 @@
  ["docBlame", "Lean.Export.State.levels"],
  ["docBlame", "Lean.Export.State.names"],
  ["docBlame", "Lean.Export.State.stk"],
- ["docBlame", "Lean.Export.exportDef.axdef"],
- ["docBlame", "Lean.Export.exportDef.defn"],
- ["docBlame", "Lean.Export.exportDef.ind"],
- ["docBlame", "Lean.Export.exportDef.indbody"],
- ["docBlame", "Lean.Export.exportDef.insert"],
- ["docBlame", "Lean.MVarId.congrN!.go"],
- ["docBlame", "Lean.MVarId.congrN!.post"],
- ["docBlame", "Lean.MVarId.congrSimp?.forSide"],
- ["docBlame", "Lean.MVarId.introsClean.eqImpOfIffImp"],
- ["docBlame", "Lean.MVarId.introsClean.heqImpOfEqImp"],
- ["docBlame", "Lean.MVarId.introsClean.isTrivialType"],
- ["docBlame", "Lean.MVarId.introsClean.loop"],
- ["docBlame", "Lean.MVarId.smartHCongr?.forSide"],
- ["docBlame", "Lean.MVarId.smartHCongr?.loop"],
- ["docBlame", "Lean.MVarId.userCongr?.forSide"],
  ["docBlame", "Lean.Parser.Attr.higherOrder"],
  ["docBlame", "Lean.Parser.Tactic.applyCongr"],
  ["docBlame", "Mathlib.Command.Variable.completeBinders"],
@@ -265,25 +249,13 @@
  ["docBlame", "Mathlib.Tactic.GCongr.exact"],
  ["docBlame", "Mathlib.Tactic.GCongr.tacticGcongr_discharger"],
  ["docBlame", "Mathlib.Tactic.Propose.proposeLemmas"],
- ["docBlame", "Mathlib.Tactic.evalIntrov.intro1PStep"],
- ["docBlame", "Mathlib.Tactic.evalIntrov.introsDep"],
  ["docBlame", "Module.End.Eigenvalues.val"],
  ["docBlame", "Order.Ideal.PrimePair.F"],
  ["docBlame", "Order.Ideal.PrimePair.I"],
- ["docBlame", "Tactic.Elementwise.elementwiseExpr.mkHomElementwise"],
  ["docBlame", "Lean.Meta.mkRichHCongr.doubleTelescope.loop"],
  ["docBlame", "Lean.Meta.mkRichHCongr.withNewEqs.loop"],
- ["docBlame", "Mathlib.Command.Variable.completeBinders'.isVariableAlias"],
- ["docBlame", "Mathlib.Command.Variable.elabVariables.extendScope"],
- ["docBlame", "Mathlib.Command.Variable.elabVariables.process"],
  ["docBlame", "Mathlib.Command.Variable.variable?.checkRedundant"],
  ["docBlame", "Mathlib.Command.Variable.variable?.maxSteps"],
- ["docBlame", "Mathlib.Meta.NormNum.evalEq.intArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalEq.nnratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalEq.ratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalMinFac.aux"],
- ["docBlame", "Mathlib.Meta.NormNum.evalMinFac.core"],
- ["docBlame", "Mathlib.Meta.NormNum.evalNatPrime.core"],
  ["docBlame", "Mathlib.Tactic.CC.CCPropagationHandler.propagated"],
  ["docBlame", "Mathlib.Tactic.CC.CCState.getNumROccs"],
  ["docBlame", "Mathlib.Tactic.CC.CCState.ppAC"],
@@ -304,13 +276,4 @@
  ["docBlame", "Mathlib.Tactic.Coherence.LiftObj.lift"],
  ["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"],
  ["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"],
- ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
- ["docBlame", "Mathlib.Meta.NormNum.Result.add.intArm"],
- ["docBlame", "Mathlib.Meta.NormNum.Result.add.nnratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.Result.add.ratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.Result.mul.ratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalLE.core.intArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalLE.core.ratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.intArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.nnratArm"],
- ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.ratArm"]]
+ ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"]]