Fix compilation with Lean 4.10.

9 files changed, 92 insertions, 102 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
index e99617b..487a50f 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
@@ -73,7 +73,7 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete
     have h₄ : j = indexl.val := Nat.succ.inj $ h₃.subst (motive := λx↦ x = indexl.val + 1) h₂
     have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl
     have h₅ : j < p := by simp only [this, indexl.isLt, h₄]
-    simp only [h₅, ↓reduceDite, Nat.add_eq]
+    simp only [h₅, ↓reduceDIte, Nat.add_eq]
     unfold get at prereq
     split at prereq
     rename_i pp ii ll _ hel hei heq _
@@ -121,7 +121,7 @@ private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : Complete
       exact Nat.succ.inj h₂
     have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl
     have h₅ : ¬(j < p) := by simp_arith [this, h₄]
-    simp only [h₅, ↓reduceDite, Nat.add_eq]
+    simp only [h₅, ↓reduceDIte, Nat.add_eq]
     unfold get at prereq
     split at prereq
     rename_i pp ii rr _ hel hei heq _
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
index 937e6d0..796130f 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
@@ -13,7 +13,7 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)
     split
     rename_i n m v l r _ _ _
     have h₂ : 0 = n + m := Eq.symm $  Nat.eq_zero_of_le_zero $ Nat.le_of_not_gt h₁
-    simp only [h₂, ↓reduceDite, id_eq, root_unfold]
+    simp only [h₂, ↓reduceDIte, id_eq, root_unfold]
     have : n = 0 := And.left $ Nat.add_eq_zero.mp h₂.symm
     subst n
     have : m = 0 := And.right $ Nat.add_eq_zero.mp h₂.symm
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index c29fc3f..92efdbc 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -58,7 +58,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N
       subst vv ll rr
       split at he₁
       <;> rename_i goLeft
-      <;> simp only [goLeft, and_self, ↓reduceDite, Fin.isValue]
+      <;> simp only [goLeft, and_self, ↓reduceDIte, Fin.isValue]
       case' isTrue =>
         cases l;
         case leaf => exact absurd goLeft.left $ Nat.not_lt_zero m
@@ -80,7 +80,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N
       case' isFalse =>
         have : ¬j<n := by omega --from he₁. It has j = something + n.
       all_goals
-        simp only [this, ↓reduceDite, Nat.pred_succ, Fin.isValue]
+        simp only [this, ↓reduceDIte, Nat.pred_succ, Fin.isValue]
         subst j -- overkill, but unlike rw it works
         simp only [Nat.pred_succ, Fin.isValue, Nat.add_sub_cancel, Fin.eta]
         apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex
@@ -247,51 +247,13 @@ revert h₁
 unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux
 intro h₁
 split at h₁
-rename_i o p v l r _ _ _ _
+rename_i o p v l r _ _ _
 simp only [Nat.add_eq, ne_eq] at h₂
