From 75f99635f27dbbedae9769395460b33092180b46 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 20:21:38 +0100
Subject: Lean 4.25

---
 BinaryHeap/CompleteTree/AdditionalProofs/Get.lean | 2 +-
 lean-toolchain                                    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index aad82c5..88ec994 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -18,7 +18,7 @@ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fi
       unfold leftLen rightLen length
       split
       intro h₂
-      rename_i o p v l r _ _ _
+      rename_i o p v l r _ _ _ _
       have h₃ := index.isLt
       apply Nat.sub_lt_right_of_lt_add
       omega
diff --git a/lean-toolchain b/lean-toolchain
index 077c4ce..f942ecf 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.24.0
+leanprover/lean4:4.25.0
-- 
cgit v1.2.3