Simplify CompleteTree.get, and remove (redundant) CompleteTree.get'

11 files changed, 251 insertions, 421 deletions

diff --git a/BinaryHeap.lean b/BinaryHeap.lean
index 61ebd42..4c7326f 100644
--- a/BinaryHeap.lean
+++ b/BinaryHeap.lean
@@ -53,12 +53,10 @@ def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le
   tree.indexOf pred
 
 instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) where
-  getElem := λ heap index h₁ ↦ match n, heap, index with
-  | (_+1), {tree, ..}, index => tree.get' ⟨index, h₁⟩
+  getElem := λ heap index h₁ ↦ heap.tree.get ⟨index, h₁⟩
 
 instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where
-  getElem := λ heap index _ ↦ match n, heap, index with
-  | (_+1), {tree, ..}, index => tree.get' index
+  getElem := λ heap index _ ↦ heap.tree.get index
 
 /--Helper for the common case of using natural numbers for sorting.-/
 theorem nat_ble_to_heap_le_total : total_le Nat.ble :=
diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean
index ee6b685..8038555 100644
--- a/BinaryHeap/CompleteTree/AdditionalOperations.lean
+++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean
@@ -32,27 +32,16 @@ def indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Opti
 ----------------------------------------------------------------------------------------------
 -- get
 
