bump to v4.23.0 (#1371)

BoltonBailey · YaelDillies · web-flow · commit e36c64de6e99 · 2025-12-11T08:22:53.000Z
This PR bumps the toolchain to v4.23.0, and makes small fixes to details
to ensure the library builds.

---------

Co-authored-by: Yaël Dillies &lt;yael.dillies@gmail.com&gt;
diff --git a/FormalConjectures/ErdosProblems/141.lean b/FormalConjectures/ErdosProblems/141.lean
@@ -43,7 +43,7 @@ theorem first_three_odd_primes : ({3, 5, 7} : Set ℕ).IsPrimeProgressionOfLengt
   use 1
   constructor
   · aesop
-  · norm_num [exists_lt_succ, or_assoc, eq_comm, Set.insert_def,
+  · norm_num [exists_lt_succ_right, or_assoc, eq_comm, Set.insert_def,
     show (2).nth Nat.Prime = 5 from nth_count prime_five,
     show (3).nth Nat.Prime = 7 from Nat.nth_count (by decide : (7).Prime)]
 
@@ -65,7 +65,7 @@ theorem exists_three_consecutive_primes_in_ap : ∃ (s : Set ℕ), s.IsAPAndPrim
     unfold Set.IsAPOfLengthWith
     constructor
     · aesop
-    · norm_num [exists_lt_succ, or_assoc, eq_comm, Set.insert_def]
+    · norm_num [exists_lt_succ_right, or_assoc, eq_comm, Set.insert_def]
   · exact first_three_odd_primes
 
 /--
diff --git a/FormalConjectures/ErdosProblems/170.lean b/FormalConjectures/ErdosProblems/170.lean
@@ -45,9 +45,8 @@ abbrev TrivialRuler (N : ℕ) : Finset ℕ := Finset.range (N+1)
 /-- Sanity Check: the trivial ruler is actually a perfect ruler if $K \geq N$ -/
 @[category API, AMS 05]
 lemma trivial_ruler_is_perfect (N : ℕ) : TrivialRuler N ∈ PerfectRulersLengthN N := by
-    simp only [PerfectRulersLengthN, Finset.mem_filter, Finset.mem_powerset, Finset.range_subset,
-      add_le_add_iff_right]
-    exact ⟨by rfl, fun k hk => ⟨0, by simp, k, hk, rfl⟩⟩
+    simp only [PerfectRulersLengthN, Finset.mem_filter, Finset.mem_powerset, Finset.range_subset]
+    exact ⟨by simp, fun k hk => ⟨0, by simp, k, hk, rfl⟩⟩
 
 /-- We define a function `F N` as the minimum cardinality of an `N`-perfect ruler of length `N`. -/
 def F (N : ℕ) : ℕ :=
diff --git a/FormalConjectures/ErdosProblems/26.lean b/FormalConjectures/ErdosProblems/26.lean
@@ -45,7 +45,8 @@ theorem not_isThick_of_geom_one_lt (r : ℕ) (hr : r > 1) : ¬IsThick fun n : 
 
 @[category test, AMS 11]
 theorem isThick_const {ι : Type*} [Infinite ι] (r : ℕ) (h : r > 0) : IsThick fun _ : ι ↦ r := by
-  field_simp [IsThick, h, summable_const_iff]
+  simp only [IsThick, one_div, summable_const_iff, inv_eq_zero, Nat.cast_eq_zero]
+  exact Nat.ne_zero_of_lt h
 
 /-- The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$. -/
 def MultiplesOf {ι : Type*} (A : ι → ℕ) : Set ℕ := Set.range fun (n, i) ↦ n * A i
@@ -69,7 +70,8 @@ theorem isBehrend_of_contains_one {ι : Type*} (A : ι → ℕ) (h : 1 ∈ Set.r
     IsBehrend A := by
   rw [IsBehrend, Set.HasDensity]
   exact tendsto_atTop_of_eventually_const (i₀ := 1) fun n hn ↦ by
-    field_simp [multiplesOf_eq_univ A h, Set.partialDensity]
+    simp [multiplesOf_eq_univ A h, Set.partialDensity]
+    field_simp
 
 @[category test, AMS 11]
 theorem isWeaklyBehrend_of_ge_one {ι : Type*} (A : ι → ℕ) {ε : ℝ} (hε : 1 ≤ ε) :
diff --git a/FormalConjectures/ErdosProblems/40.lean b/FormalConjectures/ErdosProblems/40.lean
@@ -78,7 +78,8 @@ theorem erdos_28_of_erdos_40 (h_erdos_40 : Erdos40 fun _ => True) : type_of% Erd
     use n + 1
     intro m hm
     have : 0 < m := by omega
-    field_simp [norm_one, Real.norm_natCast, one_mul, Nat.one_le_cast, ge_iff_le]
+    field_simp
+    simp only [one_mem, CStarRing.norm_of_mem_unitary, RCLike.norm_natCast, Nat.one_le_cast]
     apply Nat.card_pos_iff.mpr
     constructor
     · by_contra h_empty
diff --git a/FormalConjectures/ForMathlib/AlgebraicGeometry/ProjectiveSpace.lean b/FormalConjectures/ForMathlib/AlgebraicGeometry/ProjectiveSpace.lean
@@ -17,7 +17,7 @@ import Mathlib.AlgebraicGeometry.Limits
 import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
 import Mathlib.RingTheory.MvPolynomial.Homogeneous
 
--- The contents of this file will be in mathlib as of #26061 which should be merged in 4.21 or 4.22.
+-- The contents of this file will be in mathlib as of #26061
 
 universe u v
 open CategoryTheory Limits MvPolynomial AlgebraicGeometry
diff --git a/FormalConjectures/ForMathlib/Analysis/SpecialFunctions/Log/Basic.lean b/FormalConjectures/ForMathlib/Analysis/SpecialFunctions/Log/Basic.lean
@@ -14,8 +14,8 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
+import Mathlib.Analysis.Complex.ExponentialBounds
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
-import Mathlib.Data.Complex.ExponentialBounds
 import Mathlib.Tactic
 
 -- TODO(mercuris): define a recursive version of this for better usability?
diff --git a/FormalConjectures/ForMathlib/Combinatorics/Additive/Convolution.lean b/FormalConjectures/ForMathlib/Combinatorics/Additive/Convolution.lean
@@ -62,7 +62,7 @@ lemma sumRep_def (A : Set ℕ) (n : ℕ) :
 open PowerSeries
 
 theorem sumRep_eq_powerSeries_coeff (A : Set ℕ) (n : ℕ) : (sumRep  A  n : ℕ) =
-    ((PowerSeries.mk (𝟙_A)) * (PowerSeries.mk (𝟙_A)) : PowerSeries ℕ).coeff ℕ n := by
+    ((PowerSeries.mk (𝟙_A)) * (PowerSeries.mk (𝟙_A)) : PowerSeries ℕ).coeff n := by
   simp [sumRep, sumConv, indicatorOne, indicator, PowerSeries.coeff_mul, PowerSeries.coeff_mk]
 
 end AdditiveCombinatorics
diff --git a/FormalConjectures/ForMathlib/Computability/TuringMachine/PostTuringMachine.lean b/FormalConjectures/ForMathlib/Computability/TuringMachine/PostTuringMachine.lean
@@ -17,15 +17,6 @@ limitations under the License.
 import Mathlib.Computability.PostTuringMachine
 import Mathlib.Logic.Relation
 
-theorem Part.eq_of_get_eq_get {σ : Type*} {a b : Part σ} (ha : a.Dom) (hb : b.Dom)
-    (hab : a.get ha = b.get hb) : a = b := by
-  ext
-  rw [← Part.eq_get_iff_mem ha, ← Part.eq_get_iff_mem hb, hab]
-
-theorem Part.eq_iff_of_dom {σ : Type*} {a b : Part σ} (ha : a.Dom) (hb : b.Dom) :
-    a.get ha = b.get hb ↔ a = b :=
-  ⟨fun H ↦ Part.eq_of_get_eq_get ha hb H, fun H ↦ Part.get_eq_get_of_eq a ha H⟩
-
 theorem Part.get_eq_get {σ : Type*} {a b : Part σ} (ha : a.Dom) (hb : a.get ha ∈ b) : a = b := by
   have hb' : b.Dom := Part.dom_iff_mem.mpr ⟨a.get ha, hb⟩
   rwa [← Part.eq_get_iff_mem hb', Part.eq_iff_of_dom ha hb'] at hb
diff --git a/FormalConjectures/ForMathlib/Data/Finset/Empty.lean b/FormalConjectures/ForMathlib/Data/Finset/Empty.lean
diff --git a/FormalConjectures/ForMathlib/Data/Set/Density.lean b/FormalConjectures/ForMathlib/Data/Set/Density.lean
@@ -63,7 +63,7 @@ noncomputable def lowerDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot
 theorem lowerDensity_le_one {β : Type*} [Preorder β] [LocallyFiniteOrderBot β]
     (S : Set β) (A : Set β := Set.univ) : S.lowerDensity A ≤ 1 := by
   by_cases h : atTop (α := β) = ⊥
-  · field_simp [h, Set.lowerDensity, Filter.liminf_eq]
+  · simp [h, Set.lowerDensity, Filter.liminf_eq]
   · have : (atTop (α := β)).NeBot := ⟨h⟩
     apply Real.sSup_le (fun x hx ↦ ?_) one_pos.le
     simpa using hx.mono fun y hy ↦ hy.trans (Set.partialDensity_le_one _ _ y)
@@ -105,7 +105,7 @@ elements has density one. -/
 theorem univ {β : Type*} [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] [Nontrivial β] :
     (@Set.univ β).HasDensity 1 := by
   by_cases h : atTop (α := β) = ⊥
-  · field_simp [h, HasDensity]
+  · simp [h, HasDensity]
   · simp [HasDensity, partialDensity]
     let ⟨b, hb⟩ := Set.Iio_eventually_ncard_ne_zero β
     refine tendsto_const_nhds.congr' ?_
diff --git a/FormalConjectures/ForMathlib/Geometry/2d.lean b/FormalConjectures/ForMathlib/Geometry/2d.lean
@@ -31,7 +31,7 @@ open scoped EuclideanGeometry
 Note: this can't blindly be added to mathlib as it creates an "instance diamond"
 with an instance for modules satisfying `is_empty`. -/
 noncomputable instance Module.orientedEuclideanSpaceFinTwo : Module.Oriented ℝ ℝ² (Fin 2) :=
-  ⟨Basis.orientation <| Pi.basisFun _ _⟩
+  ⟨Basis.orientation <| PiLp.basisFun 2 _ _⟩
 
 /-- Two dimensional euclidean space is two-dimensional. -/
 instance fact_finrank_euclideanSpace_fin_two : Fact (Module.finrank ℝ ℝ² = 2) :=
@@ -159,10 +159,12 @@ theorem isConvexPolygon_three_iff_affineIndependent {A B C : P} :
   let p := ![A, B, C]
   change IsConvexPolygon p at h
   change Real.Angle.sign (∡ (p 0) (p 1) (p 2)) ≠ 0
-  cases' h with h h
-  · rw [h.sign_oangle (by simp) (by simp)]
+  cases h with
+  | inl h =>
+    rw [h.sign_oangle (by simp) (by simp)]
     rintro ⟨⟩
-  · suffices Real.Angle.sign (∡ (p 0) (p 2) (p 1)) = 1 by rw [← oangle_swap₂₃_sign, this]; rintro ⟨⟩
+  | inr h =>
+    suffices Real.Angle.sign (∡ (p 0) (p 2) (p 1)) = 1 by rw [← oangle_swap₂₃_sign, this]; rintro ⟨⟩
     exact h.sign_oangle (i := 0) (j := 1) (k := 2) (by simp) (by simp)
 
 theorem isConvexPolygon_triangle (t : Affine.Triangle ℝ P) : IsConvexPolygon t.points := by
diff --git a/FormalConjectures/Mathoverflow/34145.lean b/FormalConjectures/Mathoverflow/34145.lean
@@ -122,7 +122,7 @@ lemma tsum_area_eq_one : ∑' (n : ℕ), ((1 / (n + 1)) * (1 / (n + 2)) : ℝ) =
   have (n : ℕ) : ∑ i ∈ Finset.range n, (1 / (i + 1) * (1 / (i + 2)) : ℝ) = 1 - 1 / (n + 1) := by
     induction n with
     | zero => simp
-    | succ n ih => rw [Finset.sum_range_succ, ih]; field_simp; ring
+    | succ n ih => rw [Finset.sum_range_succ, ih]; field_simp; push_cast; ring
   refine HasSum.tsum_eq ((hasSum_iff_tendsto_nat_of_nonneg (fun i ↦ ?_) _).2 ?_)
   · positivity
   · simp_rw [this]
diff --git a/FormalConjectures/Paper/Kurepa.lean b/FormalConjectures/Paper/Kurepa.lean
@@ -65,8 +65,11 @@ theorem kurepa_conjecture.prime_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠
       refine hp.eq_two_or_odd.resolve_right fun _ ↦ ?_
       have : p ∣ ∑ a ∈ range n, (a)! := .trans (by simp)
         (dvd_of_mem_primeFactorsList h_mem |>.trans (dvd_of_mod_eq_zero h_mod))
-      rw [← CharP.cast_eq_zero_iff (ZMod p), cast_sum, ← sum_subset (range_subset.2
-        (le_of_mem_primeFactorsList h_mem)) (fun _ _ _ ↦ CharP.cast_eq_zero_iff _ p _ |>.2 <|
+      have hxp : range p ⊆ range n := by
+        simp only [range_subset_range]
+        exact le_of_mem_primeFactorsList h_mem
+      rw [← CharP.cast_eq_zero_iff (ZMod p), cast_sum,
+        ← sum_subset hxp (fun _ _ _ ↦ CharP.cast_eq_zero_iff _ p _ |>.2 <|
         hp.dvd_factorial.2 <| by aesop), ← cast_sum, CharP.cast_eq_zero_iff _ p] at this
       exact h p (hp.two_le.lt_of_ne (by omega)) hp <| mod_eq_zero_of_dvd this
     rw [List.prod_eq_pow_card _ 2 this]
@@ -107,7 +110,10 @@ theorem kurepa_conjecture.gcd_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠ 0
         pos_of_dvd_of_pos hc (factorial_pos _)])] at h_dvd
     refine by_contra fun _ ↦ h c ?_ (sum_nat_mod _ _ _ ▸ h_dvd)
     match c with
-    | 0 => field_simp [Ne.symm] at hc
+    | 0 =>
+      contrapose! hc
+      simp only [zero_dvd_iff]
+      positivity
     | 1 => trivial
     | S + 3 => omega
 
diff --git a/FormalConjectures/Util/ForMathlib.lean b/FormalConjectures/Util/ForMathlib.lean
@@ -37,7 +37,6 @@ import FormalConjectures.ForMathlib.Computability.TuringMachine.Notation
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Balanced
 import FormalConjectures.ForMathlib.Computability.TuringMachine.BusyBeavers
 import FormalConjectures.ForMathlib.Computability.TuringMachine.PostTuringMachine
-import FormalConjectures.ForMathlib.Data.Finset.Empty
 import FormalConjectures.ForMathlib.Data.Finset.OrdConnected
 import FormalConjectures.ForMathlib.Data.Nat.Factorization.Basic
 import FormalConjectures.ForMathlib.Data.Nat.Full
diff --git a/FormalConjectures/Wikipedia/AgohGiuga.lean b/FormalConjectures/Wikipedia/AgohGiuga.lean
@@ -160,13 +160,17 @@ theorem korselts_criterion (a : ℕ) (ha₁ : a.Composite) :
     refine if hb : _ = 0 then ⟨0, hb⟩ else (a.factorization_le_iff_dvd ha₁.1.ne_bot hb).1 fun p => ?_
     by_cases hp : p.Prime
     · by_cases hpa : p ∣ a
-      · obtain ⟨_, h⟩ := h_dvd p hp hpa
+      · obtain ⟨w, h⟩ := h_dvd p hp hpa
         obtain ⟨ha₁, ha₂⟩ := ha₁
         apply Nat.Prime.pow_dvd_iff_le_factorization hp hb |>.1
         have : a.factorization p ≤ 1 := not_lt.1 fun h =>
           h_sqfr p hp <| (sq p ▸ (pow_dvd_pow p h).trans (a.ordProj_dvd p))
-        field_simp [h, pow_mul, le_antisymm this (hp.dvd_iff_one_le_factorization _ |>.1 _),
-          ← CharP.cast_eq_zero_iff (ZMod p)]
+        replace : a.factorization p = 1 :=
+          this.antisymm (hp.dvd_iff_one_le_factorization (by grind) |>.1 hpa)
+        simp_rw [this, pow_one, ← CharP.cast_eq_zero_iff (ZMod p)]
+        have one_le_b_pow : 1 ≤ b ^ (a - 1) := by omega
+        push_cast [one_le_b_pow]
+        simp_rw [h, pow_mul]
         simp_all +decide [CharP.cast_eq_zero_iff _ p,
           hp.coprime_iff_not_dvd.1 (hab.of_dvd_left (by aesop)), ZMod.pow_card_sub_one_eq_one]
       · simp [a.factorization_eq_zero_of_not_dvd hpa]
diff --git a/FormalConjectures/Wikipedia/Mandelbrot.lean b/FormalConjectures/Wikipedia/Mandelbrot.lean
@@ -72,14 +72,16 @@ theorem multibrotSet_eq {n : ℕ} (hn : 2 ≤ n) :
         refine .trans ?_ <| norm_sub_le_norm_add _ _
         replace hm :
             r ^ n + a * n ^ m * r ^ (n - 1) * ↑n ≤ ‖(fun z ↦ z ^ n + c)^[k + m] 0‖ ^ n := by
-          refine .trans ?_ (pow_le_pow_left₀ (by positivity) hm n); cases n; simp
+          grw [← hm]
+          cases n
+          · simp
           rw [add_comm r _, add_pow]
           refine .trans ?_ <| Finset.add_le_sum (by intros; positivity) ?_ ?_ zero_ne_one <;> simp
         rw [norm_pow, pow_succ]
-        refine .trans ?_ (sub_le_sub hm h')
+        grw [← hm, h']
         rw [hr', hr'', show ‖(fun z ↦ z ^ n + c)^[k] 0‖ = a + r by simp [a]]
         suffices a ≤ a * (n * n ^ m) by linarith
-        refine (mul_one a).symm.trans_le <| (mul_le_mul_left ha).2 ?_
+        rw [le_mul_iff_one_le_right ha]
         have hn : 1 ≤ (n : ℝ) := Nat.one_le_cast.2 hn.le
         simpa using mul_le_mul hn (one_le_pow₀ hn)
     rw [← tendsto_norm_atTop_iff_cobounded]
diff --git a/FormalConjectures/Wikipedia/ModularityConjecture.lean b/FormalConjectures/Wikipedia/ModularityConjecture.lean
@@ -41,7 +41,7 @@ open scoped UpperHalfPlane Real ModularForm CongruenceSubgroup
 
 /-- The `n`-th Fourier coefficient of a modular forms (around the cusp at infinity). -/
 noncomputable def modularFormAn (n : ℕ) {N : ℕ} {k : ℤ} (f : CuspForm (Gamma0 N) k) : ℂ :=
-  (qExpansion N f).coeff ℂ n
+  (qExpansion N f).coeff n
 
 local notation:73 "a_[" n:0 "]" f:72 => modularFormAn n f
 
diff --git a/FormalConjectures/Wikipedia/RamanujanTau.lean b/FormalConjectures/Wikipedia/RamanujanTau.lean
@@ -36,7 +36,7 @@ open PowerSeries PowerSeries.WithPiTopology
 
 noncomputable def Δ : PowerSeries ℤ := X * ∏' (n : ℕ+), (1 - X ^ (n : ℕ)) ^ 24
 
-noncomputable def τ (n : ℕ) : ℤ := PowerSeries.coeff ℤ n Δ
+noncomputable def τ (n : ℕ) : ℤ := PowerSeries.coeff n Δ
 
 
 @[category API, AMS 11]
diff --git a/FormalConjectures/Wikipedia/SumOfThreeCubes.lean b/FormalConjectures/Wikipedia/SumOfThreeCubes.lean
@@ -75,13 +75,13 @@ The below parametrization is brought from the MSE answer [MSE].
 theorem isSumOfThreeCubesRat_any (r : ℚ) : IsSumOfThreeCubes r := by
   by_cases h : r = 0
   · exact ⟨0, 0, 0, by norm_num; exact h⟩
-  · push_neg at h
-    let x := (r ^ 6 + 45 * r ^ 4 - 81 * r ^ 2 + 27) / (6 * r * (r ^ 2 + 3) ^ 2)
+  · let x := (r ^ 6 + 45 * r ^ 4 - 81 * r ^ 2 + 27) / (6 * r * (r ^ 2 + 3) ^ 2)
     let y := (3 - r ^ 2) * (6 * r) / (r ^ 2 + 3) ^ 2
     let z := (r ^ 2 + 6 * r + 3) * (- r ^ 2 + 6 * r - 3) / (6 * r * (r ^ 2 + 3))
     use x, y, z
-    field_simp [x, y, z]
-    ring_nf
+    simp only [x, y, z]
+    field_simp
+    ring
 
 
 /-- An integer `n : ℤ` can be written as a sum of three cubes (of integers) if and only if
diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml
@@ -10,7 +10,7 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.22.0"
+rev = "v4.23.0"
 
 [[lean_exe]]
 name = "overwrite_index"
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
+   "rev": "37df177aaa770670452312393d4e84aaad56e7b6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "v4.23.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
+   "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,57 +35,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
+   "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
+   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.68",
+   "inputRev": "v0.0.71",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
+   "rev": "247ff80701c76760523b5d7c180b27b7708faf38",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
+   "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
+   "rev": "d117e2c28cba42e974bc22568ac999492a34e812",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
diff --git a/lean-toolchain b/lean-toolchain
