Lean 4.19

7 files changed, 151 insertions, 140 deletions

diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean
index e922a32..b57130a 100644
--- a/BinaryHeap/Aux.lean
+++ b/BinaryHeap/Aux.lean
@@ -42,7 +42,7 @@ def pushList {α : Type u} {n : Nat} {le : α → α → Bool} (heap : BinaryHea
   match l with
   | [] => heap
   | a :: as =>
-    have : n + 1 + as.length = n + (a :: as).length := by simp +arith[List.length_cons a as]
+    have : n + 1 + as.length = n + (a :: as).length := by simp +arith only [List.length_cons]
     this▸pushList (heap.push a) as
 
 private def ofForInAux [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : (h : Nat) ×' BinaryHeap α le h := Id.run do
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
index c233355..8b5c5e3 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
@@ -10,17 +10,17 @@ theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : Co
   unfold heapUpdateAt heapUpdateAtAux
   rfl
 
-theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) : heap.get index = (heap.heapUpdateAt le index val).snd := by
+private theorem heapUpdateAtReturnsElementAt_Aux {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) (h₁ : n > 0) : get index heap = (heapUpdateAtAux le index val heap h₁).snd := by
   cases index
   rename_i i isLt
   cases i
   case mk.zero =>
-    rw[←get_zero_eq_root, heapUpdatAtRootEqUpdateRoot]
+    rw[←heapUpdateAt,←get_zero_eq_root, heapUpdatAtRootEqUpdateRoot]
     exact Eq.symm $ heapUpdateRootReturnsRoot le val heap isLt
   case mk.succ j =>
-    unfold heapUpdateAt heapUpdateAtAux
+    have : 0 < n := Nat.zero_lt_of_lt isLt
+    unfold heapUpdateAtAux
     generalize hj : (⟨j + 1, isLt⟩ : Fin n) = index -- otherwise split fails...
-    generalize heapUpdateAt.proof_1 index = h₁ -- this sounds fragile... It's the n > 0 proof
     split
     case isTrue h => simp only [←hj, beq_iff_eq, Fin.mk.injEq, Nat.add_one_ne_zero] at h --contradiction
     case isFalse =>
@@ -34,17 +34,19 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
         case h₃ =>
           rw[leftLen_unfold _ _ _ _ _ _ (Nat.succ_pos _)]
           exact h₂
-        apply heapUpdateAtReturnsElementAt
+        apply heapUpdateAtReturnsElementAt_Aux
       case isFalse h₂ =>
         rw[get_right]
         case h₂ =>
           simp only [Nat.not_le] at h₂
           simp only [leftLen_unfold, gt_iff_lt, h₂]
-        apply heapUpdateAtReturnsElementAt
+        apply heapUpdateAtReturnsElementAt_Aux
 
-theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value).fst.contains value := by
-  unfold heapUpdateAt heapUpdateAtAux
-  generalize heapUpdateAt.proof_1 index = h₁
+theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) : heap.get index = (heap.heapUpdateAt le index val).snd :=
+  heapUpdateAtReturnsElementAt_Aux le val heap index _
+
+theorem heapUpdateAtContainsValue_Aux {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) (h₁ : n > 0) : (heapUpdateAtAux le index value heap h₁).fst.contains value := by
+  unfold heapUpdateAtAux
   split
   case isTrue h₂ =>
     apply heapUpdateRootContainsUpdatedElement
@@ -70,8 +72,10 @@ theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bo
         right
         rewrite[right_unfold]
       all_goals
-        apply heapUpdateAtContainsValue
-termination_by n
+        apply heapUpdateAtContainsValue_Aux
+
+theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value).fst.contains value :=
+  heapUpdateAtContainsValue_Aux le heap value index (Nat.zero_lt_of_lt index.isLt)
 
 theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (updateIndex : Fin n) (otherIndex : Fin n) (h₂ : updateIndex ≠ otherIndex) : (heap.heapUpdateAt le updateIndex val).fst.contains $ heap.get otherIndex :=
   have h₁ : n > 0 := Nat.zero_lt_of_lt otherIndex.isLt
@@ -83,8 +87,9 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
   else if h₄ : otherIndex = ⟨0, h₁⟩ then by
     subst h₄
     rw[←get_zero_eq_root]
-    unfold heapUpdateAt heapUpdateAtAux
-    generalize heapUpdateAt.proof_1 updateIndex = h₁
+    have : heapUpdateAt le updateIndex val heap = heapUpdateAtAux le updateIndex val heap h₁ := rfl
+    rw[this]
+    unfold heapUpdateAtAux
     --cannot use h₃ here already - it makes split fail. So, splitting twice it is...
     split
     case isTrue h => exact absurd (beq_iff_eq.mp h) h₃
