Remove useless proof parameter on CompleteTree.get

14 files changed, 184 insertions, 181 deletions

diff --git a/BinaryHeap.lean b/BinaryHeap.lean
index 774a3c3..e3c39af 100644
--- a/BinaryHeap.lean
+++ b/BinaryHeap.lean
@@ -41,14 +41,14 @@ def removeAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α
   ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
 
 /-- Updates the element at the given (depth-first) index and returns its previous value. O(log(n)) -/
-def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (Fin (n+1)) → α → (BinaryHeap α le (n+1) × α)
+def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le n) → (Fin n) → α → (BinaryHeap α le n × α)
 | {tree, valid, wellDefinedLe}, index, value =>
-  let result := tree.heapUpdateAt le index value $ Nat.succ_pos n
-  let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree _ valid wellDefinedLe.left wellDefinedLe.right
+  let result := tree.heapUpdateAt le index value
+  let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree valid wellDefinedLe.left wellDefinedLe.right
   ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
 
 /-- Searches for an element in the heap and returns its index. **O(n)** -/
-def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le (n+1) → (pred : α → Bool) → Option (Fin (n+1))
+def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le n → (pred : α → Bool) → Option (Fin n)
 | {tree, valid := _, wellDefinedLe := _}, pred =>
   tree.indexOf pred
 
diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean
index f103279..ee6b685 100644
--- a/BinaryHeap/CompleteTree/AdditionalOperations.lean
+++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean
@@ -50,7 +50,7 @@ def get' {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+
       match p with
       | (pp + 1) => get' ⟨j - o, h₆⟩ r
 
-def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) (_ : n > 0) : α :=
+def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) : α :=
   match n, index, heap with
   | (_+1), index, heap => heap.get' index
 
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
index 487a50f..6614210 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
@@ -41,17 +41,9 @@ private theorem if_get_eq_contains {α : Type u} {o : Nat} (tree : CompleteTree
         apply if_get_eq_contains
         done
 
-private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : o > 0) :
-  have : tree.leftLen (Nat.lt_succ_of_lt h₁) > 0 := by
-    unfold leftLen;
-    split
-    unfold length
-    rename_i hx _ _
-    simp only [Nat.add_eq, Nat.succ_eq_add_one, Nat.reduceEqDiff] at hx
-    omega
-  ∀(indexl : Fin (tree.leftLen (Nat.succ_pos o))), (tree.left _).get indexl this = element → ∃(index : Fin (o+1)), tree.get index (Nat.lt_succ_of_lt h₁) = element
+private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) :
+  ∀(indexl : Fin (tree.leftLen (Nat.succ_pos o))), (tree.left _).get indexl = element → ∃(index : Fin (o+1)), tree.get index = element
 := by
-  simp
   intro indexl
   let index : Fin (o+1) := indexl.succ.castLT (by
     simp only [Nat.succ_eq_add_one, Fin.val_succ, Nat.succ_lt_succ_iff, gt_iff_lt]
@@ -76,9 +68,9 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete
     simp only [h₅, ↓reduceDIte, Nat.add_eq]
     unfold get at prereq
     split at prereq
-    rename_i pp ii ll _ hel hei heq _
+    rename_i pp ii ll hel hei heq
     split
-    rename_i ppp lll _ _ _ _ _ _ _
+    rename_i ppp lll _ _ _ _ _ _
     have : pp = ppp := by omega
     subst pp
     simp only [gt_iff_lt, Nat.succ_eq_add_one, Nat.add_eq, heq_eq_eq, Nat.zero_lt_succ] at *
@@ -90,8 +82,8 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete
     rw[heq]
     assumption
 
-private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.rightLen (Nat.succ_pos o) > 0) :
-  ∀(indexl : Fin (tree.rightLen (Nat.succ_pos o))), (tree.right _).get indexl h₁ = element → ∃(index : Fin (o+1)), tree.get index (Nat.succ_pos o) = element
+private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) :
+  ∀(indexl : Fin (tree.rightLen (Nat.succ_pos o))), (tree.right _).get indexl = element → ∃(index : Fin (o+1)), tree.get index = element
 := by
   intro indexr
   let index : Fin (o+1) := ⟨(tree.leftLen (Nat.succ_pos o) + indexr.val + 1), by
@@ -124,9 +116,9 @@ private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : Complete
     simp only [h₅, ↓reduceDIte, Nat.add_eq]
     unfold get at prereq
     split at prereq
-    rename_i pp ii rr _ hel hei heq _
+    rename_i pp ii rr hel hei heq
     split
-    rename_i ppp rrr _ _ _ _ _ _ _ _
+    rename_i ppp rrr _ _ _ _ _ _ _
     have : pp = ppp := by rw[rightLen_unfold] at hel; exact Nat.succ.inj hel.symm
     subst pp
     simp only [gt_iff_lt, ne_eq, Nat.succ_eq_add_one, Nat.add_eq, Nat.reduceEqDiff, heq_eq_eq, Nat.zero_lt_succ] at *
@@ -161,7 +153,7 @@ private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree
       | (nn+1), l => by
         have nn_lt_o : nn < o := by have : o = nn + 1 + m := Nat.succ.inj he; omega --also for termination
         have h₃ := if_contains_get_eq l element h₂
