Lean 4.23

7 files changed, 17 insertions, 19 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
index d8d1de4..e66512d 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
@@ -14,7 +14,7 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
   else
     simp only [h₁, ↓reduceDIte, ge_iff_le]
     if h₂ : index = (Internal.heapRemoveLastWithIndex heap).2.snd then
-      simp only [h₂, ↓reduceDIte]
+      simp only [h₂, ↓reduceIte]
       exact Eq.symm $ CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap
     else
       if h₃ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ index then
@@ -36,7 +36,7 @@ theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bo
   else
     simp only [h₂, ↓reduceDIte, ge_iff_le]
     if h₃ : removeIndex = (Internal.heapRemoveLastWithIndex heap).2.snd then
-      simp only [h₃, ↓reduceDIte]
+      simp only [h₃, ↓reduceIte]
       exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement _ _ (h₃.subst h₁.symm)
     else
       if h₄ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ removeIndex then
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index c3b77ad..d340578 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -11,7 +11,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N
   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]
+  simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Fin.castLE_succ]
   split
   case isTrue n_m_zero =>
     have h₁ : n = 0 := And.left $ Nat.add_eq_zero.mp n_m_zero.symm
@@ -199,7 +199,7 @@ intro h₁
 split at h₁
 rename_i o p v l r _ _ _
 simp only [Nat.add_eq, ne_eq] at h₂
