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

Author: kim-em

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -225,6 +225,14 @@ end Fewnomials
 theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
     coeff (p * Polynomial.X ^ n) (d + n) = coeff p d := by
   rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
+  #adaptation_note
+  /--
+  It may be possible to change this back to
+  `all_goals grind [mem_antidiagonal, mul_zero]`
+  on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+  but if not just remove this note.
+  The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+  -/
   · rintro ⟨i, j⟩ h1 h2
     rw [coeff_X_pow, if_neg, mul_zero]
     grind [mem_antidiagonal]

Mathlib/Algebra/Polynomial/RuleOfSigns.lean

@@ -313,6 +313,14 @@ theorem succ_signVariations_le_X_sub_C_mul (hη : 0 < η) (hP : P ≠ 0) :
   · --P is zero degree, therefore a constant.
     have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
     have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
+      #adaptation_note
+      /--
+      It may be possible to change this back to
+      `grind [coeff_X_sub_C_mul, mul_zero, coeff_eq_zero_of_natDegree_lt]`
+      on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+      but if not just remove this note.
+      The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+      -/
       simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]
     dsimp [signVariations, coeffList]
     rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]

Mathlib/Data/ENNReal/Inv.lean

@@ -231,11 +231,29 @@ protected theorem div_le_iff' {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ 
 protected theorem mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) :
     (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
   cases b
-  case top => simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true,
-    or_true, mul_top, inv_top, mul_zero]
+  case top =>
+    #adaptation_note
+    /--
+    It may be possible to change this back to
+    `grind [mul_top, mul_zero, inv_top, ENNReal.inv_eq_zero]`
+    on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+    but if not just remove this note.
+    The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+    -/
+    simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true, or_true,
+      mul_top, inv_top, mul_zero]
   cases a
-  case top => simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self,
-    not_true_eq_false, coe_eq_zero, false_or, top_mul, inv_top, zero_mul]
+  case top =>
+    #adaptation_note
+    /--
+    It may be possible to change this back to
+    `grind [top_mul, zero_mul, inv_top, ENNReal.inv_eq_zero]`
+    on nightly-2025-12-14 (or ideally without needing the `zero_mul`),
+    but if not just remove this note.
+    The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `zero_mul`) by e-matching.
+    -/
+    simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self, not_true_eq_false,
+      coe_eq_zero, false_or, top_mul, inv_top, zero_mul]
   grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero,
     =_ coe_inv, zero_mul, = mul_eq_zero, mul_top, mul_zero, top_mul]
 

Mathlib/Tactic/Eqns.lean

@@ -37,6 +37,7 @@ open Lean Elab
 
 syntax (name := eqns) "eqns" (ppSpace ident)* : attr
 
+-- #adaptation_note: this will be renamed back to `NameMapExtension'` on `nightly-2025-12-14`.
 initialize eqnsAttribute : NameMapExtension' (Array Name) ←
   registerNameMapAttribute {
     name  := `eqns

lake-manifest.json

@@ -56,7 +56,7 @@
    "subDir": null,
    "scope": "leanprover-community",
    "rev": "0a83ad726ee0236e9574ef48098beedca30aa5a0",
-   "name": "quote4",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
    "inherited": false,

lakefile.lean

@@ -7,7 +7,7 @@ open Lake DSL
 -/
 
 require "leanprover-community" / "batteries" @ git "nightly-testing"
-require "leanprover-community" / "quote4" @ git "nightly-testing"
+require "leanprover-community" / "Qq" @ git "nightly-testing"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.83-pre2" -- ProofWidgets should always be pinned to a specific version
   with NameMap.empty.insert `errorOnBuild