-        have h₄ := if_contains_get_eq_auxl tree element $ Nat.zero_lt_of_lt nn_lt_o
+        have h₄ := if_contains_get_eq_auxl tree element
         simp only at h₄
         simp[get_eq_get'] at h₃ ⊢
         apply h₃.elim
@@ -179,12 +171,7 @@ private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree
       | (mm+1), r => by
         have mm_lt_o : mm < o := by have : o = n + (mm + 1) := Nat.succ.inj he; omega --termination
         have h₃ := if_contains_get_eq r element h₂
-        have : tree.rightLen (Nat.succ_pos o) > 0 := by
-          have := heqSameRightLen (he) (Nat.succ_pos o) heq
-          simp[rightLen_unfold] at this
-          rw[this]
-          exact Nat.succ_pos mm
-        have h₄ := if_contains_get_eq_auxr tree element this
+        have h₄ := if_contains_get_eq_auxr tree element
         simp[get_eq_get'] at h₃ ⊢
         apply h₃.elim
         match o, tree with
@@ -206,6 +193,6 @@ theorem contains_iff_index_exists' {α : Type u} {o : Nat} (tree : CompleteTree
   case mp =>
     exact if_contains_get_eq tree element
 
-theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : n > 0): tree.contains element ↔ ∃ (index : Fin n), tree.get index h₁ = element :=
+theorem contains_iff_index_exists {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (_ : n > 0): tree.contains element ↔ ∃ (index : Fin n), tree.get index = element :=
   match n, tree with
   | _+1, tree => contains_iff_index_exists' tree element
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean
index 83984a0..902afc4 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean
@@ -19,46 +19,53 @@ private theorem Option.bind_some_eq_map {α β : Type u} (f : α → β) (a : Op
   case none => rfl
   case some => rfl
 
-private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0) (pred : α → Bool) (currentIndex : Nat) : (CompleteTree.Internal.indexOfAux tree pred currentIndex).isNone → ∀(index : Fin n), ¬pred (tree.get index h₁) := by
-  intro h₂
-  intro index
-  simp only [Option.isNone_iff_eq_none] at h₂
-  simp only [Bool.not_eq_true]
-  unfold CompleteTree.Internal.indexOfAux at h₂
-  split at h₂ ; contradiction
-  rename_i o p v l r p_le_o max_height_difference subtree_complete
-  split at h₂; contradiction
-  unfold HOrElse.hOrElse instHOrElseOfOrElse at h₂
-  unfold OrElse.orElse Option.instOrElse at h₂
-  simp only [Nat.add_zero, Nat.reduceAdd, Option.pure_def, Option.bind_eq_bind] at h₂
-  have h₂₂ := Option.orElse_result_none_both_none h₂
-  repeat rw[Option.bind_some_eq_map] at h₂₂
-  simp only [Option.map_eq_none'] at h₂₂
-  if h₃ : index = ⟨0,h₁⟩ then
-    subst index
-    rw[←get_zero_eq_root, root_unfold]
-    rename_i solution
-    simp only [Bool.not_eq_true] at solution
-    exact solution
-  else
-    have h₃₂ : index > ⟨0,h₁⟩ := Fin.pos_iff_ne_zero.mpr h₃
-    if h₄ : index ≤ o then
-      rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) _ h₁ h₃₂ h₄]
-      rw[left_unfold]
-      have : o > 0 := by omega
-      have := indexOfNoneImpPredFalseAux l this pred (currentIndex + 1)
-      simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this
-      exact this h₂₂.left _
+private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : CompleteTree α n) (pred : α → Bool) (currentIndex : Nat) : (CompleteTree.Internal.indexOfAux tree pred currentIndex).isNone → ∀(index : Fin n), ¬pred (tree.get index) := by
+  if h₁ : n > 0 then
+    intro h₂
+    intro index
+    simp only [Option.isNone_iff_eq_none] at h₂
+    simp only [Bool.not_eq_true]
+    unfold CompleteTree.Internal.indexOfAux at h₂
+    split at h₂ ; contradiction
+    rename_i o p v l r p_le_o max_height_difference subtree_complete
+    split at h₂; contradiction
+    unfold HOrElse.hOrElse instHOrElseOfOrElse at h₂
+    unfold OrElse.orElse Option.instOrElse at h₂
+    simp only [Nat.add_zero, Nat.reduceAdd, Option.pure_def, Option.bind_eq_bind] at h₂
+    have h₂₂ := Option.orElse_result_none_both_none h₂
+    repeat rw[Option.bind_some_eq_map] at h₂₂
+    simp only [Option.map_eq_none'] at h₂₂
+    if h₃ : index = ⟨0,h₁⟩ then
+      subst index
+      rw[←get_zero_eq_root, root_unfold]
+      rename_i solution
+      simp only [Bool.not_eq_true] at solution
+      exact solution
     else
-      have h₄₂ : index > o := Nat.gt_of_not_le h₄
-      rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) _ (Nat.succ_pos _) h₄₂]
-      rw[right_unfold]
-      -- if you are wondering: this is needed to make omega work below.
-      have : (o.add p).succ = p + (o + 1) := (Nat.add_assoc p o 1).substr $ (Nat.add_comm o p).subst (motive := λx ↦ (o+p)+1 = x + 1) rfl
-      have : p > 0 := by omega
-      have := indexOfNoneImpPredFalseAux r this pred (currentIndex + o + 1)
-      simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this
-      exact this h₂₂.right _
+      have h₃₂ : index > ⟨0,h₁⟩ := Fin.pos_iff_ne_zero.mpr h₃
+      if h₄ : index ≤ o then
+        rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) _ h₁ h₃₂ h₄]
+        rw[left_unfold]
+        have := indexOfNoneImpPredFalseAux l pred (currentIndex + 1)
+        simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this
+        exact this h₂₂.left _
+      else
+        have h₄₂ : index > o := Nat.gt_of_not_le h₄
+        rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) _ (Nat.succ_pos _) h₄₂]
+        rw[right_unfold]
+        have := indexOfNoneImpPredFalseAux r pred (currentIndex + o + 1)
+        simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this
+        exact this h₂₂.right _
+  else
+    simp at h₁
+    intro h₂
+    intro hx
+    subst h₁
+    cases hx
+    contradiction
+
+theorem indexOfNoneImpPredFalse {α : Type u} {n : Nat} (tree : CompleteTree α n) (pred : α → Bool) : (tree.indexOf pred).isNone → ∀(index : Fin n), ¬pred (tree.get index) :=
+  indexOfNoneImpPredFalseAux tree pred 0
 