-simp only [Nat.add_eq, h₂, ↓reduceDite, decide_eq_true_eq, Fin.zero_eta, Fin.isValue,
+simp only [Nat.add_eq, h₂, ↓reduceDIte, decide_eq_true_eq, Fin.zero_eta, Fin.isValue,
   Nat.succ_eq_add_one, Fin.castLE_succ, Nat.pred_eq_sub_one, gt_iff_lt] at h₁ ⊢
-split
-case isFalse h₃ =>
-  --removed right
-  simp only [h₃, ↓reduceDite, Fin.isValue] at h₁ ⊢
-  cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢
-  case zero =>
-    simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃
-    subst o
-    contradiction
-  case succ pp _ _ _ _ =>
-    generalize hold : get index (branch v l r _ _ _) _ = oldValue
-    have h₄ : index ≠ 0 := Fin.ne_zero_of_gt h₁
-    have h₅ : index.pred h₄ > o := by
-      simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt]
-      rewrite[Fin.lt_iff_val_lt_val] at h₁
-      simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁
-      exact Nat.lt_of_add_right $ Nat.lt_pred_of_succ_lt h₁
-    have h₆ : index > o :=  Nat.lt_of_add_left $ Nat.succ_lt_of_lt_pred h₅
-    have h₇ : ↑index - o - 1 < pp + 1 :=
-      have : ↑index < (o + 1) + (pp + 1) := (Nat.add_comm_right o (pp+1) 1).subst index.isLt
-      have : ↑index < (pp + 1) + (o + 1) := (Nat.add_comm (o+1) (pp+1)).subst this
-      (Nat.sub_lt_of_lt_add this (Nat.succ_le_of_lt h₆) : ↑index - (o + 1) < pp + 1)
-    have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd :=
-      Nat.lt_sub_of_add_lt (b := o+1) h₁
-    rewrite[get_right' _ h₅]
-    rewrite[get_right' _ h₆] at hold
-    rewrite[←hold]
-    have h₉ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨↑index - o - 1, h₇⟩ h₈
-    unfold Internal.heapRemoveLastWithIndex at h₉
-    unfold Fin.pred Fin.subNat at h₉
-    simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one] at h₉
-    simp only [Nat.add_eq, Fin.coe_pred, Fin.isValue]
-    have : ↑index - 1 - o - 1 = ↑index - o - 1 - 1 :=
-      (rfl : ↑index - (o + 1 + 1) = ↑index - (o + 1 + 1))
-      |> (Nat.add_comm o 1).subst (motive := λx ↦ ↑index - (x + 1) = ↑index - (o + 1 + 1))
-      |> (Nat.sub_sub ↑index 1 (o+1)).substr
-    --exact this.substr h₉ --seems to run into a Lean 4.9 bug when proving termination
-    simp only [this, Nat.add_eq, Fin.isValue, h₉] --no idea why simp avoids the same issue...
-case isTrue h₃ =>
+if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then
   --removed left
-  simp only [h₃, and_self, ↓reduceDite, Fin.isValue] at h₁ ⊢
+  simp only [h₃, and_self, ↓reduceDIte, Fin.isValue] at h₁ ⊢
   cases o
   case zero => exact absurd h₃.left $ Nat.not_lt_zero p
   case succ oo _ _ _ _ =>
@@ -338,6 +300,43 @@ case isTrue h₃ =>
       have h₈ : ⟨↑index - 1, Nat.lt_succ.mpr h₇⟩ > (Internal.heapRemoveLastWithIndex l).snd.snd :=
         Nat.lt_sub_of_add_lt h₁
       exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt l ⟨↑index - 1, Nat.lt_succ.mpr h₇⟩ h₈
+else
+  --removed right
+  simp only [h₃, ↓reduceDIte, Fin.isValue] at h₁ ⊢
+  cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢
+  case zero =>
+    simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃
+    subst o
+    contradiction
+  case succ pp _ _ _ _ =>
+    generalize hold : get index (branch v l r _ _ _) _ = oldValue
+    have h₄ : index ≠ 0 := Fin.ne_zero_of_gt h₁
+    have h₅ : index.pred h₄ > o := by
+      simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt]
+      rewrite[Fin.lt_iff_val_lt_val] at h₁
+      simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁
+      exact Nat.lt_of_add_right $ Nat.lt_pred_of_succ_lt h₁
+    have h₆ : index > o :=  Nat.lt_of_add_left $ Nat.succ_lt_of_lt_pred h₅
+    have h₇ : ↑index - o - 1 < pp + 1 :=
+      have : ↑index < (o + 1) + (pp + 1) := (Nat.add_comm_right o (pp+1) 1).subst index.isLt
+      have : ↑index < (pp + 1) + (o + 1) := (Nat.add_comm (o+1) (pp+1)).subst this
+      (Nat.sub_lt_of_lt_add this (Nat.succ_le_of_lt h₆) : ↑index - (o + 1) < pp + 1)
+    have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd :=
+      Nat.lt_sub_of_add_lt (b := o+1) h₁
+    rewrite[get_right' _ h₅]
+    rewrite[get_right' _ h₆] at hold
+    rewrite[←hold]
+    have h₉ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨↑index - o - 1, h₇⟩ h₈
+    unfold Internal.heapRemoveLastWithIndex at h₉
+    unfold Fin.pred Fin.subNat at h₉
+    simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one] at h₉
+    simp only [Nat.add_eq, Fin.coe_pred, Fin.isValue]
+    have : ↑index - 1 - o - 1 = ↑index - o - 1 - 1 :=
+      (rfl : ↑index - (o + 1 + 1) = ↑index - (o + 1 + 1))
+      |> (Nat.add_comm o 1).subst (motive := λx ↦ ↑index - (x + 1) = ↑index - (o + 1 + 1))
+      |> (Nat.sub_sub ↑index 1 (o+1)).substr
+    --exact this.substr h₉ --seems to run into a Lean 4.10 bug when proving termination
+    simp only [this, Nat.add_eq, Fin.isValue, h₉] --no idea why simp avoids the same issue...
 
 protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) (h₁ : index < (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd) :
   have hn : n > 0 := Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt)