-simp only [Nat.add_eq, h₂, ↓reduceDIte, decide_eq_true_eq, Fin.zero_eta, Fin.isValue,
+simp only [Nat.add_eq, h₂, ↓reduceDIte, Fin.zero_eta, Fin.isValue,
   Nat.succ_eq_add_one, Fin.castLE_succ, Nat.pred_eq_sub_one, gt_iff_lt] at h₁ ⊢
 if h₃ : p < o ∧ (p + 1).isPowerOfTwo then
   --removed left
@@ -218,8 +218,7 @@ if h₃ : p < o ∧ (p + 1).isPowerOfTwo then
         rewrite[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
         rewrite[leftLen_unfold]
         assumption
-      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 [Fin.coe_pred, Fin.isValue, ← lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
       simp only[leftLen_unfold]
       apply heapRemoveLastWithIndexRelationGt_Aux
       case h₁ => exact Nat.add_comm_right oo 1 p
@@ -261,7 +260,7 @@ else
     have h₅ : index.pred h₄ > o := by
       simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt]
       rewrite[Fin.lt_iff_val_lt_val] at h₁
-      simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁
+      simp only [Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁
       exact Nat.lt_of_add_right $ Nat.lt_pred_of_succ_lt h₁
     have h₆ : index > o :=  Nat.lt_of_add_left $ Nat.succ_lt_of_lt_pred h₅
     have h₇ : ↑index - o - 1 < pp + 1 :=
@@ -308,7 +307,7 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea
     split at h₁
     rename_i o p v l r _ _ _
     simp only [Nat.add_eq, ne_eq] at h₃
-    simp only [h₃, Nat.add_eq, Fin.zero_eta, Fin.isValue, decide_eq_true_eq, Nat.succ_eq_add_one,
+    simp only [h₃, Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one,
       Fin.castLE_succ, Nat.pred_eq_sub_one, reduceDIte] at h₁ ⊢
     if h₄ : p < o ∧ (p + 1).isPowerOfTwo then
       --removed left
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
index 5cbfbf5..893b554 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
@@ -52,7 +52,7 @@ private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : Compl
     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₂
+    simp only [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_iff] at h₂₂
@@ -172,7 +172,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl
         rw[Option.eq_some_iff_get_eq] at he₂ he₁
         match he₁, he₂ with
         | Exists.intro he₁ h₈, Exists.intro he₂ h₉ =>
-          simp[Fin.ext_iff, Option.map_get] at h₈ h₉
+          simp[Fin.ext_iff] at h₈ h₉
           rw[Nat.mod_eq_of_lt (by omega), h₇] at h₈
           rw[Nat.mod_eq_of_lt (by omega), h₆] at h₉
           rw[←h₈, ←h₉]
@@ -221,7 +221,6 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n
     case true =>
       simp only [h₃, ↓reduceIte, Option.some.injEq] at he₁
       subst index
-      simp[Fin.ofNat] at h₂
       rw[←Fin.zero_eta, ←get_zero_eq_root, root_unfold] at h₂
       subst v
       assumption
@@ -247,7 +246,7 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n
         exact h₉
       case some lindex =>
         rw[h₄, Option.some_or, Option.some_inj] at he₁
-        simp only [Option.map_map, Option.map_eq_some_iff, Function.comp_apply] at h₄
+        simp only [Option.map_eq_some_iff] at h₄
         subst lindex
         have h₅ : (Internal.indexOfAux l pred 1).isSome := Option.isSome_iff_exists.mpr (Exists.imp (λx ↦ And.left) h₄)
         have h₆ := indexOfSomeImpPredTrueAux2 _ 0 h₅
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean
index 4320473..146595f 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean
@@ -48,11 +48,11 @@ theorem heapPushRootSameOrElem (elem : α) (heap : CompleteTree α o) (lt : α �
   rename_i n m v l r _ _ _
   split -- if h : m < n ∧ (n + 1).isPowerOfTwo then
   case h_2.isTrue h =>
-    cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, root]
+    cases (lt elem v) <;> simp[root]
   case h_2.isFalse h =>
     rw[rootSeesThroughCast n (m+1) (Nat.add_comm_right _ _ _) (Nat.succ_pos _) (Nat.succ_pos _)]
     cases (lt elem v)
-     <;> simp[instDecidableEqBool, Bool.decEq, root]
+     <;> simp[root]
 
 theorem heapPushEmptyElem (elem : α) (heap : CompleteTree α o) (lt : α → α → Bool) (h₂ : ¬0 < o) : (root (heap.heapPush lt elem) (Nat.succ_pos o) = elem) :=
   have : o = 0 := Nat.eq_zero_of_le_zero $ (Nat.not_lt_eq 0 o).mp h₂
@@ -113,7 +113,7 @@ theorem heapPushIsHeap {α : Type u} {elem : α} {heap : CompleteTree α o} {le
     case' isTrue =>
       have h := heapPushIsHeapAux le n m v elem l r h₁ h₂ h₃
     case' isFalse =>
-      apply HeapPredicate.seesThroughCast <;> try simp +arith[h₂] --gets rid of annoying cast.
+      apply HeapPredicate.seesThroughCast <;> try simp +arith --gets rid of annoying cast.
       have h := heapPushIsHeapAux le m n v elem r l (And.intro h₁.right.left $ And.intro h₁.left $ And.intro h₁.right.right.right h₁.right.right.left) h₂ h₃
     all_goals
       unfold HeapPredicate
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
index 3d8f65a..e2236f7 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
@@ -54,7 +54,7 @@ private theorem castZeroHeap (n m : Nat) (heap : CompleteTree α 0) (h₁ : 0=n+
     cases n
     case succ => contradiction
     case zero =>
-      simp[h₁, h₂]
+      simp[h₂]
 
 -- If there is only one element left, the result is a leaf.
 private theorem heapRemoveLastAuxLeaf
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
index 685a726..f0194ec 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
@@ -33,10 +33,10 @@ where
       unfold heapUpdateRoot
       split
       rename_i o p v l r h₆ h₇ h₈ h₂
-      cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, Nat.add_one_ne_zero, root_unfold, h₄, reflexive_le]
+      cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, root_unfold, h₄, reflexive_le]
       <;> unfold HeapPredicate at h₁
       <;> have h₁₀ : le value $ l.root (by omega) := h₅ value v (l.root _) ⟨h₃, h₁.right.right.left⟩
-      simp only [↓reduceIte, Nat.add_zero, h₁₀, root_unfold, h₄, reflexive_le]
+      simp only [↓reduceIte, h₁₀, root_unfold, h₄, reflexive_le]
       have h₁₁ : le value $ r.root (by omega) := h₅ value v (r.root _) ⟨h₃, h₁.right.right.right⟩
       simp only [↓reduceIte, h₁₀, h₁₁, and_self, root_unfold, h₄, reflexive_le]
     case isFalse =>
diff --git a/lean-toolchain b/lean-toolchain
index 893a7f3..f434439 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.21.0
+leanprover/lean4:4.23.0