@@ -114,8 +119,9 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
         rewrite[root_unfold]
         apply heapUpdateAtContainsValue
   else by
-    unfold heapUpdateAt heapUpdateAtAux
-    generalize heapUpdateAt.proof_1 updateIndex = h₁
+    have : heapUpdateAt le updateIndex val heap = heapUpdateAtAux le updateIndex val heap h₁ := rfl
+    rw[this]
+    unfold heapUpdateAtAux
     split
     case isTrue hx => exact absurd (beq_iff_eq.mp hx) h₃
     case isFalse =>
@@ -172,4 +178,3 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
           --rw[leftLen_unfold]
           have h₅ : index.val ≥ o + 1 := Nat.gt_of_not_le h₅
           exact (Nat.sub_ne_of_ne h₅ h₆).mp $ Fin.val_ne_iff.mpr h₂
-termination_by n
diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean
index b5d8f01..28115b0 100644
--- a/BinaryHeap/CompleteTree/HeapOperations.lean
+++ b/BinaryHeap/CompleteTree/HeapOperations.lean
@@ -20,7 +20,7 @@ private theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h�
 /--Adds a new element to a given CompleteTree.-/
 def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : CompleteTree α (o+1) :=
   match o, heap with
-  | 0, .leaf => .branch elem (.leaf) (.leaf) (Nat.le_refl 0) (by decide) (Or.inl Nat.one_isPowerOfTwo)
+  | 0, .leaf => .branch elem (.leaf) (.leaf) (Nat.le_refl 0) (by decide) (Or.inl Nat.isPowerOfTwo_one)
   | (n+m+1), .branch a left right p max_height_difference subtree_complete =>
     let (elem, a) := if le elem a then (a, elem) else (elem, a)
     -- okay, based on n and m we know if we want to add left or right.
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
index 86d2499..17a40e9 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
@@ -5,128 +5,134 @@ import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot
 
 namespace BinaryHeap.CompleteTree
 
-private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) (h₄ : total_le le) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateAt le index value heap).fst := by
-  unfold heapUpdateAt heapUpdateAtAux
-  split
-  case isTrue => exact CompleteTree.heapUpdateRootIsHeapLeRootAux le value heap h₁ h₂ h₃
-  case isFalse hi =>
-    generalize heapUpdateAt.proof_1 index = h₂
+private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) (h₄ : total_le le) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateAt le index value heap).fst :=
+  heapUpdateAtIsHeapLeRootAux_RootLeValue_Aux h₂ --factored out to avoid having to generalize an automatically named proof
+where
+  heapUpdateAtIsHeapLeRootAux_RootLeValue_Aux (h₂ : n > 0) : HeapPredicate.leOrLeaf le (heap.root h₂) (heapUpdateAtAux le index value heap h₂).fst := by
+    unfold heapUpdateAtAux
     split
-    rename_i o p v l r h₆ h₇ h₈ index h₁ h₅
-    cases h₉ : le v value <;> simp only
-    case false => rw[root_unfold] at h₃; exact absurd h₃ ((Bool.not_eq_true (le v value)).substr h₉)
-    case true =>
-      rw[root_unfold]
+    case isTrue => exact CompleteTree.heapUpdateRootIsHeapLeRootAux le value heap h₁ h₂ h₃
+    case isFalse hi =>
       split
-      <;> simp![reflexive_le, h₄]
+      rename_i o p v l r h₆ h₇ h₈ index h₁ h₅
+      cases h₉ : le v value <;> simp only
+      case false => rw[root_unfold] at h₃; exact absurd h₃ ((Bool.not_eq_true (le v value)).substr h₉)
+      case true =>
+        rw[root_unfold]
+        split
+        <;> simp![reflexive_le, h₄]
 
-private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le value (root heap h₂)) (h₄ : total_le le) (h₅ : transitive_le le) : HeapPredicate.leOrLeaf le value (heapUpdateAt le index value heap).fst := by
-  unfold heapUpdateAt heapUpdateAtAux
-  generalize heapUpdateAt.proof_1 index = h₂
-  split
-  <;> rename_i h₉
-  case isTrue =>
-    unfold heapUpdateRoot
+private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le value (root heap h₂)) (h₄ : total_le le) (h₅ : transitive_le le) : HeapPredicate.leOrLeaf le value (heapUpdateAt le index value heap).fst :=
+  heapUpdateAtIsHeapLeRootAux_ValueLeRoot_Aux h₂
+where
+  heapUpdateAtIsHeapLeRootAux_ValueLeRoot_Aux (h₂ : n > 0): HeapPredicate.leOrLeaf le value (heapUpdateAtAux le index value heap h₂).fst := by
+    unfold heapUpdateAtAux
     split