@@ -361,14 +360,41 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea
     unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux
     intro h₁
     split at h₁
-    rename_i o p v l r _ _ _ _
+    rename_i o p v l r _ _ _
     simp only [Nat.add_eq, ne_eq] at h₃
     simp only [h₃, Nat.add_eq, Fin.zero_eta, Fin.isValue, decide_eq_true_eq, Nat.succ_eq_add_one,
-      Fin.castLE_succ, Nat.pred_eq_sub_one, reduceDite] at h₁ ⊢
-    split
-    case isFalse h₄ =>
+      Fin.castLE_succ, Nat.pred_eq_sub_one, reduceDIte] at h₁ ⊢
+    if h₄ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then
+      --removed left
+      --get has to go into the square hole - erm, left branch too
+      cases o
+      case zero =>
+        exact absurd h₄.left $ Nat.not_lt_zero _
+      case succ oo _ _ _ _ =>
+        rewrite[Fin.lt_iff_val_lt_val] at h₁
+        simp only [Nat.add_eq, h₄, and_self, ↓reduceDIte, Fin.isValue, Fin.val_succ,
+          Fin.coe_castLE] at h₁ ⊢
+        have h₂₂ : index > 0 := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂
+        have h₆ := (Nat.add_comm_right oo 1 p).subst hi
+        have h₈ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) > ⟨0,Nat.succ_pos _⟩ := h₂₂
+        have h₇ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) ≤ oo := by
+          generalize (Internal.heapRemoveLastAux l (β := λn ↦ α × Fin n) _ _ _).2.snd = i at h₁
+          have a : i.val ≤ oo := Nat.le_of_lt_succ i.isLt
+          have b : index.val ≤ i.val := Nat.le_of_lt_succ h₁
+          exact Nat.le_trans b a
+        have h₅ : index ≤ oo+1 := Nat.le_succ_of_le h₇
+        rewrite[get_left' _ h₂₂ h₅]
+        rewrite[heapRemoveLastWithIndexRelationGt_Aux2]
+        case h₃ => exact Nat.succ_pos _
+        case h₄ => exact h₆
+        rewrite[get_left' _ h₈ h₇]
+        have : index.val - 1 < oo + 1 := Nat.sub_one_lt_of_le h₂₂ h₅
+        have h₉ : ⟨↑index - 1, this⟩ < (Internal.heapRemoveLastWithIndex l).snd.snd :=
+            Nat.sub_lt_of_lt_add h₁ h₂₂
+        exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt l ⟨↑index - 1, _⟩ h₉
+    else
       --removed right
-      simp only [h₄, ↓reduceDite, Fin.isValue] at h₁ ⊢
+      simp only [h₄, ↓reduceDIte, Fin.isValue] at h₁ ⊢
       cases p
       case zero =>
         simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄
@@ -398,34 +424,6 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea
           have h₅ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) ≤ o := h₄₂
           have h₆ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) > ⟨0,Nat.succ_pos _⟩ := h₂₂
           rw[get_left' _ h₆ h₅]
-    case isTrue h₄ =>
-      --removed left
-      --get has to go into the square hole - erm, left branch too
-      cases o
-      case zero =>
-        exact absurd h₄.left $ Nat.not_lt_zero _
-      case succ oo _ _ _ _ =>
-        rewrite[Fin.lt_iff_val_lt_val] at h₁
-        simp only [Nat.add_eq, h₄, and_self, ↓reduceDite, Fin.isValue, Fin.val_succ,
-          Fin.coe_castLE] at h₁ ⊢
-        have h₂₂ : index > 0 := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂
-        have h₆ := (Nat.add_comm_right oo 1 p).subst hi
-        have h₈ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) > ⟨0,Nat.succ_pos _⟩ := h₂₂
-        have h₇ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) ≤ oo := by
-          generalize (Internal.heapRemoveLastAux l (β := λn ↦ α × Fin n) _ _ _).2.snd = i at h₁
-          have a : i.val ≤ oo := Nat.le_of_lt_succ i.isLt
-          have b : index.val ≤ i.val := Nat.le_of_lt_succ h₁
-          exact Nat.le_trans b a
-        have h₅ : index ≤ oo+1 := Nat.le_succ_of_le h₇
-        rewrite[get_left' _ h₂₂ h₅]
-        rewrite[heapRemoveLastWithIndexRelationGt_Aux2]
-        case h₃ => exact Nat.succ_pos _
-        case h₄ => exact h₆
-        rewrite[get_left' _ h₈ h₇]
-        have : index.val - 1 < oo + 1 := Nat.sub_one_lt_of_le h₂₂ h₅
-        have h₉ : ⟨↑index - 1, this⟩ < (Internal.heapRemoveLastWithIndex l).snd.snd :=
-            Nat.sub_lt_of_lt_add h₁ h₂₂
-        exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt l ⟨↑index - 1, _⟩ h₉
 
 protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)):
   let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index 7ac98c9..bc7ca14 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -68,7 +68,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
         simp
         if h : j < oo + 1 then
           -- index was in l