-theorem indexOfNoneImpPredFalse {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0) (pred : α → Bool) : (tree.indexOf pred).isNone → ∀(index : Fin n), ¬pred (tree.get index h₁) :=
-  indexOfNoneImpPredFalseAux tree h₁ pred 0
+theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n) (pred : α → Bool) : (h₁ : (tree.indexOf pred).isSome) → pred (tree.get ((tree.indexOf pred).get h₁)) := by
+  sorry
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index b8cd934..f872836 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -3,9 +3,9 @@ import BinaryHeap.CompleteTree.Lemmas
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
-theorem get_eq_get' {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (index : Fin (n+1)) : tree.get' index = tree.get index (Nat.succ_pos n) := rfl
+theorem get_eq_get' {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (index : Fin (n+1)) : tree.get' index = tree.get index := rfl
 
-theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ h₁ := by
+theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ := by
   unfold get
   match n with
   | nn+1 =>
@@ -29,14 +29,13 @@ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fi
     have : p+1+o = (o.add p).succ := by simp_arith
     rw[this]
     assumption
-  have h₄ : tree.rightLen h₁ > 0 := Nat.zero_lt_of_lt h₃
-  tree.get index h₁ = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩ h₄
+  tree.get index = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩
 :=
   match n, tree with
   | (o+p+1), .branch v l r _ _ _ => by
     simp[right_unfold, leftLen_unfold]
     rw[leftLen_unfold] at h₂
-    generalize hnew : get ⟨↑index - o - 1, _⟩ r _ = new
+    generalize hnew : get ⟨↑index - o - 1, _⟩ r = new
     unfold get get'
     split
     case h_1 =>
@@ -73,19 +72,18 @@ theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r
     have : m + 1 + n = n + m + 1 := by simp_arith
     rw[this]
     assumption
-  (branch v l r m_le_n max_height_diff subtree_complete).get index (Nat.succ_pos _) = r.get ⟨index.val - n - 1, h₂⟩  (Nat.zero_lt_of_lt h₂)
+  (branch v l r m_le_n max_height_diff subtree_complete).get index = r.get ⟨index.val - n - 1, h₂⟩
 :=
   get_right (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁
 
 theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₁ : n > 0) (h₂ : index > ⟨0, h₁⟩) (h₃ : index ≤ tree.leftLen h₁) :
   have h₃ : ↑index - 1 < tree.leftLen h₁ := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₂) h₃
-  have h₄ : tree.leftLen h₁ > 0 := Nat.zero_lt_of_lt h₃
-  tree.get index h₁ = (tree.left h₁).get ⟨index.val - 1, h₃⟩ h₄
+  tree.get index = (tree.left h₁).get ⟨index.val - 1, h₃⟩
 :=
   match n, tree with
   | (o+p+1), .branch v l r _ _ _ => by
     simp[left_unfold]
-    generalize hnew : get ⟨↑index - 1, _⟩ l _ = new
+    generalize hnew : get ⟨↑index - 1, _⟩ l = new
     unfold get get'
     split
     case h_1 => contradiction
@@ -106,6 +104,6 @@ theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin
 
 theorem get_left' {α : 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 > ⟨0, Nat.succ_pos _⟩) (h₂ : index ≤ n) :
   have h₃ : ↑index - 1 < n := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₁) h₂
-  (branch v l r m_le_n max_height_diff subtree_complete).get index (Nat.succ_pos _) = l.get ⟨index.val - 1, h₃⟩  (Nat.zero_lt_of_lt h₃)
+  (branch v l r m_le_n max_height_diff subtree_complete).get index = l.get ⟨index.val - 1, h₃⟩
 :=
   get_left (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁ h₂
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
index fb5b81b..807bdcb 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
@@ -29,7 +29,7 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)
   This is not a rigorous proof that the rest of the tree remained unchanged, as (1 (1 (1 1)) (2)).heapPop = (1 (2 (2 _)) (2)) would pass it too...
   Imho it is still a good indication that there are no obvious bugs.
   -/
-theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index (Nat.succ_pos _) := by
+theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index := by
   unfold heapPop
   split <;> simp
   case isFalse h₃ => omega --contradiction. if n == 0 then index cannot be ≠ 0
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
index 66035a1..ea2b5a7 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
@@ -46,13 +46,15 @@ theorem heapPushContainsValue {α : Type u} {n : Nat} (le : α → α → Bool)
       rw[left_unfold]
       exact heapPushContainsValue le l val
 
-theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Bool) (heap : CompleteTree α n) (val : α) (index : Fin n) (h₁ : n > 0) : (heap.heapPush le val).contains (heap.get index h₁) := by
+theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Bool) (heap : CompleteTree α n) (val : α) (index : Fin n) : (heap.heapPush le val).contains (heap.get index) := by
   unfold heapPush
   split
   case h_1 =>
+    have := index.isLt
     contradiction
   case h_2 =>
     rename_i o p v l r p_le_o max_height_difference subtree_complete
+    have h₁ : o+p+1 > 0 := Nat.succ_pos _
     if h₂ : index = ⟨0, h₁⟩ then
       subst h₂
       cases le val v
@@ -95,7 +97,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo
             have : index.val - 1 < o := Nat.sub_one_lt_of_le h₂₂ h₃
             exists ⟨index.val - 1, this⟩
           case isFalse =>
-            exact heapPushRetainsHeapValues le l _ ⟨index.val - 1, _⟩ _
+            exact heapPushRetainsHeapValues le l _ ⟨index.val - 1, _⟩
         else
           split
           case' isFalse => rw[←containsSeesThroughCast]
@@ -107,7 +109,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo
             rw[right_unfold]
             simp only [Nat.succ_eq_add_one, leftLen_unfold]
           case isTrue =>
