From 7df84f9a3e399587c65a149bf4247154d9b07cc7 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 20 Aug 2024 23:50:11 +0200
Subject: heapRemoveAtReturnsElementAt

---
 BinaryHeap/CompleteTree/AdditionalProofs.lean      |  1 +
 .../AdditionalProofs/HeapRemoveAt.lean             | 29 ++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean
index 3659fa4..4ab43f0 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean
@@ -3,3 +3,4 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapPop
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateAt
+import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveAt
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
new file mode 100644
index 0000000..ca4299f
--- /dev/null
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
@@ -0,0 +1,29 @@
+import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateAt
+import BinaryHeap.CompleteTree.AdditionalProofs.Get
+import BinaryHeap.CompleteTree.AdditionalProofs.HeapPop
+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
+  unfold heapRemoveAt
+  if h₁ : index = 0 then
+    simp only [h₁, ↓reduceDIte]
+    rw[get_eq_get', ←Fin.zero_eta, ←get_zero_eq_root]
+    exact heapPopReturnsRoot heap le
+  else
+    simp only [h₁, ↓reduceDIte, ge_iff_le]
+    if h₂ : index = (Internal.heapRemoveLastWithIndex heap).2.snd then
+      simp only [h₂, ↓reduceDIte]
+      exact Eq.symm $ CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap
+    else
+      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₄]
+        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 _ _ _ _
-- 
cgit v1.2.3