-/--Returns the lement at the given index. Indices are depth first.-/
-def get' {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α :=
-  match h₁ : index, h₂ : n, heap with
-  | 0, (_+_), .branch v _ _ _ _ _ => v
-  | ⟨j+1,h₃⟩, (o+p), .branch _ l r _ _ _ =>
-    if h₄ : j < o then
-      match o with
-      | (oo+1) => get' ⟨j, h₄⟩ l
-    else
-      have h₅ : n - o = p := Nat.sub_eq_of_eq_add $ (Nat.add_comm o p).subst h₂
-      have : p ≠ 0 :=
-        have h₆ : o < n := Nat.lt_of_le_of_lt (Nat.ge_of_not_lt h₄) (Nat.lt_of_succ_lt_succ h₃)
-        h₅.symm.substr $ Nat.sub_ne_zero_of_lt h₆
-      have h₆ : j - o < p := h₅.subst $ Nat.sub_lt_sub_right (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃
-      have _termination : j - o < index.val := (Fin.val_inj.mpr h₁).substr (Nat.sub_lt_succ j o)
-      match p with
-      | (pp + 1) => get' ⟨j - o, h₆⟩ r
-
+/--Returns the element at the given index. Indices are depth first.-/
 def get {α : Type u} {n : Nat} (index : Fin n) (heap : CompleteTree α n) : α :=
   match n, index, heap with
-  | (_+1), index, heap => heap.get' index
+  | (_+_+1), 0, .branch v _ _ _ _ _ => v
+  | (o+p+1), ⟨j+1,h₃⟩, .branch _ l r _ _ _ =>
+    if h₄ : j < o then
+      get ⟨j, h₄⟩ l
+    else
+      have h₄ : j - o < p := Nat.sub_lt_left_of_lt_add (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃
+      get ⟨j - o, h₄⟩ r
 
 ----------------------------------------------------------------------------------------------
 -- contains - implemented as decidable proposition
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
index 6614210..7a0c893 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
@@ -3,93 +3,46 @@ import BinaryHeap.CompleteTree.AdditionalProofs.Get
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
-private theorem if_get_eq_contains {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (index : Fin (o+1)) : tree.get' index = element → tree.contains element := by
-    unfold get' contains
-    simp only [Nat.succ_eq_add_one, Fin.zero_eta, Nat.add_eq, ne_eq]
-    split
-    case h_1 p q v l r _ _ _ _ =>
-      intro h₁
-      split; omega
-      rename α => vv
-      rename_i hsum heq
-      have h₂ := heqSameRoot (hsum) (Nat.succ_pos (p+q)) heq
-      rw[root_unfold] at h₂
-      rw[root_unfold] at h₂
-      simp only [←h₂, h₁, true_or]
-    case h_2 index p q v l r _ _ _ _ h₃ =>
-      intro h₄
-      split ; rename_i hx _; exact absurd hx (Nat.succ_ne_zero _)
-      case h_2 pp qq vv ll rr _ _  _ h₅ heq =>
-      have : p = pp := heqSameLeftLen h₅ (Nat.succ_pos _) heq
-      have : q = qq := heqSameRightLen h₅ (Nat.succ_pos _) heq
-      subst pp qq
-      simp only [Nat.add_eq, Nat.succ_eq_add_one, heq_eq_eq, branch.injEq] at heq
-      have : v = vv := heq.left
-      have : l = ll := heq.right.left
-      have : r = rr := heq.right.right
-      subst vv ll rr
-      revert h₄
-      split
-      all_goals
-        split
-        intro h₄
-        right
+private theorem if_get_eq_contains {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (index : Fin n) : tree.get index = element → tree.contains element := by
+    rw[get_unfold]
+    rw[contains_as_root_left_right]
+    intro h₁
+    split at h₁
+    case isTrue =>
+      left
+      assumption
+    case isFalse h =>
+      have _termination : index.val ≠ 0 := Fin.val_ne_iff.mpr h
+      right
+      simp only at h₁
+      split at h₁
       case' isTrue => left
       case' isFalse => right
       all_goals
-        revert h₄
+        revert h₁
         apply if_get_eq_contains
-        done
+termination_by index.val
 
-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
+private theorem if_contains_get_eq_auxl {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : n > 0):
+  ∀(indexl : Fin (tree.leftLen h₁)), (tree.left _).get indexl = element → ∃(index : Fin n), tree.get index = element
 := by
   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]
-    exact Nat.lt_of_lt_of_le indexl.isLt $ Nat.le_of_lt_succ $ leftLenLtN tree (Nat.succ_pos o)
-  )
+  let index : Fin n := indexl.succ.castLT (Nat.lt_of_le_of_lt (Nat.succ_le_of_lt indexl.isLt) (leftLenLtN tree h₁))
   intro prereq
   exists index
-  unfold get
-  simp
-  unfold get'
-  generalize hindex : index = i
-  split
-  case h_1 =>
-    have : index.val = 0 := Fin.val_eq_of_eq hindex
-    contradiction
-  case h_2 j p q v l r ht1 ht2 ht3 _ _ =>
-    have h₂ : index.val = indexl.val + 1 := rfl
-    have h₃ : index.val = j.succ := Fin.val_eq_of_eq hindex
-    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]
-    unfold get at prereq
-    split at prereq
-    rename_i pp ii ll hel hei heq
-    split
-    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 *
-    have : j = ii.val := by omega
-    subst j
-    simp
-    rw[←hei] at prereq
-    rw[left_unfold] at heq
-    rw[heq]
-    assumption
+  have h₂ : index > ⟨0,h₁⟩ := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr $ Fin.succ_ne_zero _
+  have h₃ : index.val ≤ tree.leftLen h₁ := Nat.succ_le_of_lt indexl.isLt
+  rw[get_left _ _ h₂ h₃]
+  exact prereq
 
-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
+private theorem if_contains_get_eq_auxr {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : n > 0):
+  ∀(indexr : Fin (tree.rightLen h₁)), (tree.right _).get indexr = element → ∃(index : Fin n), tree.get index = element
 := by
   intro indexr
-  let index : Fin (o+1) := ⟨(tree.leftLen (Nat.succ_pos o) + indexr.val + 1), by
-    have h₂ : tree.leftLen (Nat.succ_pos _) + tree.rightLen _ + 1 = tree.length := Eq.symm $ lengthEqLeftRightLenSucc tree _
+  let index : Fin n := ⟨(tree.leftLen h₁ + indexr.val + 1), by
+    have h₂ : tree.leftLen h₁ + tree.rightLen _ + 1 = tree.length := Eq.symm $ lengthEqLeftRightLenSucc tree _
     rw[length] at h₂
-    have h₃ : tree.leftLen (Nat.succ_pos o) + indexr.val + 1 < tree.leftLen (Nat.succ_pos o) + tree.rightLen (Nat.succ_pos o) + 1 := by
+    have h₃ : tree.leftLen h₁ + indexr.val + 1 < tree.leftLen h₁ + tree.rightLen h₁ + 1 := by
       apply Nat.succ_lt_succ
       apply Nat.add_lt_add_left
       exact indexr.isLt
@@ -97,95 +50,39 @@ private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : Complete
   ⟩
   intro prereq
   exists index
-  unfold get
-  simp
-  unfold get'
-  generalize hindex : index = i
-  split
-  case h_1 =>
-    have : index.val = 0 := Fin.val_eq_of_eq hindex
-    contradiction
-  case h_2 j p q v l r ht1 ht2 ht3 _ _ =>
-    have h₂ : index.val = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) + indexr.val + 1 := rfl
-    have h₃ : index.val = j.succ := Fin.val_eq_of_eq hindex
-    have h₄ : j = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) + indexr.val := by
-      rw[h₃] at h₂
-      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]
-    unfold get at prereq
-    split at prereq
-    rename_i pp ii rr hel hei heq
-    split
-    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 *
-    have : j = ii.val + p := by omega
-    subst this
-    simp
-    rw[right_unfold] at heq
-    rw[heq]
-    assumption
+  have h₂ : tree.leftLen h₁ < tree.leftLen h₁ + indexr.val + 1 := Nat.lt_of_le_of_lt (Nat.le_add_right _ _) (Nat.lt_succ_self _)
+  rw[get_right _ index h₂]
+  have : index.val - tree.leftLen h₁ - 1 = indexr.val :=
+    have : index.val = tree.leftLen h₁ + indexr.val + 1 := rfl
+    have : index.val = indexr.val + tree.leftLen h₁ + 1 := (Nat.add_comm indexr.val (tree.leftLen h₁)).substr this
+    have : index.val - (tree.leftLen h₁ + 1) = indexr.val := Nat.sub_eq_of_eq_add this
+    (Nat.sub_sub _ _ _).substr this
+  simp only[this]
+  assumption
 