-    rename_i o p v l r h₆ h₇ h₈ h₂
-    cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, Nat.add_one_ne_zero, 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]
-    have h₁₁ : le value $ r.root (by omega) := h₅ value v (r.root _) ⟨h₃, h₁.right.right.right⟩
-    simp only [↓reduceIte, h₁₀, h₁₁, and_self, root_unfold, h₄, reflexive_le]
-  case isFalse =>
-    split
-    rename_i o p v l r h₆ h₇ h₈ index h₂ hi
-    cases le v value
-    <;> simp +ground only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢
-    <;> split
-    <;> unfold HeapPredicate.leOrLeaf
-    <;> simp only [reduceIte, root_unfold, h₃, h₄, reflexive_le]
+    <;> rename_i h₉
+    case isTrue =>
+      unfold heapUpdateRoot
+      split
+      rename_i o p v l r h₆ h₇ h₈ h₂
+      cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, Nat.add_one_ne_zero, 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]
+      have h₁₁ : le value $ r.root (by omega) := h₅ value v (r.root _) ⟨h₃, h₁.right.right.right⟩
+      simp only [↓reduceIte, h₁₀, h₁₁, and_self, root_unfold, h₄, reflexive_le]
+    case isFalse =>
+      split
+      rename_i o p v l r h₆ h₇ h₈ index h₂ hi
+      cases le v value
+      <;> simp +ground only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢
+      <;> split
+      <;> unfold HeapPredicate.leOrLeaf
+      <;> simp only [reduceIte, root_unfold, h₃, h₄, reflexive_le]
 
-theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateAt le index value).fst le := by
-  unfold heapUpdateAt heapUpdateAtAux
-  generalize heapUpdateAt.proof_1 index = h₁
-  split
-  case isTrue h₅ =>
-    exact heapUpdateRootIsHeap le value heap _ h₂ h₃ h₄
-  case isFalse h₅ =>
+theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateAt le index value).fst le :=
+  heapUpdateAtIsHeap_Aux (Fin.pos index)
+where
+  heapUpdateAtIsHeap_Aux (h₁ : n > 0) : HeapPredicate (heapUpdateAtAux le index value heap h₁).fst le := by
+    unfold heapUpdateAtAux
     split
