Skip to content

Commit 29798ff

Browse files
committed
Merge branch 'bump/nightly-2025-12-13' into nightly-testing
2 parents 8dd51cf + 5fead68 commit 29798ff

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -621,7 +621,7 @@ def eraseMiddle (c : OrderedFinpartition (n + 1)) (hc : range (c.emb 0) ≠ {0})
621621
congr 1
622622
rw [← val_eq_val]
623623
simp only [val_cast, val_succ, val_pred]
624-
lia
624+
omega
625625
· have A : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i := by
626626
simp [hi]
627627
exact ⟨i, Fin.cast A.symm j, by simp [hi, hij]⟩

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:nightly-2025-12-13
1+
leanprover/lean4:nightly-2025-12-13

0 commit comments

Comments
 (0)