-private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.contains element) : ∃(index : Fin (o+1)), tree.get' index = element := by
-    revert h₁
-    unfold contains
-    split ; rename_i hx _; exact absurd hx (Nat.succ_ne_zero o)
-    rename_i n m v l r _ _ _ he heq
-    intro h₁
+private theorem if_contains_get_eq {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) (h₁ : tree.contains element) : ∃(index : Fin n), tree.get index = element := by
+    unfold contains at h₁
+    match n, tree with
+    | 0, .leaf => contradiction
+    | (o+p+1), .branch v l r o_le_p max_height_diff subtree_complete =>
     cases h₁
-    case h_2.inl h₂ =>
-      unfold get'
+    case inl h₂ =>
       exists 0
-      split
-      case h_2 hx => have hx := Fin.val_eq_of_eq hx; simp at hx;
-      case h_1 vv _ _ _ _ _ _ _ =>
-        have h₃ := heqSameRoot he (Nat.succ_pos _) heq
-        simp only[root_unfold] at h₃
-        simp only[h₃, h₂]
-    rename_i h
-    cases h
-    case h_2.inr.inl h₂ => exact
-      match hn : n, hl: l with
-      | 0, .leaf => by contradiction
-      | (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
-        simp only at h₄
-        simp[get_eq_get'] at h₃ ⊢
-        apply h₃.elim
-        match o, tree with
-        | (yy+_), .branch _ ll _ _ _ _ =>
-          simp_all[left_unfold, leftLen_unfold]
-          have : yy = nn+1 := heqSameLeftLen (by omega) (Nat.succ_pos _) heq
-          have : _ = m := heqSameRightLen (by omega) (Nat.succ_pos _) heq
-          subst yy m
-          simp_all
-          exact h₄
-    case h_2.inr.inr h₂ => exact
-      match hm : m, hr: r with
-      | 0, .leaf => by contradiction
-      | (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 h₄ := if_contains_get_eq_auxr tree element
-        simp[get_eq_get'] at h₃ ⊢
-        apply h₃.elim
-        match o, tree with
-        | (_+zz), .branch _ _ rr _ _ _ =>
-          simp_all[right_unfold, rightLen_unfold]
-          have : _ = n := heqSameLeftLen (by omega) (Nat.succ_pos _) heq
-          have : zz = mm+1 := heqSameRightLen (by omega) (Nat.succ_pos _) heq
-          subst n zz
-          simp_all
-          exact h₄
-  termination_by o
+    case inr h₂ =>
+      cases h₂
+      case inl h₂ =>
+        have h₄ := if_contains_get_eq l element h₂
+        have h₅ := if_contains_get_eq_auxl (.branch v l r o_le_p max_height_diff subtree_complete) element (Nat.succ_pos _)
+        apply h₄.elim
+        assumption
+      case inr h₂ =>
+        have h₄ := if_contains_get_eq r element h₂
+        have h₅ := if_contains_get_eq_auxr (.branch v l r o_le_p max_height_diff subtree_complete) element (Nat.succ_pos _)
+        apply h₄.elim
+        assumption
 
 
-theorem contains_iff_index_exists' {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) : tree.contains element ↔ ∃ (index : Fin (o+1)), tree.get' index = element := by
+theorem contains_iff_index_exists' {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : tree.contains element ↔ ∃ (index : Fin n), tree.get index = element := by
   constructor
   case mpr =>
     simp only [forall_exists_index]
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean
index 902afc4..32bf722 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Find.lean
@@ -44,14 +44,14 @@ private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : Compl
     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[get_left (.branch v l r p_le_o max_height_difference subtree_complete) _ 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[get_right (.branch v l r p_le_o max_height_difference subtree_complete) _ h₄₂]
         rw[right_unfold]
         have := indexOfNoneImpPredFalseAux r pred (currentIndex + o + 1)
         simp only [Option.isNone_iff_eq_none, Bool.not_eq_true] at this
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index f872836..1012ef5 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -3,64 +3,39 @@ 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 := rfl
+theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ :=
+  match h₂ : n, h₃ : (⟨0,h₁⟩ : Fin n), tree with
+  | (_+_+1), 0, .branch v _ _ _ _ _ => rfl
+  | nn+1, ⟨j+1,h₄⟩, _ => by
+    subst h₂
+    simp only [heq_eq_eq, Fin.ext_iff] at h₃
 
-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 =>
-    unfold get'
-    split
-    case h_2 hx => exact absurd (Fin.mk.inj hx) (Nat.zero_ne_add_one _)
-    case h_1 => trivial
-
-theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₁ : n > 0) (h₂ : index > tree.leftLen h₁) :
-  have h₃ : ↑index - tree.leftLen h₁ - 1 < tree.rightLen h₁ := by
-    revert h₂
-    unfold leftLen rightLen length
-    split
-    intro h₂
-    rename_i o p v l r _ _ _ _
-    have h₃ := index.isLt
-    apply Nat.sub_lt_right_of_lt_add
-    omega
-    apply Nat.sub_lt_right_of_lt_add
-    omega
-    have : p+1+o = (o.add p).succ := by simp_arith
-    rw[this]
-    assumption
-  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
-    unfold get get'
-    split
-    case h_1 =>
-      contradiction
-    case h_2 j h₃ o2 p2 v2 l2 r2 _ _ _ d1 he₁ he₂ _ =>
-      clear d1
-      have : o = o2 := heqSameLeftLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂
-      have : p = p2 := heqSameRightLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂
-      subst o2 p2
-      simp at he₂
-      have : v = v2 := he₂.left
-      have : l = l2 := he₂.right.left
-      have : r = r2 := he₂.right.right
-      subst r2 l2 v2
-      simp_all
-      have : ¬j < o := by simp_arith[h₂]
-      simp[this]
-      cases p <;> simp
-      case zero =>
-        omega
-      case succ pp _ _ _ _ _ _ =>
-        have : j + 1 - o - 1 = j - o := by omega
-        simp[this] at hnew
-        rw[get_eq_get']
-        assumption
+theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₂ : index > tree.leftLen (Nat.zero_lt_of_lt index.isLt))
+  : have h₁ : n > 0 := Nat.zero_lt_of_lt index.isLt
+    have h₃ : ↑index - tree.leftLen h₁ - 1 < tree.rightLen h₁ := by
+      revert h₂
+      unfold leftLen rightLen length
+      split
+      intro h₂
+      rename_i o p v l r _ _ _
+      have h₃ := index.isLt
+      apply Nat.sub_lt_right_of_lt_add
+      omega
+      apply Nat.sub_lt_right_of_lt_add
+      omega
+      have : p+1+o = (o.add p).succ := by simp_arith
+      rw[this]
+      assumption
+    tree.get index = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩
+  :=
+  match n, index, tree with
+  | (o+p+1), ⟨j+1,h₃⟩, .branch _ _ r _ _ _ =>
+    if h₄ : j < o then
+      absurd h₄ $ Nat.not_lt_of_ge (Nat.le_of_lt_succ h₂)
+    else by
+      simp only[right_unfold, leftLen_unfold]
+      have : j + 1 - o - 1 = j - o := by omega
+      simp (config := {autoUnfold := true})[this, h₄]
 
 theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r : CompleteTree α m} {m_le_n : m ≤ n} {max_height_diff : n < 2 * (m + 1)} {subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo} (index : Fin (n + m + 1)) (h₁ : index > n) :
   have h₂ : ↑index - n - 1 < m := by
@@ -74,36 +49,73 @@ theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r
     assumption
   (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₁
+  get_right (branch v l r m_le_n max_height_diff subtree_complete) index 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₁) :
+theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₂ : index > ⟨0, (Nat.zero_lt_of_lt index.isLt)⟩) (h₃ : index ≤ tree.leftLen (Nat.zero_lt_of_lt index.isLt)) :
+  have h₁ : n > 0 := Nat.zero_lt_of_lt index.isLt
   have h₃ : ↑index - 1 < tree.leftLen h₁ := Nat.lt_of_lt_of_le (Nat.pred_lt_self 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
-    unfold get get'
-    split
-    case h_1 => contradiction
-    case h_2 j h₃ o2 p2 v2 l2 r2 _ _ _ d1 he₁ he₂ =>
-      clear d1
-      have : o = o2 := heqSameLeftLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂
-      have : p = p2 := heqSameRightLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂
-      subst o2 p2
-      simp[leftLen_unfold] at h₃
-      have h₄ : j < o :=Nat.lt_of_succ_le h₃
-      simp[h₄]
-      cases o ; contradiction
-      case succ oo =>
-        simp at hnew he₂ ⊢
-        have := he₂.right.left
-        subst l2
-        assumption
+    match n, index, tree with
+  | (o+p+1), ⟨j+1,h₅⟩, .branch _ l _ _ _ _ =>
+    if h₄ : j < o then by
+      simp only[left_unfold, leftLen_unfold]
+      have : j + 1 - o - 1 = j - o := by omega
+      simp (config := {autoUnfold := true})[this, h₄]
+    else
+      absurd (Nat.lt_of_succ_le h₃) h₄
 
 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 = 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₂
+  get_left (branch v l r m_le_n max_height_diff subtree_complete) index h₁ h₂
+
+theorem get_unfold {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n)
+  :
+  have h₁ : n > 0 := (Nat.zero_lt_of_lt index.isLt)
+  tree.get index =
+    if h₂ : index = ⟨0, h₁⟩ then
+      tree.root h₁
+    else if h₃ : index ≤ tree.leftLen h₁ then
+      have h₃ : ↑index - 1 < tree.leftLen h₁ := Nat.lt_of_lt_of_le (Nat.pred_lt_self $ Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂) h₃
+      (tree.left h₁).get ⟨index.val - 1, h₃⟩
+    else
+      have h₃ : ↑index - tree.leftLen h₁ - 1 < tree.rightLen h₁ := by
+        revert h₃
+        unfold leftLen rightLen length
+        split
+        intro h₂
+        rename_i o p v l r _ _ _ _ _
+        have h₃ := index.isLt
+        apply Nat.sub_lt_right_of_lt_add
+        omega
+        apply Nat.sub_lt_right_of_lt_add
+        omega
+        have : p+1+o = (o.add p).succ := by simp_arith
+        rw[this]
+        assumption
+      (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩
+  :=
+  have h₁ : n > 0 := (Nat.zero_lt_of_lt index.isLt)
+  if h₂ : index = ⟨0, h₁⟩ then by
+    simp only [h₂]
+    exact Eq.symm $ get_zero_eq_root _ _
+  else if h₃ : index ≤ tree.leftLen h₁ then by
+    simp [h₂, h₃]
+    exact get_left tree index (Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂) h₃
+  else by
+    simp [h₂, h₃]
+    exact get_right tree index (Nat.gt_of_not_le h₃)
+
+theorem get_unfold' {α : 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)) :
+  (branch v l r m_le_n max_height_diff subtree_complete).get index = if h₂ : index = ⟨0, Nat.zero_lt_of_lt index.isLt⟩ then
+      v
+    else if h₃ : index ≤ n then
+      have h₃ : ↑index - 1 < n := Nat.lt_of_lt_of_le (Nat.pred_lt_self $ Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂) h₃
+      l.get ⟨index.val - 1, h₃⟩
+    else
+      have h₃ : ↑index - n - 1 < m := by omega
+      r.get ⟨index.val - n - 1, h₃⟩
+  :=
+    get_unfold _ _
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
index 807bdcb..09b1450 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
@@ -37,8 +37,6 @@ theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (
     if h₂ : index = (Internal.heapRemoveLastWithIndex tree).snd.snd then
       have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex tree
       rw[←h₂] at h₃
-      unfold get
-      simp only
       have := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement tree
       rw[←this] at h₃
       simp[h₃, heapUpdateRootContainsUpdatedElement]
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
index ea2b5a7..62b0e2c 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
@@ -87,7 +87,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo
           split
           case' isFalse => rw[←containsSeesThroughCast]
           case' isTrue | isFalse =>
-            rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) index (Nat.succ_pos _) h₂₂ h₃]
+            rw[get_left (.branch v l r p_le_o max_height_difference subtree_complete) index h₂₂ h₃]
             rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
             right; left
             rw[left_unfold]
@@ -102,7 +102,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo
           split
           case' isFalse => rw[←containsSeesThroughCast]
           case' isTrue | isFalse =>
-            rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) index (Nat.succ_pos _) (Nat.gt_of_not_le h₃)]
+            rw[get_right (.branch v l r p_le_o max_height_difference subtree_complete) index (Nat.gt_of_not_le h₃)]
             rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
             right; right
             rw[right_unfold]
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
index a8a551f..dcff870 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
@@ -5,11 +5,11 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
-theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).snd = heap.get' index := by
+theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).snd = heap.get index := by
   unfold heapRemoveAt
   if h₁ : index = 0 then
     simp only [h₁, ↓reduceDIte]