-    rename_i o p v l r h₆ h₇ h₈ index h₁ h₅
-    cases h₁₀ : le v value <;> simp +ground -- this could probably be solved without this split, but readability...
-    <;> split
-    <;> rename_i h -- h is the same name as used in the function
-    <;> unfold HeapPredicate at h₂ ⊢
-    <;> simp only [h₂, and_true, true_and]
-    case false.isFalse =>
-      have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀)
-      have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _
-      apply And.intro <;> try apply And.intro
-      case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ v r h₂.right.left h₃ h₄
-      case right.left => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.left
-      case right.right =>
-        have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄)
-        cases h₁₂ : le v (r.root h₁₄)
-        case false =>
-          cases p
-          exact absurd (Nat.lt_succ.mp index.isLt) h
-          exact absurd h₂.right.right.right ((Bool.eq_false_iff).mp h₁₂)
-        case true =>
-          have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left (by omega) h₁₂ h₄ h₃
-          apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
-          exact h₁₀
-    case false.isTrue =>
-      have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀)
-      have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _
-      apply And.intro <;> try apply And.intro
-      case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ v l h₂.left h₃ h₄
-      case right.right => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.right
-      case right.left =>
-        have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (_)⟩ v l).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄)
-        cases h₁₂ : le v (l.root h₁₄)
-        case false =>
-          cases o
-          contradiction -- h₁₄ is False
-          exact absurd h₂.right.right.left ((Bool.eq_false_iff).mp h₁₂)
-        case true =>
-          have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ v l h₂.left (by omega) h₁₂ h₄ h₃
-          apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
-          exact h₁₀
-    case true.isFalse =>
-      have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _
-      apply And.intro
-      case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ value r h₂.right.left h₃ h₄
-      case right =>
-        have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄)
-        cases h₁₂ : le value (r.root h₁₄)
-        case false =>
-          have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) (not_le_imp_le h₄ value (r.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄
-          apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
-          cases p
-          contradiction -- h₁₄ is False
-          exact h₂.right.right.right
-        case true =>
-          have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) h₁₂ h₄ h₃
-          apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
-          exact h₁₀
-    case true.isTrue =>
-      have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _
-      apply And.intro
-      case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ value l h₂.left h₃ h₄
-      case right =>
-        have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (by omega)⟩ v l).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄)
-        cases h₁₂ : le value (l.root h₁₄)
-        case false =>
-          have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) (not_le_imp_le h₄ value (l.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄
-          apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
-          cases o
-          contradiction -- h₁₄ is False
-          exact h₂.right.right.left
-        case true =>
-          have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) h₁₂ h₄ h₃
-          apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
-          exact h₁₀
+    case isTrue h₅ =>
+      exact heapUpdateRootIsHeap le value heap _ h₂ h₃ h₄
+    case isFalse h₅ =>
+      split
+      rename_i o p v l r h₆ h₇ h₈ index h₁ h₅
+      cases h₁₀ : le v value <;> simp +ground -- this could probably be solved without this split, but readability...
+      <;> split
+      <;> rename_i h -- h is the same name as used in the function
+      <;> unfold HeapPredicate at h₂ ⊢
+      <;> simp only [h₂, and_true, true_and]
+      case false.isFalse =>
+        have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀)
+        have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _
+        apply And.intro <;> try apply And.intro
+        case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ v r h₂.right.left h₃ h₄
+        case right.left => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.left
+        case right.right =>
+          have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le :=
+            (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄)
+          cases h₁₂ : le v (r.root h₁₄)
+          case false =>
+            cases p
+            exact absurd (Nat.lt_succ.mp index.isLt) h
+            exact absurd h₂.right.right.right ((Bool.eq_false_iff).mp h₁₂)
+          case true =>
+            have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left (by omega) h₁₂ h₄ h₃
+            apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
+            exact h₁₀
+      case false.isTrue =>
+        have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀)
+        have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _
+        apply And.intro <;> try apply And.intro
+        case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ v l h₂.left h₃ h₄
+        case right.right => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.right
+        case right.left =>
+          have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (_)⟩ v l).fst le :=
+            (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄)
+          cases h₁₂ : le v (l.root h₁₄)
+          case false =>
+            cases o
+            contradiction -- h₁₄ is False
+            exact absurd h₂.right.right.left ((Bool.eq_false_iff).mp h₁₂)
+          case true =>
+            have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ v l h₂.left (by omega) h₁₂ h₄ h₃
+            apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
+            exact h₁₀
+      case true.isFalse =>
+        have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _
+        apply And.intro
+        case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ value r h₂.right.left h₃ h₄
+        case right =>
+          have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le :=
+            (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄)
+          cases h₁₂ : le value (r.root h₁₄)
+          case false =>
+            have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) (not_le_imp_le h₄ value (r.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄
+            apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
+            cases p
+            contradiction -- h₁₄ is False
+            exact h₂.right.right.right
+          case true =>
+            have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) h₁₂ h₄ h₃
+            apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
+            exact h₁₀
+      case true.isTrue =>
+        have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _
+        apply And.intro
+        case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ value l h₂.left h₃ h₄
+        case right =>
+          have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (by omega)⟩ v l).fst le :=
+            (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄)
+          cases h₁₂ : le value (l.root h₁₄)
+          case false =>
+            have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) (not_le_imp_le h₄ value (l.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄
+            apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
+            cases o
+            contradiction -- h₁₄ is False
+            exact h₂.right.right.left
+          case true =>
+            have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) h₁₂ h₄ h₃
+            apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃
+            exact h₁₀
diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean
index 56b3203..1050c17 100644
--- a/BinaryHeap/CompleteTree/NatLemmas.lean
+++ b/BinaryHeap/CompleteTree/NatLemmas.lean
@@ -40,7 +40,7 @@ private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.n
   unfold Nat.nextPowerOfTwo
   apply power_of_two_go_one_eq
   case h₁ => assumption
-  case h₂ => exact Nat.one_isPowerOfTwo
+  case h₂ => exact Nat.isPowerOfTwo_one
   case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁)
 
 private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by
diff --git a/lake-manifest.json b/lake-manifest.json
index 644812c..c1148ad 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "BinaryHeap",
diff --git a/lean-toolchain b/lean-toolchain
index 9f78e65..a0922e9 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.18.0
+leanprover/lean4:4.19.0