-            exact heapPushRetainsHeapValues le r _ ⟨index.val - o - 1, _⟩ _
+            exact heapPushRetainsHeapValues le r _ ⟨index.val - o - 1, _⟩
           case isFalse =>
             have : (o.add p).succ = p + (o + 1) := (Nat.add_assoc p o 1).substr $ (Nat.add_comm o p).subst (motive := λx ↦ (o+p)+1 = x + 1) rfl
             have : p > 0 := by omega
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
index 195e24d..a8a551f 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
@@ -21,12 +21,12 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
         simp only[h₂, h₃, ↓reduceDIte]
         have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt heap index $ Nat.lt_of_le_of_ne h₃ (Fin.val_ne_iff.mpr (Ne.symm h₂))
         rewrite[get_eq_get', ←h₄]
-        exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ _
+        exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _
       else
         simp only[h₂, h₃, ↓reduceDIte]
         have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt heap index (Nat.gt_of_not_le h₃)
         rewrite[get_eq_get', ←h₄]
-        exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _ _
+        exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _
 
 theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).fst.contains (heap.get' otherIndex) := by
   unfold heapRemoveAt
@@ -62,7 +62,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo
             subst h₉
             subst h₈
             rw[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex]
-            exact heapUpdateAtContainsValue _ _ _ _ _
+            exact heapUpdateAtContainsValue _ _ _ _
       else
         simp only [h₃, h₄, ↓reduceDIte]
         have h₅ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap otherIndex
@@ -87,4 +87,4 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo
             subst h₉
             subst h₈
             rw[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex]
-            exact heapUpdateAtContainsValue _ _ _ _ _
+            exact heapUpdateAtContainsValue _ _ _ _
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index b852995..694a0ee 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -208,11 +208,11 @@ private theorem Fin.ne_zero_of_gt {n : Nat} {i j : Fin (n+1)} (h₁ : i > j) : i
   have : 0 ≤ j := Fin.zero_le _
   by omega
 
-private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat} (index : Fin (((o + 1).add p + 1))) (h₁ : o + 1 + p = o + p + 1) (tree : CompleteTree α (o+p+1)) (h₂ : o + 1 + p > 0) (h₃ : (h₁ ▸ tree).rightLen h₂ > 0) (h₄ : ↑index - 1 - q - 1 < (h₁ ▸ tree).rightLen h₂) (h₅ : o + p + 1 > 0) (h₆ : tree.rightLen h₅ > 0) (h₇ : ↑index - (q + 1) - 1 < tree.rightLen h₅)
+private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat} (index : Fin (((o + 1).add p + 1))) (h₁ : o + 1 + p = o + p + 1) (tree : CompleteTree α (o+p+1)) (h₂ : o + 1 + p > 0) (h₄ : ↑index - 1 - q - 1 < (h₁ ▸ tree).rightLen h₂) (h₅ : o + p + 1 > 0) (h₇ : ↑index - (q + 1) - 1 < tree.rightLen h₅)
 :
   get ⟨↑index - 1 - q - 1, h₄⟩
-    ((h₁ ▸ tree).right h₂) h₃ =
-  get ⟨↑index - (q + 1) - 1, h₇⟩ (tree.right h₅) h₆
+    ((h₁ ▸ tree).right h₂) =
+  get ⟨↑index - (q + 1) - 1, h₇⟩ (tree.right h₅)
 := by
   induction p generalizing o
   case zero =>
@@ -225,9 +225,9 @@ private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat
     have hp₄ : (o + 1 + 1 + pp) = o + 1 + (pp + 1) := (Nat.add_comm_right (o+1) 1 pp).substr $ Nat.add_assoc (o+1) pp 1
     rw[hp₃, hp₄] at hp₂
     have : o + 1 + (pp + 1) + 1 = o + 1 + 1 + pp + 1 := Nat.add_comm_right (o + 1) (pp + 1) 1
-    exact hp₂ (index.cast this) h₁ tree h₂ h₃ h₄ h₅ h₆ h₇
+    exact hp₂ (index.cast this) h₁ tree h₂ h₄ h₅ h₇
 
-private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {o p : Nat} (index : Fin (o + 1 + p)) (tree : CompleteTree α (o + p + 1)) (h₁ :  o + p + 1 = o + 1 + p) (h₂ : o + 1 + p > 0) (h₃ : o + p + 1 > 0) (h₄ : index.val < o + p + 1) : get index (h₁▸tree) h₂ = get ⟨index.val,h₄⟩ tree h₃ := by
+private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {o p : Nat} (index : Fin (o + 1 + p)) (tree : CompleteTree α (o + p + 1)) (h₁ :  o + p + 1 = o + 1 + p) (h₄ : index.val < o + p + 1) : get index (h₁▸tree) = get ⟨index.val,h₄⟩ tree := by
   induction p generalizing o
   case zero =>
     simp
@@ -236,11 +236,10 @@ private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {o p : Nat}
     have hp₃ : (o + 1 + pp + 1) = o + (pp + 1) + 1 := Nat.add_comm_right o 1 (pp + 1)
     have hp₄ : (o + 1 + 1 + pp) = o + 1 + (pp + 1) := (Nat.add_comm_right (o+1) 1 pp).substr $ Nat.add_assoc (o+1) pp 1
     rw[hp₃, hp₄] at hp₂
