chore: adaptations for nightly-2025-12-10 (#141)

Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>

Author: 5 people

Mathlib/Geometry/Euclidean/Incenter.lean

@@ -699,7 +699,7 @@ lemma ExcenterExists.affineSpan_faceOpposite_eq_orthRadius [hf : Fact (Module.fi
   rw [direction_affineSpan, (s.faceOpposite i).independent.finrank_vectorSpan_add_one,
     Fintype.card_fin, hf.out]
   have := NeZero.ne n
-  cutsat
+  lia
 
 lemma affineSpan_faceOpposite_eq_orthRadius_insphere [Fact (Module.finrank ℝ V = n)]
     (i : Fin (n + 1)) :

Mathlib/NumberTheory/MahlerMeasure.lean

@@ -40,7 +40,7 @@ local notation3 "BoxPoly" =>
   {p : ℤ[X] | p.natDegree < n + 1 ∧ ∀ i, B₁ i ≤ p.coeff i ∧ p.coeff i ≤ B₂ i}
 
 open Finset in
-theorem card_eq_of_natDegree_le_of_coeff_le (h_B : ∀ i, ⌈B₁ i⌉ ≤ ⌊B₂ i⌋) :
+theorem card_eq_of_natDegree_le_of_coeff_le :
     Set.ncard BoxPoly = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat := by
   let e : BoxPoly ≃ Icc (⌈B₁ ·⌉) (⌊B₂ ·⌋) := {
     toFun p := ⟨toFn (n + 1) p, by
@@ -67,11 +67,8 @@ private lemma card_mahlerMeasure (n : ℕ) (B : ℝ≥0) :
   have h_card :
       Set.ncard {p : ℤ[X] | p.natDegree < n + 1 ∧ ∀ i : Fin (n + 1), ‖p.coeff i‖ ≤ n.choose i * B} =
       ∏ i : Fin (n + 1), (2 * ⌊n.choose i * B⌋₊ + 1) := by
-    have h_B (i : Fin (n + 1)) : ⌈-(n.choose i * B  : ℝ)⌉ ≤ ⌊(n.choose i * B : ℝ)⌋ := by
-      simp only [ceil_neg, neg_le_self_iff, floor_nonneg]
-      positivity
     conv => enter [1, 1, 1, p, 2, i]; rw [norm_eq_abs, abs_le]
-    rw [card_eq_of_natDegree_le_of_coeff_le h_B]
+    rw [card_eq_of_natDegree_le_of_coeff_le]
     simp only [ceil_neg, sub_neg_eq_add, ← two_mul]
     apply Finset.prod_congr rfl fun i _ ↦ ?_
     zify

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bda61ace1e2fbf73689899a8b3ca5fc74b0e21b1",
+   "rev": "80627bbde8b8a0474814092e1dd2aff89123cc1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lakefile.lean

@@ -177,7 +177,7 @@ update its toolchain to match Mathlib's and fetch the new cache.
 -/
 post_update pkg do
   let rootPkg ← getRootPackage
-  if rootPkg.name = pkg.name then
+  if rootPkg.baseName = pkg.baseName then
     return -- do not run in Mathlib itself
   if (← IO.getEnv "MATHLIB_NO_CACHE_ON_UPDATE") != some "1" then
     -- Check if Lake version matches toolchain version
@@ -204,4 +204,4 @@ post_update pkg do
     finally
       IO.Process.setCurrentDir cwd
     if exitCode ≠ 0 then
-      error s!"{pkg.name}: failed to fetch cache"
+      error s!"{pkg.baseName}: failed to fetch cache"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-12-09
+leanprover/lean4:nightly-2025-12-10