From a2fcff2dbe3561e3a51b810b3f0577ba99ef5e78 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 13 Feb 2025 22:33:06 +0100
Subject: Lean 4.16

---
 BinaryHeap/CompleteTree/AdditionalOperations.lean | 11 ++++++++---
 BinaryHeap/CompleteTree/AdditionalProofs/Get.lean |  4 ++--
 BinaryHeap/CompleteTree/HeapOperations.lean       |  8 +++-----
 lean-toolchain                                    |  2 +-
 4 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean
index 100af76..82dfbe9 100644
--- a/BinaryHeap/CompleteTree/AdditionalOperations.lean
+++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean
@@ -34,9 +34,14 @@ def indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Opti
 
 /--Returns the element at the given index. Indices are depth first.-/
 def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) : α :=
-  match n, index, heap with
-  | (_+_+1), 0, .branch v _ _ _ _ _ => v
-  | (o+p+1), ⟨j+1,h₃⟩, .branch _ l r _ _ _ =>
+  --this all was one match in Lean 4.15, but I couldn't get it to unfold properly in 4.16...
+  match index with
+  | ⟨0, _⟩ =>
+    match n, heap with
+    | (_+_+1), .branch v _ _ _ _ _ => v
+  | ⟨j+1, h₃⟩ =>
+    match n, heap with
+    | (o+p+1), .branch _ l r _ _ _ =>
     if h₄ : j < o then
       get ⟨j, h₄⟩ l
     else
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index 5c9552b..b8d94e5 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -36,7 +36,7 @@ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fi
     else by
       simp only[right_unfold, leftLen_unfold]
       have : j + 1 - o - 1 = j - o := by omega
-      simp (config := {autoUnfold := true})[this, h₄]
+      simp only [get, reduceDIte, this, h₄]
 
 theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r : CompleteTree α m} {m_le_n : m ≤ n} {max_height_diff : n < 2 * (m + 1)} {subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo} (index : Fin (n + m + 1)) (h₁ : index > n) :
   have h₂ : ↑index - n - 1 < m := by
@@ -62,7 +62,7 @@ theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin
     if h₄ : j < o then by
       simp only[left_unfold, leftLen_unfold]
       have : j + 1 - o - 1 = j - o := by omega
-      simp (config := {autoUnfold := true})[this, h₄]
+      simp only [get, h₄, reduceDIte, Nat.add_one_sub_one]
     else
       absurd (Nat.lt_of_succ_le h₃) h₄
 
diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean
index 202ff5e..e2b0019 100644
--- a/BinaryHeap/CompleteTree/HeapOperations.lean
+++ b/BinaryHeap/CompleteTree/HeapOperations.lean
@@ -109,12 +109,10 @@ private theorem removeRightLeftIsFull {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextP
   cases r
   case inl h₁ => rewrite[Nat.not_lt_eq] at h₁
                  have h₂ := Nat.le_antisymm h₁ m_le_n
-                 rewrite[←h₂] at subtree_complete
-                 simp at subtree_complete
-                 assumption
-  case inr h₁ => simp(config := {zetaDelta := true })[←Nat.power_of_two_iff_next_power_eq] at h₁
-                 simp[h₁] at subtree_complete
+                 rewrite[←h₂, or_self] at subtree_complete
                  assumption
+  case inr h₁ => simp[←Nat.power_of_two_iff_next_power_eq] at h₁
+                 exact Or.resolve_right subtree_complete h₁
 
 /-- Helper for heapRemoveLastAux -/
 private theorem stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo = m+1 : Bool))) (m_le_n : m ≤ n) (m_gt_0 : m > 0) (leftIsFull : (n+1).isPowerOfTwo) (max_height_difference: n < 2 * (m + 1)) : n < 2*m := by
diff --git a/lean-toolchain b/lean-toolchain
index f1f4005..b1c65af 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.15.0
+leanprover/lean4:4.16.0
-- 
cgit v1.2.3