Merge branch 'bump/nightly-2025-12-10' into nightly-testing

Author: kim-em

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