Lean 4.18

12 files changed, 53 insertions, 53 deletions

diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean
index 1b23bbf..e922a32 100644
--- a/BinaryHeap/Aux.lean
+++ b/BinaryHeap/Aux.lean
@@ -42,7 +42,7 @@ def pushList {α : Type u} {n : Nat} {le : α → α → Bool} (heap : BinaryHea
   match l with
   | [] => heap
   | a :: as =>
-    have : n + 1 + as.length = n + (a :: as).length := by simp_arith[List.length_cons a as]
+    have : n + 1 + as.length = n + (a :: as).length := by simp +arith[List.length_cons a as]
     this▸pushList (heap.push a) as
 
 private def ofForInAux [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : (h : Nat) ×' BinaryHeap α le h := Id.run do
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index b8d94e5..7379638 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -24,7 +24,7 @@ theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fi
       omega
       apply Nat.sub_lt_right_of_lt_add
       omega
-      have : p+1+o = (o.add p).succ := by simp_arith
+      have : p+1+o = (o.add p).succ := (Nat.add_assoc o p 1).substr $ Nat.add_comm (p +1) o
       rw[this]
       assumption
     tree.get index = (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩
@@ -45,7 +45,7 @@ theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r
     omega
     apply Nat.sub_lt_right_of_lt_add
     omega
-    have : m + 1 + n = n + m + 1 := by simp_arith
+    have : m + 1 + n = n + m + 1 := (Nat.add_assoc m n 1).substr $ Nat.add_comm (m +1 ) n
     rw[this]
     assumption
   (branch v l r m_le_n max_height_diff subtree_complete).get index = r.get ⟨index.val - n - 1, h₂⟩
@@ -93,7 +93,7 @@ theorem get_unfold {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : F
         omega
         apply Nat.sub_lt_right_of_lt_add
         omega
-        have : p+1+o = (o.add p).succ := by simp_arith
+        have : p+1+o = (o.add p).succ := (Nat.add_assoc o p 1).substr $ Nat.add_comm (p +1) o
         rw[this]
         assumption
       (tree.right h₁).get ⟨index.val - (tree.leftLen h₁) - 1, h₃⟩
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index ce9c3e2..8222879 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -31,10 +31,10 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N
     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 leaf => simp +ground 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]
+        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]
@@ -76,7 +76,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameTree {α : Type u} {n
       simp only
       cases p
       case zero =>
-        simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂
+        simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂
         simp only [Nat.add_zero] at h₁
         exact absurd h₂.symm h₁
       case succ pp =>
@@ -111,7 +111,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameElement {α : Type u}
       simp only
       cases p
       case zero =>
-        simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂
+        simp +ground only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂
         simp only [Nat.add_zero] at h₁
         exact absurd h₂.symm h₁
       case succ pp =>
@@ -258,7 +258,7 @@ else
   simp only [h₃, ↓reduceDIte, Fin.isValue] at h₁ ⊢
   cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢
   case zero =>
-    simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃
+    simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃
     subst o
     contradiction
   case succ pp _ _ _ _ =>
@@ -348,7 +348,7 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea
       simp only [h₄, ↓reduceDIte, Fin.isValue] at h₁ ⊢
       cases p
       case zero =>
-        simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄
+        simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₄
         subst o
         contradiction
       case succ pp _ _ _ _ =>
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index fe64a72..6193643 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -94,7 +94,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
                 right
                 left
                 rw[←h₃, left_unfold]
-                have : oo + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination
+                have : oo + 1 < oo + 1 + pp + 1 + 1 := by simp +arith --termination
                 apply heapUpdateRootOnlyUpdatesRoot
                 apply Fin.val_ne_iff.mp
                 exact Nat.succ_ne_zero _
@@ -147,7 +147,7 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
                 right
                 right
                 rw[←h₃, right_unfold]
-                have : pp + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination
+                have : pp + 1 < oo + 1 + pp + 1 + 1 := by simp +arith --termination
                 apply heapUpdateRootOnlyUpdatesRoot
                 apply Fin.ne_of_val_ne
                 simp only [ne_eq, Nat.add_one_ne_zero, not_false_eq_true]
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
index 0d69ebc..e913a59 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
@@ -118,7 +118,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl
   case h_2 o p v l r _ _ _ =>
     split
     case isTrue =>
-      have : currentIndex < o + p + 1 + currentIndex := by simp_arith
+      have : currentIndex < o + p + 1 + currentIndex := by simp +arith
       simp only [Nat.add_eq, Nat.succ_eq_add_one, Option.get_some, Fin.val_ofNat', this,
         Nat.mod_eq_of_lt, Nat.add_zero, Nat.zero_lt_succ, Nat.zero_add]
     case isFalse =>
@@ -175,7 +175,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl
           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₉]
-          simp_arith[o1, o2]
+          simp +arith[o1, o2]
 
 
 private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : CompleteTree α p) (pred : α → Bool) {o : Nat} (index : Fin ((o+p)+1)) (h₂ : (Internal.indexOfAux r pred 0).isSome) : ∀(a : Fin (p + (o + 1))), (Internal.indexOfAux r pred (o + 1) = some a ∧ Fin.ofNat' (o+p+1) ↑a = index) → (Internal.indexOfAux r pred 0).get h₂ + o + 1 = index.val := by
@@ -187,7 +187,7 @@ private theorem indexOfSomeImpPredTrueAuxR {α : Type u} {p : Nat} (r : Complete
     exact this.subst (motive := λx↦x=index.val) h₄
   rw[←this]
   have := indexOfAuxAddsCurrentIndex r pred (o+1) (indexOfSomeImpPredTrueAux2 0 _ h₂) h₂
-  simp_arith at this
+  have := (Nat.add_assoc _ o 1).substr (p := λx ↦ ((Internal.indexOfAux r pred (o + 1)).get _).val = x) this
   rw[←this]
   simp only [h₃, Option.get_some]
 
@@ -201,7 +201,6 @@ private theorem indexOfSomeImpPredTrueAuxL {α : Type u} {o : Nat} (l : Complete
     exact this.subst (motive := λx↦x=index.val) h₄
   rw[←this]
   have := indexOfAuxAddsCurrentIndex l pred 1 (indexOfSomeImpPredTrueAux2 0 _ h₂) h₂
-  simp_arith at this
   rw[←this]
   simp only [h₃, Option.get_some]
 
diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean
index e2b0019..b5d8f01 100644
--- a/BinaryHeap/CompleteTree/HeapOperations.lean
+++ b/BinaryHeap/CompleteTree/HeapOperations.lean
@@ -95,7 +95,7 @@ private theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo)
     have h₈ : n ≠ 0 := Ne.symm $ Nat.ne_of_lt h₇
     have h₉ : (n+1).isEven := (Nat.isPowerOfTwo_even_or_one h₁).resolve_left
       $ if h : n+1=1 then absurd (Nat.succ.inj h) h₈ else h
-    have h₉ : n.isOdd := Nat.pred_even_odd h₉ (by simp_arith[h₇])
+    have h₉ : n.isOdd := Nat.pred_even_odd h₉ (Nat.succ_pos n)
     have h₁₀ : ¬n.isOdd := Nat.even_not_odd_even.mp $ Nat.mul_2_is_even h₆
     absurd h₉ h₁₀
   else
@@ -121,7 +121,7 @@ private theorem stillInRange {n m : Nat} (r : ¬(m < n ∧ ((m+1).nextPowerOfTwo
   | inl h₁ => have m_eq_n : m = n := Nat.le_antisymm m_le_n (Nat.not_lt.mp h₁)
               have m_lt_2_m : m < 2 * m := (Nat.one_mul m).subst (motive := λ x ↦ x < 2 * m) $ Nat.mul_lt_mul_of_pos_right Nat.one_lt_two m_gt_0
               exact m_eq_n.subst (motive := λx ↦ x < 2 * m) m_lt_2_m
-  | inr h₁ => simp (config := { zetaDelta := true }) only [← Nat.power_of_two_iff_next_power_eq, decide_eq_true_eq] at h₁
+  | inr h₁ => simp +zetaDelta only [← Nat.power_of_two_iff_next_power_eq, decide_eq_true_eq] at h₁
               apply power_of_two_mul_two_le <;> assumption
 
 /--
@@ -155,7 +155,7 @@ protected def Internal.heapRemoveLastAux
           have s : m ≤ l := Nat.le_of_lt_succ r.left
           have rightIsFull : (m+1).isPowerOfTwo := (Nat.power_of_two_iff_next_power_eq (m+1)).mpr $ decide_eq_true_eq.mp r.right
           have l_lt_2_m_succ : l < 2 * (m+1) := Nat.lt_of_succ_lt max_height_difference
-          let res := auxl res (by simp_arith)
+          let res := auxl res (Nat.lt_of_le_of_lt (Nat.le_add_right (l+1) m) (Nat.lt_succ_self (l+1+m)))
           (q▸CompleteTree.branch a newLeft right s l_lt_2_m_succ (Or.inr rightIsFull), res)
       else
         --remove right
@@ -167,7 +167,7 @@ protected def Internal.heapRemoveLastAux
             absurd ⟨hn, hr⟩ r
           | mm+1 => Nat.succ_pos mm
         let l := m.pred
-        have h₂ : l.succ = m := Nat.succ_pred $ Nat.not_eq_zero_of_lt m_gt_0
+        have h₂ : l.succ = m := Nat.succ_pred $ Nat.ne_zero_of_lt m_gt_0
         let ((newRight : CompleteTree α l), res) := Internal.heapRemoveLastAux (h₂▸right : CompleteTree α l.succ) aux0 auxl auxr
         have leftIsFull : (n+1).isPowerOfTwo := removeRightLeftIsFull r m_le_n subtree_complete
         have still_in_range : n < 2 * (l+1) := h₂.substr (p := λx ↦ n < 2 * x) $ stillInRange r m_le_n m_gt_0 leftIsFull max_height_difference
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean
index 1ce9e56..52cba4c 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPush.lean
@@ -13,8 +13,8 @@ private theorem rootSeesThroughCast
   case zero => simp
   case succ o ho =>
     have h₄ := ho (n+1)
-    have h₅ : n + 1 + 1 + o = n + 1 + (Nat.succ o) := by simp_arith
-    have h₆ : n + 1 + o + 1 = n + (Nat.succ o + 1) := by simp_arith
+    have h₅ : n + 1 + 1 + o = n + 1 + (Nat.succ o) := Nat.add_right_comm (n+1) 1 o
+    have h₆ : n + 1 + o + 1 = n + (Nat.succ o + 1) := (Nat.add_comm 1 o).subst (motive := λx ↦ n + 1 + o + 1 = n + (x + 1)) (Nat.add_assoc n 1 (o+1))
     rewrite[h₅, h₆] at h₄
     revert heap h₁ h₂ h₃
     assumption
@@ -32,9 +32,10 @@ private theorem HeapPredicate.seesThroughCast
   case zero => simp[h₄]
   case succ o ho =>
     have h₅ := ho (n+1)
-    have h₆ : n+1+1+o+1 = n+1+(Nat.succ o)+1 := by simp_arith
+    have h₆ : n+1+1+o+1 = n+1+(Nat.succ o)+1 :=
+      congrArg Nat.succ $ (Nat.add_comm 1 o).subst (motive := λx ↦ n+1+1+o = n + 1 + x) (Nat.add_assoc (n+1) 1 o)
     rw[h₆] at h₅
-    have h₆ : n + 1 + o + 1 + 1 = n + (Nat.succ o + 1 + 1) := by simp_arith
+    have h₆ : n + 1 + o + 1 + 1 = n + (Nat.succ o + 1 + 1) := (Nat.add_comm 1 o).subst (motive := λx ↦ n + 1 + o + 1 + 1 = n + (x + 1 + 1)) (Nat.add_assoc n 1 (o + 1 + 1))
     rewrite[h₆] at h₅
     revert heap h₁ h₂ h₃
     assumption
@@ -49,7 +50,7 @@ theorem heapPushRootSameOrElem (elem : α) (heap : CompleteTree α o) (lt : α �
   case h_2.isTrue h =>
     cases (lt elem v) <;> simp[instDecidableEqBool, Bool.decEq, root]
   case h_2.isFalse h =>
-    rw[rootSeesThroughCast n (m+1) (by simp_arith) (by simp_arith) (by simp_arith)]
+    rw[rootSeesThroughCast n (m+1) (Nat.add_comm_right _ _ _) (Nat.succ_pos _) (Nat.succ_pos _)]
     cases (lt elem v)
      <;> simp[instDecidableEqBool, Bool.decEq, root]
 
@@ -112,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[h₂] --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 29e9837..8eec6df 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveLast.lean
@@ -16,8 +16,8 @@ private theorem rootSeesThroughCast2
   case zero => simp
   case succ mm mh =>
     have h₄ := mh (n+1)
-    have h₅ : n + 1 + mm + 1 = n + Nat.succ mm + 1 := by simp_arith
-    have h₆ : n + 1 + 1 + mm = n + 1 + Nat.succ mm := by simp_arith
+    have h₅ : n + 1 + mm + 1 = n + Nat.succ mm + 1 := congrArg Nat.succ $ (Nat.add_comm 1 mm).subst (motive := λx ↦ _ = n + (x)) (Nat.add_assoc n 1 mm)
+    have h₆ : n + 1 + 1 + mm = n + 1 + Nat.succ mm := Nat.add_comm_right _ _ _
     rw[h₅, h₆] at h₄
     revert heap h₁ h₂ h₃
     assumption
@@ -35,9 +35,9 @@ private theorem HeapPredicate.seesThroughCast2
   case zero => simp[h₄]
   case succ o ho =>
     have h₅ := ho (n+1)
-    have h₆ : n+1+o+1 = n+(Nat.succ o)+1 := by simp_arith
+    have h₆ : n+1+o+1 = n+(Nat.succ o)+1 := congrArg Nat.succ $ Nat.add_comm_right _ _ _
     rw[h₆] at h₅
-    have h₆ : n + 1 + 1 + o = n + 1 + Nat.succ o := by simp_arith
+    have h₆ : n + 1 + 1 + o = n + 1 + Nat.succ o := Nat.add_comm_right (n+1) 1 o
     rewrite[h₆] at h₅
     revert heap h₁ h₂ h₃
     assumption
@@ -82,7 +82,7 @@ protected theorem heapRemoveLastAuxLeavesRoot
   unfold CompleteTree.Internal.heapRemoveLastAux
   split
   rename_i o p v l r _ _ _
-  have h₃ : (0 ≠ o + p) := Ne.symm $ Nat.not_eq_zero_of_lt h₁
+  have h₃ : (0 ≠ o + p) := Ne.symm $ Nat.ne_zero_of_lt h₁
   simp[h₃]
   exact
     if h₄ : p < o ∧ Nat.nextPowerOfTwo (p + 1) = p + 1 then by
@@ -91,16 +91,16 @@ protected theorem heapRemoveLastAuxLeavesRoot
       case zero => exact absurd h₄.left $ Nat.not_lt_zero p
       case succ oo _ _ _ =>
         simp -- redundant, but makes goal easier to read
-        rw[rootSeesThroughCast2 oo p _ (by simp_arith) _]
+        rw[rootSeesThroughCast2 oo p _ (Nat.succ_pos _) _]
         apply root_unfold
     else by
       simp[h₄]
       cases p
       case zero =>
-        simp_arith at h₁ -- basically o ≠ 0
-        simp_arith (config := {ground := true})[h₁] at h₄ -- the second term in h₄ is decidable and True. What remains is ¬(0 < o), or o = 0
+        have h₁ : 0 < o := (Nat.add_zero o).subst h₁
+        simp +ground[h₁] at h₄ -- the second term in h₄ is decidable and True. What remains is ¬(0 < o), or o = 0
       case succ pp hp =>
-        simp_arith
+        simp +arith
         apply root_unfold
 
 private theorem heapRemoveLastAuxIsHeap
@@ -128,7 +128,7 @@ private theorem heapRemoveLastAuxIsHeap
             exact absurd h₅.left $ Nat.not_lt_zero m
           case succ ll h₆ h₇ h₈  =>
             simp only
-            apply HeapPredicate.seesThroughCast2 <;> try simp_arith
+            apply HeapPredicate.seesThroughCast2; exact Nat.lt_add_right m (Nat.succ_pos _); exact Nat.succ_pos _
             cases ll
             case a.zero => -- if ll is zero, then (heapRemoveLast l).snd is a leaf.
               have h₆ := heapRemoveLastAuxLeaf l aux0 auxl auxr
@@ -149,7 +149,7 @@ private theorem heapRemoveLastAuxIsHeap
           cases m
           case zero =>
             simp only [Nat.add_zero] at h₄ -- n ≠ 0
-            simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq, Ne.symm h₄] at h₅ -- the second term in h₅ is decidable and True. What remains is ¬(0 < n), or n = 0
+            simp +ground only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq, Ne.symm h₄] at h₅ -- the second term in h₅ is decidable and True. What remains is ¬(0 < n), or n = 0
           case succ mm h₆ h₇ h₈ =>
             unfold HeapPredicate at *
             simp only [h₁, heapRemoveLastAuxIsHeap aux0 auxl auxr h₁.right.left h₂ h₃, true_and]
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
index c12f76f..86d2499 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
@@ -13,7 +13,7 @@ private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat}
     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
+    cases h₉ : le v value <;> simp only
     case false => rw[root_unfold] at h₃; exact absurd h₃ ((Bool.not_eq_true (le v value)).substr h₉)
     case true =>
       rw[root_unfold]
@@ -39,7 +39,7 @@ private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat}
     split
     rename_i o p v l r h₆ h₇ h₈ index h₂ hi
     cases le v value
-    <;> simp (config := { ground := true }) only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢
+    <;> simp +ground only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢
     <;> split
     <;> unfold HeapPredicate.leOrLeaf
     <;> simp only [reduceIte, root_unfold, h₃, h₄, reflexive_le]
@@ -53,7 +53,7 @@ theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (in
   case isFalse h₅ =>
     split
     rename_i o p v l r h₆ h₇ h₈ index h₁ h₅
-    cases h₁₀ : le v value <;> simp (config := {ground := true}) -- this could probably be solved without this split, but readability...
+    cases h₁₀ : le v value <;> simp +ground -- this could probably be solved without this split, but readability...
     <;> split
     <;> rename_i h -- h is the same name as used in the function
     <;> unfold HeapPredicate at h₂ ⊢
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
index d712b8e..d3e7017 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateRoot.lean
@@ -34,7 +34,7 @@ private theorem heapUpdateRootPossibleRootValuesAuxR {α : Type u} (heap : Compl
   | (o+p+1), .branch v l r h₂ h₃ h₄ => by
     simp[rightLen, length]
     cases p
-    case zero => simp_arith at h₁; simp at h₃; exact absurd h₁ (Nat.not_le_of_gt h₃)
+    case zero => exact absurd (Nat.le_of_lt_succ 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 (h₁.substr (p := λx ↦ 0<x) (Nat.lt_succ_self 0)) le value).fst.root (h₁.substr (Nat.lt_succ_self 0)) = value := by
@@ -114,8 +114,8 @@ protected theorem heapUpdateRootIsHeapLeRootAux {α : Type u} (le : α → α �
       case h_2 o p v l r h₇ h₈ h₉ =>
         have h₁₁ : p = 0 := by
          simp at h₅
-         cases o; simp only [Nat.le_zero_eq] at h₇; exact h₇; simp_arith[Nat.add_eq_zero] at h₅; exact h₅.right
-        have h₁₀ : o = 1 := by simp_arith[h₁₁] at h₅; assumption
+         cases o; simp only [Nat.le_zero_eq] at h₇; exact h₇; simp +arith only [Nat.add_eq_zero_iff] at h₅; exact h₅.left
+        have h₁₀ : o = 1 := by simp only [h₁₁, Nat.add_zero, Nat.reduceEqDiff] at h₅; assumption
         simp only
         rw[h₆]
         have h₁₂ := h₁.right.right.left
@@ -186,7 +186,7 @@ theorem heapUpdateRootIsHeap {α : Type u} {n: Nat} (le : α → α → Bool) (v
         case false =>
           rw[heapUpdateRootReturnsRoot]
           have h₁₂ : le (l.root (Nat.zero_lt_of_ne_zero h₁₀)) value := by simp[h₉, h₄, not_le_imp_le]
-          have h₁₃ : o = 1 := Nat.le_antisymm (by simp_arith[h₁₁] at h₈; exact h₈) (Nat.succ_le_of_lt (Nat.zero_lt_of_ne_zero h₁₀))
+          have h₁₃ : o = 1 := Nat.le_antisymm (by simp[h₁₁] at h₈; exact Nat.le_of_lt_succ h₈) (Nat.succ_le_of_lt (Nat.zero_lt_of_ne_zero h₁₀))
           unfold HeapPredicate at *
           simp only [h₂, true_and] --closes one sub-goal
           apply And.intro <;> try apply And.intro
diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean
index f9b730c..56b3203 100644
--- a/BinaryHeap/CompleteTree/NatLemmas.lean
+++ b/BinaryHeap/CompleteTree/NatLemmas.lean
@@ -2,9 +2,9 @@ namespace Nat
 
 theorem smaller_smaller_exp {n m o : Nat} (p : o ^ n < o ^ m) (q : o > 0) : n < m :=
   if h₁ : m ≤ n  then
-    by have h₂ := Nat.pow_le_pow_of_le_right (q) h₁
+    by have h₂ := Nat.pow_le_pow_right (q) h₁
        have h₃ := Nat.lt_of_le_of_lt h₂ p
-       simp_arith at h₃
+       simp at h₃
   else
     by rewrite[Nat.not_ge_eq] at h₁
        trivial
@@ -17,11 +17,11 @@ private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat)
   rewrite[←Nat.pow_succ 2 l]
   rewrite[h₄]
   have h₆ : 2 > 0 := by decide
-  apply (Nat.pow_le_pow_of_le_right h₆)
+  apply (Nat.pow_le_pow_right h₆)
   rewrite [h₅] at h₃
   rewrite [h₄] at h₃
   have h₃ := smaller_smaller_exp h₃
-  simp_arith at h₃
+  simp at h₃
   assumption
 
 private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by
@@ -70,7 +70,7 @@ theorem mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n).
       cases n with
       | zero => contradiction
       | succ m => cases k with
-        | zero => simp_arith at h₄
+        | zero => simp +arith at h₄
         | succ l => rewrite[Nat.pow_succ 2 l] at h₄
                     rewrite[Nat.mul_comm (2^l) 2] at h₄
                     have h₄ := Nat.eq_of_mul_eq_mul_left (by decide : 0<2) h₄
@@ -91,7 +91,7 @@ end
 theorem mul_2_is_even {n m : Nat} (h₁ : n = 2 * m) : Nat.isEven n := by
   cases m with
   | zero => simp[Nat.isEven, h₁]
-  | succ o => simp_arith at h₁
+  | succ o => simp +arith at h₁
               simp[Nat.isEven, Nat.isOdd, h₁]
               exact Nat.mul_2_is_even (rfl)
 
@@ -99,7 +99,7 @@ theorem isPowerOfTwo_even_or_one {n : Nat} (h₁ : n.isPowerOfTwo) : (n = 1 ∨
   simp[Nat.isPowerOfTwo] at h₁
   let ⟨k,h₂⟩ := h₁
   cases k with
-  | zero => simp_arith[h₂]
+  | zero => simp[h₂]
   | succ l => rewrite[Nat.pow_succ] at h₂
               rewrite[Nat.mul_comm (2^l) 2] at h₂
               exact Or.inr $ Nat.mul_2_is_even h₂
@@ -157,7 +157,7 @@ theorem add_eq_zero {a b : Nat} :  a + b = 0 ↔ a = 0 ∧ b = 0 := by
   case mpr =>
     simp[h₁]
   case mp =>
-    cases a <;> simp_arith at *; assumption
+    cases a <;> simp at *; assumption
 
 -- Yes, this is trivial. Still, I needed it so often, that it deserves its own lemma.
 theorem add_comm_right (a b c : Nat) : a + b + c = a + c + b :=
diff --git a/lean-toolchain b/lean-toolchain
index db29c97..9f78e65 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.17.0
+leanprover/lean4:4.18.0