-    rw[get_eq_get', ←Fin.zero_eta, ←get_zero_eq_root]
+    rw[←Fin.zero_eta, ←get_zero_eq_root]
     exact heapPopReturnsRoot heap le
   else
     simp only [h₁, ↓reduceDIte, ge_iff_le]
@@ -20,15 +20,15 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
       if h₃ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ index then
         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₄]
+        rewrite[←h₄]
         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₄]
+        rewrite[←h₄]
         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
+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
   if h₂ : removeIndex = 0 then
     subst removeIndex
@@ -45,13 +45,13 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo
         simp only [gt_iff_lt] at h₅
         split at h₅
         case isTrue h₆ =>
-          rw[get_eq_get', ←h₅]
+          rw[←h₅]
           apply heapUpdateAtOnlyUpdatesAt
           simp only [ne_eq, Fin.pred_inj, h₁, not_false_eq_true]
         case isFalse h₆ =>
           split at h₅
           case isTrue h₇ =>
-            rw[get_eq_get', ←h₅]
+            rw[←h₅]
             apply heapUpdateAtOnlyUpdatesAt
             simp only [ne_eq, Fin.ext_iff, Fin.coe_pred, Fin.coe_castLT]
             generalize (Internal.heapRemoveLastWithIndex heap).snd.snd = j at *
@@ -69,7 +69,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo
         simp only [gt_iff_lt] at h₅
         split at h₅
         case isTrue h₆ =>
-          rw[get_eq_get', ←h₅]
+          rw[←h₅]
           apply heapUpdateAtOnlyUpdatesAt
           simp[Fin.ext_iff]
           generalize (Internal.heapRemoveLastWithIndex heap).snd.snd = j at *
@@ -77,7 +77,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo
         case isFalse h₆ =>
           split at h₅
           case isTrue h₇ =>
-            rw[get_eq_get', ←h₅]
+            rw[←h₅]
             apply heapUpdateAtOnlyUpdatesAt
             rw[←Fin.val_ne_iff] at h₁ ⊢
             exact h₁
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index 694a0ee..cf0774f 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -7,84 +7,39 @@ import BinaryHeap.CompleteTree.NatLemmas
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
 /--Shows that the index and value returned by heapRemoveLastWithIndex are consistent.-/
-protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get' (Internal.heapRemoveLastWithIndex heap).snd.snd = (Internal.heapRemoveLastWithIndex heap).snd.fst := by
+protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : Nat} (heap : CompleteTree α (o+1)) : heap.get (Internal.heapRemoveLastWithIndex heap).snd.snd = (Internal.heapRemoveLastWithIndex heap).snd.fst := by
   unfold CompleteTree.Internal.heapRemoveLastWithIndex CompleteTree.Internal.heapRemoveLastAux
   split
   rename_i n m v l r m_le_n max_height_difference subtree_full
   simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, decide_eq_true_eq, Fin.castLE_succ]
   split
   case isTrue n_m_zero =>
-    unfold get'
-    split
-    case h_1 nn mm vv ll rr mm_le_nn _ _ _ _ he₁ he₂ =>
-      have h₁ : n = 0 := And.left $ Nat.add_eq_zero.mp n_m_zero.symm
-      have h₂ : m = 0 := And.right $ Nat.add_eq_zero.mp n_m_zero.symm
-      have h₃ : nn = 0 := And.left (Nat.add_eq_zero.mp $ Eq.symm $ (Nat.zero_add 0).subst (motive := λx ↦ x = nn + mm) $ h₂.subst (motive := λx ↦ 0 + x = nn + mm) (h₁.subst (motive := λx ↦ x + m = nn + mm) he₁))
-      have h₄ : mm = 0 := And.right (Nat.add_eq_zero.mp $ Eq.symm $ (Nat.zero_add 0).subst (motive := λx ↦ x = nn + mm) $ h₂.subst (motive := λx ↦ 0 + x = nn + mm) (h₁.subst (motive := λx ↦ x + m = nn + mm) he₁))
-      subst n m nn mm
-      exact And.left $ CompleteTree.branch.inj (eq_of_heq he₂.symm)
-    case h_2 =>
-      omega -- to annoying to deal with Fin.ofNat... There's a hypothesis that says 0 = ⟨1,_⟩.
+    have h₁ : n = 0 := And.left $ Nat.add_eq_zero.mp n_m_zero.symm
+    have h₂ : m = 0 := And.right $ Nat.add_eq_zero.mp n_m_zero.symm
+    subst n m
+    rfl
   case isFalse n_m_not_zero =>
-    unfold get'
     split
-    case h_1 nn mm vv ll rr mm_le_nn max_height_difference_2 subtree_full2 _ he₁ he₂ he₃ =>
-      --aaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
-      --okay, I know that he₁ is False.
-      --but reducing this wall of text to something the computer understands - I am frightened.
-      exfalso
-      revert he₁
-      split
-      case' isTrue => cases l; case leaf hx => exact absurd hx.left $ Nat.not_lt_zero m
-      all_goals
-        apply Fin.ne_of_val_ne
-        simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, Nat.add_one_ne_zero, not_false_eq_true]
-      --okay, this wasn't that bad
-    case h_2 j j_lt_n_add_m nn mm vv ll rr mm_le_nn max_height_difference_2 subtree_full2 heap he₁ he₂ he₃ =>
-      --he₁ relates j to the other indices. This is the important thing here.
-      --it should be reducible to j = (l or r).heap.heapRemoveLastWithIndex.snd.snd
-      --or something like it.
-
-      --but first, let's get rid of mm and nn, and vv while at it.
-      -- which are equal to m, n, v, but we need to deduce this from he₃...
-      have : n = nn := heqSameLeftLen (congrArg (·+1) he₂) (Nat.succ_pos _) he₃
-      have : m = mm := heqSameRightLen (congrArg (·+1) he₂) (Nat.succ_pos _) he₃
-      subst nn mm
-      simp only [heq_eq_eq, branch.injEq] at he₃
-      -- yeah, no more HEq fuglyness!
-      have : v = vv := he₃.left
-      have : l = ll := he₃.right.left
-      have : r = rr := he₃.right.right
-      subst vv ll rr
-      split at he₁
-      <;> rename_i goLeft
-      <;> simp only [goLeft, and_self, ↓reduceDIte, Fin.isValue]
-      case' isTrue =>
-        cases l;
-        case leaf => exact absurd goLeft.left $ Nat.not_lt_zero m
-        rename_i o p _ _ _ _ _ _ _
-      case' isFalse =>
-        cases r;
-        case leaf => simp (config := { ground := true }) only [and_true, Nat.not_lt, Nat.le_zero_eq] at goLeft;
-                     exact absurd ((Nat.add_zero n).substr goLeft.symm) n_m_not_zero
-      all_goals
-        have he₁ := Fin.val_eq_of_eq he₁
-        simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, Nat.reduceEqDiff] at he₁
-        have : max_height_difference_2 = max_height_difference := rfl
-        have : subtree_full2 = subtree_full := rfl
-        subst max_height_difference_2 subtree_full2
-        rename_i del1 del2
-        clear del1 del2
-      case' isTrue =>
-        have : j < o + p + 1 := by omega --from he₁. It has j = (blah : Fin (o+p+1)).val
-      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]
-        subst j -- overkill, but unlike rw it works
-        simp only [Nat.pred_succ, Fin.isValue, Nat.add_sub_cancel, Fin.eta]
+    case isTrue goLeft =>
+      match _term : n, l, m_le_n, max_height_difference, subtree_full with
+      | (nn+1), l ,m_le_n, max_height_difference, subtree_full =>
+      dsimp only [Fin.isValue, Nat.succ_eq_add_one]
+      rw[get_left, left_unfold]
+      case h₂ => exact Nat.succ_pos _
+      case h₃ => exact (Internal.heapRemoveLastAux (β := λ n ↦ α × Fin n) l _ _ _).2.snd.isLt
+      apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex
+    case isFalse goRight =>
+      dsimp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, Fin.isValue]
+      cases r -- to work around cast
+      case leaf => simp (config:={ground:=true}) at goRight; exact absurd goRight.symm n_m_not_zero
+      case branch rv rl rr rm_le_n rmax_height_difference rsubtree_full =>
+        rw[get_right, right_unfold]
+        case h₂ => simp_arith[leftLen_unfold]
+        simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat, leftLen_unfold]
+        have : ∀(a : Nat), a + n + 1 - n - 1 = a := λa↦(Nat.add_sub_cancel _ _).subst $ (Nat.add_assoc a n 1).subst (motive := λx↦a+n+1-n-1 = x-(n+1)) $ (Nat.sub_sub (a+n+1) n 1).subst rfl
+        simp only[this]
         apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex
-        done
+
 
 protected theorem heapRemoveLastWithIndexLeavesRoot {α : Type u} {n: Nat} (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.succ_pos n) = (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.root h₁ :=
   CompleteTree.heapRemoveLastAuxLeavesRoot heap _ _ _ h₁
@@ -267,7 +222,6 @@ 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]
@@ -502,10 +456,10 @@ protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Ty
   else by
     right
     have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap
-    unfold get
     simp at h₁
     subst index
-    exact h₂.symm
+    rw[h₂]
+    rfl
 
 /--
   Shows that each element contained before removing the last that is not the last is still contained after removing the last.
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
index be82a57..606b687 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
@@ -5,19 +5,18 @@ import BinaryHeap.CompleteTree.AdditionalProofs.Get
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
+theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot h₁ le := by
+  funext
+  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
   cases index
   rename_i i isLt
   cases i
   case mk.zero =>
-    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₄ _ _=>
-      exact Eq.symm $ heapUpdateRootReturnsRoot le val (.branch v l r h₂ h₃ h₄) (Nat.succ_pos _)
+    rw[←get_zero_eq_root, heapUpdatAtRootEqUpdateRoot]
+    exact Eq.symm $ heapUpdateRootReturnsRoot le val heap isLt
   case mk.succ j =>
     unfold heapUpdateAt heapUpdateAtAux
     generalize hj : (⟨j + 1, isLt⟩ : Fin n) = index -- otherwise split fails...