-    exact hp₂ index tree h₁ h₂ h₃ h₄
+    exact hp₂ index tree h₁ h₄
 
 protected theorem heapRemoveLastWithIndexRelationGt {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) (h₁ : index > (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd) :
-  have : 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 index.isLt)
-  (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get (index.pred $ Fin.ne_zero_of_gt h₁) this = heap.get index (Nat.succ_pos _)
+  (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get (index.pred $ Fin.ne_zero_of_gt h₁) = heap.get index
 := by
 have h₂ : 0 ≠ n := Ne.symm $ Nat.ne_zero_iff_zero_lt.mpr $ Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ index.isLt)
 revert h₁
@@ -268,6 +267,7 @@ if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then
         rewrite[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
         rewrite[leftLen_unfold]
         assumption
+        omega
       simp only [Nat.add_eq, ne_eq, Fin.zero_eta, Nat.succ_eq_add_one, Nat.pred_eq_sub_one,
         Fin.coe_pred, Fin.isValue, ← lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
       simp only[leftLen_unfold]
@@ -278,14 +278,13 @@ if h₃ : p < o ∧ (p + 1).nextPowerOfTwo = p + 1 then
       -- get goes into the left branch
       have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁
       rewrite[heapRemoveLastWithIndexRelationGt_Aux2]
-      case h₃ => exact Nat.succ_pos _
       case h₄ => exact
         Nat.le_of_not_gt h₄
         |> (Nat.succ_pred (Fin.val_ne_of_ne h₅)).substr
         |> Nat.succ_le.mp
         |> Nat.lt_add_right p
         |> (Nat.add_comm_right oo 1 p).subst
-      generalize hold :  get index (branch v l r _ _ _) _ = old
+      generalize hold :  get index (branch v l r _ _ _) = old
       have h₆ : index.pred h₅ ≤ oo := Nat.pred_le_iff_le_succ.mpr $ Nat.le_of_not_gt h₄
       have h₇ : ↑index - 1 ≤ oo := (Fin.coe_pred index h₅).subst (motive := λx↦x ≤ oo) h₆
       have h₈ : ↑index ≤ oo + 1 := Nat.le_succ_of_pred_le h₇
@@ -309,7 +308,7 @@ else
     subst o
     contradiction
   case succ pp _ _ _ _ =>
-    generalize hold : get index (branch v l r _ _ _) _ = oldValue
+    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]
@@ -339,16 +338,15 @@ else
     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)
   have : index.val < n := Nat.lt_of_lt_of_le h₁ $ Nat.lt_succ.mp (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt
-  (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get ⟨index.val, this⟩ hn = heap.get index (Nat.succ_pos _)
+  (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get ⟨index.val, this⟩ = heap.get index
 :=
   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)
   have hi : index.val < n := Nat.lt_of_lt_of_le h₁ $ Nat.lt_succ.mp (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt
   if h₂ : index = 0 then by
     subst index
     simp only [Fin.val_zero]
-    have := Fin.zero_eta.subst (motive := λx ↦ heap.root _ = get x heap _) $ get_zero_eq_root heap (Nat.succ_pos _)
+    have := Fin.zero_eta.subst (motive := λx ↦ heap.root _ = get x heap) $ get_zero_eq_root heap (Nat.succ_pos _)
     rewrite[←this]
     have :=  get_zero_eq_root (Internal.heapRemoveLastWithIndex heap).fst hn
     rewrite[←this]
@@ -385,7 +383,6 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea
         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₅
@@ -436,11 +433,11 @@ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap
   if h₁ : index > oldIndex then
     have : oldIndex ≥ 0 := Fin.zero_le oldIndex
     have : index > 0 := by omega
-    result.get (index.pred $ Fin.ne_of_gt this) (by omega) = heap.get index (by omega)
+    result.get (index.pred $ Fin.ne_of_gt this) = heap.get index
   else if h₂ : index < oldIndex then
-    result.get (index.castLT (by omega)) (by omega) = heap.get index (by omega)
+    result.get (index.castLT (by omega)) = heap.get index
   else
-    removedElement = heap.get index (Nat.succ_pos _)
+    removedElement = heap.get index
 := by
   simp
   split
@@ -473,13 +470,12 @@ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap
   -/
 protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) :
   let (newHeap, _, removedIndex) := Internal.heapRemoveLastWithIndex heap
-  (h₁ : index ≠ removedIndex) → newHeap.contains (heap.get index (Nat.succ_pos n))
+  (h₁ : index ≠ removedIndex) → newHeap.contains (heap.get index)
 := by
   simp only [ne_eq]
   intro h₁
   have h₂ : n > 0 := by omega
-  rw[contains_iff_index_exists]
-  case h₁ => exact h₂
+  rw[contains_iff_index_exists _ _ h₂]
   have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap index
   simp at h₃
   split at h₃
@@ -498,7 +494,7 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n
   -/
 protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) :
   let (newHeap, removedElement, _) := Internal.heapRemoveLastWithIndex heap
-  newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n)
+  newHeap.contains (heap.get index) ∨ removedElement = heap.get index
 :=
   let removedIndex := (Internal.heapRemoveLastWithIndex heap).snd.snd
   if h₁ : index ≠ removedIndex then
@@ -517,7 +513,7 @@ protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Ty
   -/
 protected theorem heapRemoveLastEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) :
   let (newHeap, removedElement) := Internal.heapRemoveLast heap
-  newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n)
+  newHeap.contains (heap.get index) ∨ removedElement = heap.get index
 := by
   have h₁ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexEitherContainsOrReturnsElement heap index
   simp at h₁ ⊢
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
index 7dbe23d..be82a57 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
@@ -5,22 +5,23 @@ import BinaryHeap.CompleteTree.AdditionalProofs.Get
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
-theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) (h₁ : n > 0) : heap.get index h₁ =  (heap.heapUpdateAt le index val h₁).snd := by
+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
   cases index
   rename_i i isLt
   cases i
   case mk.zero =>
-    unfold get get' heapUpdateAt
+    unfold get get'
     split
     split
     case h_2 hx =>
       have hx := Fin.val_eq_of_eq hx
       contradiction
-    case h_1 v l r h₂ h₃ h₄ _ _ _=>
+    case h_1 v l r h₂ h₃ h₄ _ _=>
       exact Eq.symm $ heapUpdateRootReturnsRoot le val (.branch v l r h₂ h₃ h₄) (Nat.succ_pos _)
   case mk.succ j =>
-    unfold heapUpdateAt
+    unfold heapUpdateAt 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 =>
@@ -32,23 +33,25 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
         rw[get_left]
         case h₂ => exact Nat.succ_pos j
         case h₃ =>
-          rw[leftLen_unfold]
+          rw[leftLen_unfold _ _ _ _ _ _ (Nat.succ_pos _)]
           exact h₂
         apply heapUpdateAtReturnsElementAt
       case isFalse h₂ =>
-        rw[get_right]
+        rw[get_right _ _]
+        case h₁ => exact Nat.succ_pos _
         case h₂ =>
           simp only [Nat.not_le] at h₂
           simp only [leftLen_unfold, gt_iff_lt, h₂]
         apply heapUpdateAtReturnsElementAt
 
-theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot le := by
+theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot h₁ le := by
   funext