-          simp only [h, ↓reduceDite] at h₃
+          simp only [h, ↓reduceDIte] at h₃
           split
           case isTrue =>
             simp
@@ -111,7 +111,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
               exists ⟨j, h⟩
         else
           -- index was in r
-          simp only [h, ↓reduceDite] at h₃
+          simp only [h, ↓reduceDIte] at h₃
           rename_i h₄ _ _ _ _
           have h₄ : j - (oo + 1) < pp + 1 := Nat.sub_lt_left_of_lt_add (Nat.le_of_not_gt h) (Nat.lt_of_succ_lt_succ h₄)
           split
@@ -162,10 +162,10 @@ theorem heapUpdateRootContainsUpdatedElement {α : Type u} {n : Nat} (tree : Com
   unfold heapUpdateRoot
   split
   rename_i o p v l r _ _ _ h₁
-  cases o <;> simp only [Nat.add_eq, Nat.succ_eq_add_one, Nat.add_one_ne_zero, ↓reduceDite]
+  cases o <;> simp only [Nat.add_eq, Nat.succ_eq_add_one, Nat.add_one_ne_zero, ↓reduceDIte]
   case zero => simp only [contains, true_or]
   case succ oo _ _ _ =>
-    cases p <;> simp only [Nat.add_one_ne_zero, ↓reduceDite]
+    cases p <;> simp only [Nat.add_one_ne_zero, ↓reduceDIte]
     case zero =>
       split
       case isTrue => simp only [contains, true_or]
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
index e9c357d..29e9837 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
@@ -117,12 +117,12 @@ private theorem heapRemoveLastAuxIsHeap
   rename_i n m v l r _ _ _
   exact
     if h₄ : 0 = (n+m) then by
-      simp only [h₄, reduceDite, castZeroHeap]
+      simp only [h₄, reduceDIte, castZeroHeap]
     else by
       simp[h₄]
       exact
         if h₅ : (m<n ∧ Nat.nextPowerOfTwo (m+1) = m+1) then by
-          simp only [h₅, and_self, ↓reduceDite]
+          simp only [h₅, and_self, ↓reduceDIte]
           cases n
           case zero =>
             exact absurd h₅.left $ Nat.not_lt_zero m
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
index 90991d8..b50d8c5 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
@@ -26,7 +26,7 @@ private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat}
     unfold heapUpdateRoot
     split
     rename_i o p v l r h₆ h₇ h₈ h₂