@@ -37,18 +36,12 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
           exact h₂
         apply heapUpdateAtReturnsElementAt
       case isFalse h₂ =>
-        rw[get_right _ _]
-        case h₁ => exact Nat.succ_pos _
+        rw[get_right]
         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 h₁ le := by
-  funext
-  unfold heapUpdateAt heapUpdateAtAux
-  rfl
-
 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₁
@@ -141,7 +134,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
       case false.isTrue h₅ | true.isTrue 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₆]
-          rw[get_left _ _ (Nat.succ_pos _) h₄₂ this]
+          rw[get_left _ _ h₄₂ this]
           left
           --rw[left_unfold]
           have : o < o + p + 1 := Nat.lt_of_le_of_lt (Nat.le_add_right o p) (Nat.lt_succ_self (o+p))
@@ -150,7 +143,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
           exact (Nat.pred_ne_of_ne (Fin.pos_iff_ne_zero.mpr h₃) (Fin.pos_iff_ne_zero.mpr h₄)).mp $ Fin.val_ne_iff.mpr h₂
         else
           have : 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 _) this]
+          rw[get_right _ _ this]
           right
           --rw[right_unfold]
           --rw[right_unfold]
@@ -164,7 +157,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
       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₆]
-          rw[get_left _ _ (Nat.succ_pos _) h₄₂ this]
+          rw[get_left _ _ h₄₂ this]
           left
           --rw[left_unfold]
           --rw[left_unfold]