-  unfold heapUpdateAt
+  unfold heapUpdateAt heapUpdateAtAux
   rfl
 
-theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (h₁ : n > 0) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value h₁).fst.contains value := by
-  unfold heapUpdateAt
+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₁
   split
   case isTrue h₂ =>
     apply heapUpdateRootContainsUpdatedElement
@@ -77,16 +80,18 @@ theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bo
         apply heapUpdateAtContainsValue
 termination_by n
 
-theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (updateIndex : Fin n) (otherIndex : Fin n) (h₁ : n > 0) (h₂ : updateIndex ≠ otherIndex) : (heap.heapUpdateAt le updateIndex val h₁).fst.contains $ heap.get otherIndex h₁ :=
+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
   if h₃ : updateIndex = ⟨0, h₁⟩ then
     have h₄ : otherIndex ≠ ⟨0, h₁⟩ := h₃.subst h₂.symm
     heapUpdateRootOnlyUpdatesRoot le heap h₁ otherIndex h₄ val
-    |> heapUpdatAtRootEqUpdateRoot.substr (p := λx↦(x val heap h₁).fst.contains (heap.get otherIndex h₁))
-    |> h₃.substr (p := λx↦((heap.heapUpdateAt le x val h₁).fst.contains $ heap.get otherIndex h₁))
+    |> heapUpdatAtRootEqUpdateRoot.substr (p := λx↦(x val heap).fst.contains (heap.get otherIndex))
+    |> h₃.substr (p := λx↦((heap.heapUpdateAt le x val).fst.contains $ heap.get otherIndex))
   else if h₄ : otherIndex = ⟨0, h₁⟩ then by
     subst h₄
     rw[←get_zero_eq_root]
-    unfold heapUpdateAt
+    unfold heapUpdateAt heapUpdateAtAux
+    generalize heapUpdateAt.proof_1 updateIndex = h₁
     --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₃
@@ -116,7 +121,8 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
         rewrite[root_unfold]
         apply heapUpdateAtContainsValue
   else by
-    unfold heapUpdateAt
+    unfold heapUpdateAt heapUpdateAtAux
+    generalize heapUpdateAt.proof_1 updateIndex = h₁
     split
     case isTrue hx => exact absurd ((beq_iff_eq _ _).mp hx) h₃
     case isFalse =>
@@ -152,6 +158,9 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
           rw[contains_iff_index_exists]
           generalize (⟨↑otherIndex - o - 1, _⟩ : Fin _) = solution -- Allows to skip the annoying proof that Lean already has...
           exists solution --also solves h.h₁ goal? Okay, I don't know why, but I won't complain.
+          rw[rightLen_unfold]
+          have : (o.add p).succ = p + (o + 1) := (Nat.add_assoc p o 1).substr $ (Nat.add_comm o p).subst (motive := λx ↦ (o+p)+1 = x + 1) rfl
+          omega
       case false.isFalse h₅ | true.isFalse h₅ =>
         if h₆ : otherIndex ≤ o then
           have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆]
@@ -162,6 +171,8 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
           rw[contains_iff_index_exists]
           generalize (⟨↑otherIndex - 1, _⟩ : Fin _) = solution
           exists solution
+          rw[leftLen_unfold]
+          omega
         else
           have h₆ : otherIndex > (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by rw[leftLen_unfold]; exact Nat.gt_of_not_le h₆
           rw[get_right _ _ (Nat.succ_pos _) h₆]
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index 9912bf3..cd765bb 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -16,8 +16,8 @@ abbrev heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Boo
   This is not a rigorous proof that the rest of the tree remained unchanged. See comment on heapPopOnlyRemovesRoot.
   Imho it is still a good indication that there are no obvious bugs.
   -/
-theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot le value h₁).fst.contains $ tree.get index h₁ := by
-  generalize h₃ : (get index tree h₁) = oldVal
+theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot h₁ le value).fst.contains $ tree.get index := by
+  generalize h₃ : (get index tree) = oldVal
   unfold get at h₃
   unfold heapUpdateRoot
   split
@@ -163,7 +163,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
                 simp only [Nat.add_one_ne_zero, not_false_eq_true]
 termination_by n
 
-theorem heapUpdateRootContainsUpdatedElement {α : Type u} {n : Nat} (tree : CompleteTree α n) (le : α → α → Bool) (value : α) (h₁ : n > 0): (tree.heapUpdateRoot le value h₁).fst.contains value := by
+theorem heapUpdateRootContainsUpdatedElement {α : Type u} {n : Nat} (tree : CompleteTree α n) (le : α → α → Bool) (value : α) (h₁ : n > 0): (tree.heapUpdateRoot h₁ le value).fst.contains value := by
   unfold heapUpdateRoot
   split
   rename_i o p v l r _ _ _ h₁
diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean
index f3ff41c..aa2eb2c 100644
--- a/BinaryHeap/CompleteTree/HeapOperations.lean
+++ b/BinaryHeap/CompleteTree/HeapOperations.lean
@@ -200,7 +200,7 @@ protected def Internal.heapRemoveLastWithIndex {α : Type u} {o : Nat} (heap : C
 /--
   Helper for heapUpdateAt. Makes proofing heap predicate work in Lean 4.9
   -/
-def heapUpdateRoot  {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (_ : n > 0) : CompleteTree α n × α :=
+def heapUpdateRoot  {α : Type u} {n : Nat} (_ : n > 0) (le : α → α → Bool) (value : α) (heap : CompleteTree α n) : CompleteTree α n × α :=
 match n, heap with
   | (o+p+1), .branch v l r h₃ h₄ h₅ =>
     if h₆ : o = 0 then
@@ -216,7 +216,7 @@ match n, heap with
           -- We would not need to recurse further, because we know o = 1.
           -- However, that would introduce type casts, what makes proving harder...
           -- have h₉: o = 1 := Nat.le_antisymm (by simp_arith[h₈] at h₄; exact h₄) (Nat.succ_le_of_lt h₇)
-          let ln := heapUpdateRoot le value l h₇
+          let ln := heapUpdateRoot h₇ le value l
           (.branch ln.snd ln.fst r h₃ h₄ h₅, v)
       else
         have h₉ : p > 0 := Nat.zero_lt_of_ne_zero h₈
@@ -224,23 +224,18 @@ match n, heap with
         if le value lr ∧ le value rr then
           (.branch value l r h₃ h₄ h₅, v)
         else if le lr rr then -- value is gt either left or right root. Move it down accordingly
-          let ln := heapUpdateRoot le value l h₇
+          let ln := heapUpdateRoot h₇ le value l
           (.branch ln.snd ln.fst r h₃ h₄ h₅, v)
         else
-          let rn := heapUpdateRoot le value r h₉
+          let rn := heapUpdateRoot h₉ le value r
           (.branch rn.snd l rn.fst h₃ h₄ h₅, v)
 
 ----------------------------------------------------------------------------------------------
 -- heapRemoveAt
 
-/--
-  Helper for heapRemoveAt.
-  Removes the element at index, and instead inserts the given value.
-  Returns the element at index, and the resulting tree.
-  -/
-def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : CompleteTree α n × α :=
+def heapUpdateAtAux {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : CompleteTree α n × α :=
   if h₂ : index == ⟨0,h₁⟩ then
-    heapUpdateRoot le value heap h₁
+    heapUpdateRoot h₁ le value heap
   else
     match n, heap with
     | (o+p+1), .branch v l r h₃ h₄ h₅ =>
@@ -249,7 +244,7 @@ def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin
         have h₇ : Nat.pred index.val < o := Nat.lt_of_lt_of_le (Nat.pred_lt $ Fin.val_ne_of_ne (ne_of_beq_false $ Bool.of_not_eq_true h₂)) h₆
         let index_in_left : Fin o := ⟨index.val.pred, h₇⟩
         have h₈ : 0 < o := Nat.zero_lt_of_lt h₇
-        let result := heapUpdateAt le index_in_left value l h₈
+        let result := heapUpdateAtAux le index_in_left value l h₈
         (.branch v result.fst r h₃ h₄ h₅, result.snd)
       else
         have h₇ : index.val - (o + 1) < p :=
@@ -262,16 +257,24 @@ def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin
           Nat.sub_lt_of_lt_add h₈ $ (Nat.not_le_eq index.val o).mp h₆
         let index_in_right : Fin p := ⟨index.val - o - 1, h₇⟩
         have h₈ : 0 < p := Nat.zero_lt_of_lt h₇
-        let result := heapUpdateAt le index_in_right value r h₈
+        let result := heapUpdateAtAux le index_in_right value r h₈
         (.branch v l result.fst h₃ h₄ h₅, result.snd)
 
+/--
+  Helper for heapRemoveAt.
+  Removes the element at index, and instead inserts the given value.
+  Returns the element at index, and the resulting tree.
+  -/
+def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) : CompleteTree α n × α :=
+  heapUpdateAtAux le index value heap (Nat.zero_lt_of_lt index.isLt)
+
 ----------------------------------------------------------------------------------------------
 -- heapPop
 
 def heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α :=
   let l := Internal.heapRemoveLast heap
   if p : n > 0 then
-    heapUpdateRoot le l.snd l.fst p
+    heapUpdateRoot p le l.snd l.fst
   else
     l
 
@@ -288,17 +291,13 @@ def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin
     heapPop le heap
   else
     let (remaining_tree, removed_element, removed_index) := Internal.heapRemoveLastWithIndex heap
-    if p : index = removed_index then
+    if index = removed_index then
       (remaining_tree, removed_element)
     else
-      have n_gt_zero : n > 0 := by
-        cases n
-        case succ nn => exact Nat.zero_lt_succ nn
-        case zero => omega
       if index_lt_lastIndex : index ≥ removed_index then
         let index := index.pred index_ne_zero
-        heapUpdateAt le index removed_element remaining_tree n_gt_zero
+        heapUpdateAt le index removed_element remaining_tree
       else
         let h₁ : index < n := by omega
         let index : Fin n := ⟨index, h₁⟩
-        heapUpdateAt le index removed_element remaining_tree n_gt_zero
+        heapUpdateAt le index removed_element remaining_tree
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
index 295fcbd..32e6fb9 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
@@ -5,11 +5,12 @@ 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 h₂).fst := by
-  unfold heapUpdateAt
+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₂
     split
     rename_i o p v l r h₆ h₇ h₈ index h₁ h₅
     cases h₉ : le v value <;> simp (config := { ground := true }) only
@@ -19,8 +20,9 @@ private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat}
       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 h₂).fst := by
-  unfold heapUpdateAt
+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 =>
@@ -42,11 +44,12 @@ private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat}
     <;> unfold HeapPredicate.leOrLeaf
     <;> simp only [root_unfold, h₃, h₄, reflexive_le]
 
-theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateAt le index value h₁).fst le := by
-  unfold heapUpdateAt
+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₃ 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₅
@@ -59,11 +62,11 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in
       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₁₄ h₂.right.left h₃ h₄
+      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 h₁₄).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r _ h₂.right.left h₃ h₄)
+        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
@@ -77,11 +80,11 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in
       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₁₄ h₂.left h₃ h₄
+      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 h₁₄).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l _ h₂.left h₃ h₄)
+        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
@@ -94,10 +97,10 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in
     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₁₄ h₂.right.left h₃ h₄
+      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 (h₁₄)).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r _ h₂.right.left h₃ h₄)
+        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₄
@@ -112,10 +115,10 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in
     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₁₄ h₂.left h₃ h₄
+      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 h₁₄).fst le :=
-          (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l _ h₂.left h₃ h₄)
+        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₄
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
index e930a30..c6b421f 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
@@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.Lemmas
 
 namespace BinaryHeap.CompleteTree
 
-theorem heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : (heap.heapUpdateRoot le value h₁).snd = heap.root h₁ := by
+theorem heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) : (heap.heapUpdateRoot h₁ le value).snd = heap.root h₁ := by
   unfold heapUpdateRoot
   split
   rename_i o p v l r h₃ h₄ h₅ h₁
