chore: bump to nightly-2025-12-07 (#685)

Author: david-christiansen

Manual/Grind/Algebra.lean

@@ -307,6 +307,7 @@ h_2 : ¬y * x = 1
   [facts] Asserted facts
   [eqc] False propositions
   [eqc] Equivalence classes
+  [ematch] E-matching patterns
   [linarith] Linarith assignment for `α`
 ```
 
@@ -369,6 +370,7 @@ h_4 : ¬t ^ 2 = t + 1
   [eqc] True propositions
   [eqc] False propositions
   [eqc] Equivalence classes
+  [ematch] E-matching patterns
   [ring] Ring `α`
   [limits] Thresholds reached
 ```

Manual/Grind/Cutsat.lean

@@ -101,6 +101,7 @@ h_2 : 2 ∣ 2 * a + b
 [grind] Goal diagnostics
   [facts] Asserted facts
   [eqc] True propositions
+  [ematch] E-matching patterns
   [linarith] Linarith assignment for `Int`
 ```
 ::::
@@ -175,6 +176,7 @@ h : x * x + 1 ≤ 0
 [grind] Goal diagnostics
   [facts] Asserted facts
   [eqc] True propositions
+  [ematch] E-matching patterns
   [cutsat] Assignment satisfying linear constraints
 ```
 
@@ -193,6 +195,7 @@ h : x * x + 1 ≤ 0
 [grind] Goal diagnostics
   [facts] Asserted facts
   [eqc] True propositions
+  [ematch] E-matching patterns
   [cutsat] Assignment satisfying linear constraints
 ```
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-12-04
+leanprover/lean4:nightly-2025-12-07