@@ -175,7 +168,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
           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₆]
+          rw[get_right _ _ h₆]
           right
           --rw[right_unfold]
           have : p < o + p + 1 := Nat.lt_of_le_of_lt (Nat.le_add_left p o) (Nat.lt_succ_self (o+p))
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index cd765bb..1a44da1 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -18,10 +18,8 @@ abbrev heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Boo
   -/
 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
-  simp at h₃
   rename_i o p v l r p_le_o _ _ _
   cases o
   case zero =>
@@ -30,50 +28,46 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
     exact absurd (Fin.fin_one_eq_zero index) h₂
   case succ oo _ _ _ =>
     simp
-    unfold get' at h₃
-    split at h₃
-    case h_1 => omega
-    case h_2 j _ o2 p2 v2 l2 r2 _ _ _ _ he1 he2 =>
-      have : oo+1 = o2 := heqSameLeftLen (congrArg Nat.succ he1) (by simp_arith) he2
-      have : p = p2 := heqSameRightLen (congrArg Nat.succ he1) (by simp_arith) he2
-      subst o2
-      subst p2
-      simp at he2
-      have := he2.left
-      have := he2.right.left
-      have := he2.right.right
-      subst v2 l2 r2
-      simp at h₃
-      cases p
-      case zero =>
-        have : j < oo + 1 := by omega
-        simp[this] at h₃ ⊢
-        cases le value (l.root _) <;> simp
-        case false =>
-          cases j
-          case zero =>
-            rw[heapUpdateRootReturnsRoot]
-            rw[get_zero_eq_root]
-            unfold get; simp only
-            rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)]
-            left
-            rw[root_unfold]
-          case succ jj h₄ =>
-            have h₅ : oo = 0 := by omega
-            have h₆ : jj < oo := Nat.lt_of_succ_lt_succ this
-            have h₆ : jj < 0 := h₅.subst h₆
-            exact absurd h₆ $ Nat.not_lt_zero jj
-        case true h₄ _ _ _ _ _=>
-          rw[contains_as_root_left_right _ _ h₄]
-          right
+    rw[get_unfold'] at h₃
+    simp only[h₂, reduceDIte] at h₃
+    cases p
+    case zero =>
+      let j := index.val.pred
+      simp at h₃ ⊢
+      have : index.val ≤ oo + 1 := Nat.le_of_lt_succ index.isLt
+      simp only [this, reduceDIte] at h₃
+      cases le value (l.root _) <;> simp
+      case false =>
+        cases hj : j
+        case zero =>
+          rw[heapUpdateRootReturnsRoot]
+          rw[get_zero_eq_root]
+          rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
           left
-          rewrite[contains_iff_index_exists']
-          exists ⟨j,this⟩
-      case succ pp _ _ _ _ _ _ _ _ =>
+          rw[root_unfold]
+          simp only[←hj]
+          exact h₃
+        case succ jj =>
+          have h₅ : oo = 0 := by omega
+          have h₆ : index.val = jj + 1 + 1 := hj.subst (motive := λx ↦ index.val = x + 1) $ Eq.symm $ Nat.succ_pred (Fin.val_ne_iff.mpr h₂)
+          have h₇ : jj < 0 := h₅.subst $ Nat.le_of_succ_le_succ $ h₆.subst (motive := λx ↦ x ≤ oo + 1) this
+          exact absurd h₇ $ Nat.not_lt_zero jj
+      case true h₄ =>
+        rw[contains_as_root_left_right _ _ h₄]
+        right
+        left
+        rewrite[contains_iff_index_exists']
+        exists ⟨j, (Nat.succ_pred (Fin.val_ne_iff.mpr h₂)).substr (p := λx ↦ x ≤ oo + 1) this⟩
+    case succ pp _ _ _ =>
+      have h₂ := Fin.val_ne_iff.mpr h₂
+      generalize hi :  index.val = i at h₂ ⊢
+      simp only[hi] at h₃
+      cases i; contradiction
+      case succ j =>
         simp
         if h : j < oo + 1 then
           -- index was in l
-          simp only [h, ↓reduceDIte] at h₃
+          simp only [Nat.succ_le_of_lt h, ↓reduceDIte] at h₃
           split
           case isTrue =>
             simp
@@ -91,8 +85,6 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
               cases j
               case zero =>
                 rw[get_zero_eq_root]
-                unfold get
-                simp only
                 rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)]
                 left
                 rw[root_unfold]
@@ -104,8 +96,8 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
                 rw[←h₃, left_unfold]
                 have : oo + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination
                 apply heapUpdateRootOnlyUpdatesRoot
-                apply Fin.ne_of_val_ne
-                simp only [Nat.add_one_ne_zero, not_false_eq_true]
+                apply Fin.val_ne_iff.mp
+                exact Nat.succ_ne_zero _
             case isFalse =>
               -- r.root gets moved up
               rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
@@ -116,9 +108,9 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
               exists ⟨j, h⟩
         else
           -- index was in r
-          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₄)
+          have : j + 1 - (oo + 1) - 1 = j - oo - 1 := (Nat.sub_sub (j+1) 1 oo).substr $ (Nat.add_comm oo 1).substr rfl
+          simp only [this, Not.intro $ h ∘ Nat.lt_of_succ_le ∘ (Nat.succ_eq_add_one j).substr, ↓reduceDIte] at 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 $ hi.subst (motive := λx ↦ x < _) index.isLt)
           split
           case isTrue h₄ _ _ _ _ _ =>
             simp
@@ -141,14 +133,12 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
             case isFalse =>
               --r.root gets moved up
               simp only
-              generalize h₅ : j - (oo + 1) = jr
+              generalize h₅ : j - oo - 1 = jr
               simp only [h₅] at h₃
               have h₄ : jr < pp+1 := h₅.subst (motive := λx ↦ x < pp+1) h₄
               cases jr
               case zero =>
                 rw[get_zero_eq_root]
-                unfold get
-                simp only
                 rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)]
                 left
                 rw[root_unfold]
@@ -161,7 +151,6 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
                 apply heapUpdateRootOnlyUpdatesRoot
                 apply Fin.ne_of_val_ne
                 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 h₁ le value).fst.contains value := by
   unfold heapUpdateRoot