From 6d10b7594f487bdfbef99d05bda34405dd85c8b8 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 16 Nov 2025 14:24:46 +0100 Subject: Lean 4.23 --- Day9.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Day9.lean') diff --git a/Day9.lean b/Day9.lean index 8fc449c..ac8edd8 100644 --- a/Day9.lean +++ b/Day9.lean @@ -31,7 +31,7 @@ private def extrapolate : List Int → Int 0 else have : (differences (a :: as)).length < as.length + 1 := by - simp +arith[differences] + simp +arith induction (as) <;> simp +arith[differences] case cons b bs hb => rw[←differences_length_independent_arg] assumption -- cgit v1.2.3