@@ -37,7 +37,7 @@ private theorem heapUpdateRootPossibleRootValuesAuxR {α : Type u} (heap : Compl
     case zero => simp_arith at h₁; simp at h₃; exact absurd h₁ (Nat.not_le_of_gt h₃)
     case succ q => exact Nat.zero_lt_succ q
 
-private theorem heapUpdateRootPossibleRootValues1 {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n = 1) : (heap.heapUpdateRoot le value (h₁.substr (Nat.lt_succ_self 0))).fst.root (h₁.substr (Nat.lt_succ_self 0)) = value := by
+private theorem heapUpdateRootPossibleRootValues1 {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n = 1) : (heap.heapUpdateRoot (h₁.substr (p := λx ↦ 0<x) (Nat.lt_succ_self 0)) le value).fst.root (h₁.substr (Nat.lt_succ_self 0)) = value := by
   unfold heapUpdateRoot
   generalize (h₁.substr (Nat.lt_succ_self 0) : n > 0) = hx
   split
@@ -48,8 +48,8 @@ private theorem heapUpdateRootPossibleRootValues1 {α : Type u} (le : α → α
 private theorem heapUpdateRootPossibleRootValues2 {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n = 2) :
 have h₂ : 0 < n := Nat.lt_trans (Nat.lt_succ_self 0) $  h₁.substr (Nat.lt_succ_self 1)
 have h₃ : 0 < leftLen heap h₂ := heapUpdateRootPossibleRootValuesAuxL heap (h₁.substr (Nat.lt_succ_self 1))
-(heap.heapUpdateRoot le value h₂).fst.root h₂ = value
-∨ (heap.heapUpdateRoot le value h₂).fst.root h₂ = (heap.left h₂).root h₃
+(heap.heapUpdateRoot h₂ le value).fst.root h₂ = value
+∨ (heap.heapUpdateRoot h₂ le value).fst.root h₂ = (heap.left h₂).root h₃
 := by
   simp
   unfold heapUpdateRoot
@@ -68,9 +68,9 @@ private theorem heapUpdateRootPossibleRootValues3 {α : Type u} (le : α → α
 have h₂ : 0 < n := Nat.lt_trans (Nat.lt_succ_self 0) $ Nat.lt_trans (Nat.lt_succ_self 1) h₁
 have h₃ : 0 < leftLen heap h₂ := heapUpdateRootPossibleRootValuesAuxL heap $ Nat.lt_trans (Nat.lt_succ_self 1) h₁
 have h₄ : 0 < rightLen heap h₂ := heapUpdateRootPossibleRootValuesAuxR heap h₁
-(heap.heapUpdateRoot le value h₂).fst.root h₂ = value
-∨ (heap.heapUpdateRoot le value h₂).fst.root h₂ = (heap.left h₂).root h₃
-∨ (heap.heapUpdateRoot le value h₂).fst.root h₂ = (heap.right h₂).root h₄
+(heap.heapUpdateRoot h₂ le value).fst.root h₂ = value
+∨ (heap.heapUpdateRoot h₂ le value).fst.root h₂ = (heap.left h₂).root h₃
+∨ (heap.heapUpdateRoot h₂ le value).fst.root h₂ = (heap.right h₂).root h₄
 := by
   simp only
   unfold heapUpdateRoot
@@ -90,9 +90,9 @@ have h₄ : 0 < rightLen heap h₂ := heapUpdateRootPossibleRootValuesAuxR heap
       cases le (l.root _) (r.root _)
       <;> simp only [Bool.false_eq_true, ↓reduceIte, heapUpdateRootReturnsRoot, root_unfold, left_unfold, right_unfold, true_or, or_true]
 
-protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateRoot le value heap h₂).fst :=
+protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateRoot h₂ le value heap).fst :=
   if h₄ : n = 1 then by
-    have h₅ : le (heap.root h₂) ( (heapUpdateRoot le value heap h₂).fst.root h₂) := by simp only[h₃, h₄, heapUpdateRootPossibleRootValues1]
+    have h₅ : le (heap.root h₂) ( (heapUpdateRoot h₂ le value heap).fst.root h₂) := by simp only[h₃, h₄, heapUpdateRootPossibleRootValues1]
     unfold HeapPredicate.leOrLeaf
     split
     · rfl
@@ -101,7 +101,7 @@ protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α �
     have h₆ := heapUpdateRootPossibleRootValues2 le value heap h₅
     cases h₆
     case inl h₆ =>
-      have h₇ : le (heap.root h₂) ( (heapUpdateRoot le value heap h₂).fst.root h₂) := by simp only [h₆, h₃]
+      have h₇ : le (heap.root h₂) ((heapUpdateRoot h₂ le value heap).fst.root h₂) := by simp only [h₆, h₃]
       unfold HeapPredicate.leOrLeaf
       split
       · rfl
@@ -130,7 +130,7 @@ protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α �
     unfold HeapPredicate at h₁
     cases h₇
     case inl h₇ =>
-      have h₈ : le (heap.root h₂) ( (heapUpdateRoot le value heap h₂).fst.root h₂) := by simp only [h₇, h₃]
+      have h₈ : le (heap.root h₂) ( (heapUpdateRoot h₂ le value heap).fst.root h₂) := by simp only [h₇, h₃]
       unfold HeapPredicate.leOrLeaf
       split
       · rfl
@@ -155,7 +155,7 @@ private theorem heapUpdateRootIsHeapLeRootAuxLe {α : Type u} (le : α → α �
 | .inr h₅ => not_le_imp_le h₂ _ _ h₅
 | .inl h₅ => h₁ b c a ⟨h₃,not_le_imp_le h₂ _ _ h₅⟩
 
-theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateRoot le value h₁).fst le := by
+theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateRoot h₁ le value).fst le := by
     unfold heapUpdateRoot
     split
     rename_i o p v l r h₇ h₈ h₉ heq