-    cases o <;> cases p <;> simp only [↓reduceDite,HeapPredicate.leOrLeaf, root_unfold, h₄, reflexive_le]
+    cases o <;> cases p <;> simp only [↓reduceDIte,HeapPredicate.leOrLeaf, root_unfold, h₄, reflexive_le]
     <;> unfold HeapPredicate at h₁
     <;> have h₁₀ : le value $ l.root (by omega) := h₅ value v (l.root _) ⟨h₃, h₁.right.right.left⟩
     simp only [↓reduceIte, Nat.add_zero, h₁₀, root_unfold, h₄, reflexive_le]
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
index 0788180..e930a30 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
@@ -60,7 +60,7 @@ have h₃ : 0 < leftLen heap h₂ := heapUpdateRootPossibleRootValuesAuxL heap (
   case zero => simp only[root, true_or]
   case succ oo =>
     have h₆ : p = 0 := by simp at h₁; omega
-    simp only [h₆, ↓reduceDite]
+    simp only [h₆, ↓reduceDIte]
     cases le value (l.root _)
     <;> simp[heapUpdateRootReturnsRoot, root_unfold, left_unfold]
 
@@ -81,7 +81,7 @@ have h₄ : 0 < rightLen heap h₂ := heapUpdateRootPossibleRootValuesAuxR heap
   case zero => simp only[root, true_or]
   case succ oo =>
     have h₆ : p ≠ 0 := by simp at h₁; omega
-    simp only [Nat.add_one_ne_zero, ↓reduceDite, h₆]
+    simp only [Nat.add_one_ne_zero, ↓reduceDIte, h₆]
     cases le value (l.root _) <;> simp
     rotate_right
     cases le value (r.root _) <;> simp
@@ -161,7 +161,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v
     rename_i o p v l r h₇ h₈ h₉ heq
     exact
       if h₁₀ : o = 0 then by
-        simp only [Nat.add_eq, Nat.succ_eq_add_one, h₁₀, ↓reduceDite]
+        simp only [Nat.add_eq, Nat.succ_eq_add_one, h₁₀, ↓reduceDIte]
         unfold HeapPredicate at h₂ ⊢
         simp only [h₂, true_and]
         unfold HeapPredicate.leOrLeaf
@@ -172,7 +172,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v
         case right => match p, r with
         | Nat.zero, _ => trivial
       else if h₁₁ : p = 0 then by
-        simp only [↓reduceDite, h₁₀, h₁₁]
+        simp only [↓reduceDIte, h₁₀, h₁₁]
         cases h₉ : le value (root l (_ : 0 < o)) <;> simp
         case true =>
           unfold HeapPredicate at *
@@ -202,7 +202,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v
             exact h₄
       else if h₁₂ : le value (root l (Nat.zero_lt_of_ne_zero h₁₀)) ∧ le value (root r (Nat.zero_lt_of_ne_zero h₁₁)) then by
         unfold HeapPredicate at *
-        simp only [↓reduceDite, and_self, ↓reduceIte, true_and, h₁₀, h₁₁, h₁₂, h₂]
+        simp only [↓reduceDIte, and_self, ↓reduceIte, true_and, h₁₀, h₁₁, h₁₂, h₂]
         unfold HeapPredicate.leOrLeaf
         cases o
         · contradiction
@@ -210,7 +210,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v
           · contradiction
           · assumption
       else by
-        simp only [↓reduceDite, ↓reduceIte, h₁₀, h₁₁, h₁₂]
+        simp only [↓reduceDIte, ↓reduceIte, h₁₀, h₁₁, h₁₂]
         have h₁₃ : ¬le value (root l _) ∨ ¬le value (root r _) := (Decidable.not_and_iff_or_not (le value (root l (Nat.zero_lt_of_ne_zero h₁₀)) = true) (le value (root r (Nat.zero_lt_of_ne_zero h₁₁)) = true)).mp h₁₂
         cases h₁₄ : le (root l (_ : 0 < o)) (root r (_ : 0 < p))
         <;> simp only [Bool.false_eq_true, ↓reduceIte]
diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean
index 8038405..5733b21 100644
--- a/BinaryHeap/CompleteTree/NatLemmas.lean
+++ b/BinaryHeap/CompleteTree/NatLemmas.lean
@@ -153,14 +153,6 @@ theorem sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) : a -
   have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇
   Nat.lt_of_succ_le h₈
 
-theorem sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a - b < c - b) := by
-  apply Nat.sub_lt_of_lt_add
-  case h₂ => assumption
-  case h₁ =>
-    have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂
-    rw[Nat.sub_add_cancel h₃]
-    assumption
-
 theorem add_eq_zero {a b : Nat} :  a + b = 0 ↔ a = 0 ∧ b = 0 := by
   constructor <;> intro h₁
   case mpr =>
diff --git a/lean-toolchain b/lean-toolchain
index 6ab472f..c0eeb78 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.9.0
+leanprover/lean4:4.10