Remove redundant contains_iff_index_exists' function.

5 files changed, 12 insertions, 21 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
index 7a0c893..950183b 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean
@@ -82,14 +82,10 @@ private theorem if_contains_get_eq {α : Type u} {n : Nat} (tree : CompleteTree
         assumption
 
 
-theorem contains_iff_index_exists' {α : Type u} {n : Nat} (tree : CompleteTree α n) (element : α) : tree.contains element ↔ ∃ (index : Fin n), 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]
     exact if_get_eq_contains tree element
   case mp =>
     exact if_contains_get_eq tree 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/HeapPush.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
index 62b0e2c..1585b99 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
@@ -93,7 +93,7 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo
             rw[left_unfold]
             rw[left_unfold]
           case isTrue =>
-            rw[contains_iff_index_exists _ _ (Nat.lt_of_lt_of_le (Fin.lt_iff_val_lt_val.mp h₂₂) h₃)]
+            rw[contains_iff_index_exists _ _]
             have : index.val - 1 < o := Nat.sub_one_lt_of_le h₂₂ h₃
             exists ⟨index.val - 1, this⟩
           case isFalse =>
@@ -113,5 +113,6 @@ theorem heapPushRetainsHeapValues {α : Type u} {n: Nat} (le : α → α → Boo
           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
-            rw[contains_iff_index_exists _ _ this]
-            exists ⟨index.val - o - 1, by omega⟩
+            rw[contains_iff_index_exists _ _]
+            have : index.val - o - 1 < p := by omega
+            exists ⟨index.val - o - 1, this⟩
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index cf0774f..d68aedc 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -428,8 +428,7 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n
 := by
   simp only [ne_eq]
   intro h₁
-  have h₂ : n > 0 := by omega
-  rw[contains_iff_index_exists _ _ h₂]
+  rw[contains_iff_index_exists _ _]
   have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap index
   simp at h₃
   split at h₃
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
index 606b687..09ea532 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
@@ -150,10 +150,7 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo
           simp only[leftLen_unfold]
           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
+          exists solution
       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₆]
@@ -164,8 +161,6 @@ 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 _ _ h₆]
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index 1a44da1..48ba8ca 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -56,7 +56,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
         rw[contains_as_root_left_right _ _ h₄]
         right
         left
-        rewrite[contains_iff_index_exists']
+        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₂
@@ -74,7 +74,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
             rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
             right
             left
-            rw[←h₃, contains_iff_index_exists', left_unfold]
+            rw[←h₃, contains_iff_index_exists, left_unfold]
             exists ⟨j,h⟩
           case isFalse =>
             split
@@ -104,7 +104,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
               right
               left
               simp only [left_unfold]
-              rw[←h₃, contains_iff_index_exists']
+              rw[←h₃, contains_iff_index_exists]
               exists ⟨j, h⟩
         else
           -- index was in r
@@ -117,7 +117,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
             rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
             right
             right
-            rw[←h₃, contains_iff_index_exists', right_unfold]
+            rw[←h₃, contains_iff_index_exists, right_unfold]
             exists ⟨j-(oo+1), h₄⟩
           case isFalse =>
             split
@@ -128,7 +128,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
               right
               right
               simp only [right_unfold]
-              rw[←h₃, contains_iff_index_exists']
+              rw[←h₃, contains_iff_index_exists]
               exists ⟨j- (oo + 1), h₄⟩
             case isFalse =>
               --r.root gets moved up