Lean 4.20.1

5 files changed, 16 insertions, 23 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index 7379638..aad82c5 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -9,7 +9,7 @@ theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h�
   | nn+1, ⟨j+1,h₄⟩, _ => by
     subst h₂
     simp only [Nat.succ_eq_add_one, Fin.zero_eta, heq_eq_eq, Fin.ext_iff, Fin.val_zero,
-      Nat.self_eq_add_left, Nat.add_one_ne_zero] at h₃
+      Nat.right_eq_add, Nat.add_one_ne_zero] at h₃
 
 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
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
index e913a59..5e11d8e 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/IndexOf.lean
@@ -21,13 +21,13 @@ private theorem Option.bind_some_eq_map {α β : Type u} (f : α → β) (a : Op
 
 private theorem Option.is_some_map {α : Type u} {β : Type v} {f : α → β} {a : Option α} : (Option.map f a).isSome ↔ a.isSome := by
   cases a
-  case none => simp only [Option.map_none', Option.isSome_none]
-  case some => simp only [Option.map_some', Option.isSome_some]
+  case none => simp only [Option.map_none, Option.isSome_none]
+  case some => simp only [Option.map_some, Option.isSome_some]
 
-private theorem Option.orElse_is_some {α : Type u} (a b : Option α) : (HOrElse.hOrElse a λ_ ↦ b).isSome = (a.isSome || b.isSome) := by
+private theorem Option.orElse_is_some {α : Type u} (a b : Option α) : (Option.orElse a (λ_↦b)).isSome = true ↔ a.isSome || b.isSome := by
   cases a
-  case none => simp only [Option.none_orElse, Option.isSome_none, Bool.false_or]
-  case some _ => simp only [Option.some_orElse, Option.isSome_some, Bool.true_or]
+  case none => simp only [Option.none_orElse, Option.isSome_none, Bool.false_or, imp_self]
+  case some _ => simp only [Option.some_orElse, Option.isSome_some, Bool.true_or, imp_self]
 
 private theorem Option.isSome_of_eq_some {α : Type u} {a : α} {o : Option α} : o = some a → o.isSome := by
   intro h₁
@@ -55,7 +55,7 @@ private theorem indexOfNoneImpPredFalseAux {α : Type u} {n : Nat} (tree : Compl
     simp only [Nat.add_zero, Nat.reduceAdd, 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'] at h₂₂
+    simp only [Option.map_eq_none_iff] at h₂₂
     if h₃ : index = ⟨0,h₁⟩ then
       subst index
       rw[←get_zero_eq_root, root_unfold]
@@ -99,7 +99,7 @@ private theorem indexOfSomeImpPredTrueAux2 {α : Type u} {p : Nat} {r : Complete
       simp only [Option.isSome_some, imp_self]
     case isFalse =>
       unfold Function.comp
-      simp only [Option.map_some']
+      simp only [Option.map_some]
       repeat rw[Option.bind_some_eq_map]
       simp only [Option.orElse_is_some, Bool.or_eq_true, Option.is_some_map]
       intro h₁
@@ -142,7 +142,7 @@ private theorem indexOfAuxAddsCurrentIndex {α : Type u} {n : Nat} (tree : Compl
         have hx₂ := Option.isSome_of_eq_some hx₂
         have hx₂ : (Internal.indexOfAux l pred _).isSome := Option.is_some_map.mp hx₂
         have hx₂ := indexOfSomeImpPredTrueAux2 _ off hx₂
-        have hx₁ := Option.map_eq_none.mp hx₁
+        have hx₁ := Option.map_eq_none_iff.mp hx₁
         have hx₁ := Option.not_isSome_iff_eq_none.mpr hx₁
         contradiction
       all_goals
@@ -227,11 +227,11 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n
     case false =>
       --unfold HOrElse.hOrElse instHOrElseOfOrElse at he₁
       unfold Function.comp at he₁
-      simp only [h₃, Bool.false_eq_true, ↓reduceIte, Option.map_some', Option.bind_some_eq_map] at he₁
+      simp only [h₃, Bool.false_eq_true, ↓reduceIte, Option.map_some, Option.bind_some_eq_map] at he₁
       cases h₄ : (Option.map (fun a => Fin.ofNat' (o+p+1) a.val) (Internal.indexOfAux l pred 1))
       case none =>
         rw[h₄, Option.none_orElse] at he₁
-        simp only [Option.map_map, Option.map_eq_some', Function.comp_apply] at he₁
+        simp only [Option.map_map, Option.map_eq_some_iff, Function.comp_apply] at he₁
         rw[Nat.zero_add] at he₁
         have h₅ : (Internal.indexOfAux r pred (o + 1)).isSome := Option.isSome_iff_exists.mpr (Exists.imp (λx ↦ And.left) he₁)
         have h₆ := indexOfSomeImpPredTrueAux2 _ 0 h₅
@@ -246,7 +246,7 @@ theorem indexOfSomeImpPredTrue {α : Type u} {n : Nat} (tree : CompleteTree α n
         exact h₉
       case some lindex =>
         rw[h₄, Option.some_orElse, Option.some_inj] at he₁
-        simp only [Option.map_map, Option.map_eq_some', Function.comp_apply] at h₄
+        simp only [Option.map_map, Option.map_eq_some_iff, Function.comp_apply] 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/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean
index 28115b0..2901b61 100644
--- a/BinaryHeap/CompleteTree/HeapOperations.lean
+++ b/BinaryHeap/CompleteTree/HeapOperations.lean
@@ -11,7 +11,7 @@ private theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h�
   if h₄ : n+1 > 2*m then
     absurd h₄ ((Nat.not_lt_eq (2*m) (n+1)).substr $ Nat.succ_le_of_lt h₂)
   else if h₅ : n+1 = 2*m then
-    have h₆ : (2*m).isPowerOfTwo := (Nat.mul_comm 2 m).substr $ Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₁
+    have h₆ : (2*m).isPowerOfTwo := (Nat.mul_comm 2 m).substr $ Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₁
     have h₇ : (n+1).isPowerOfTwo := h₅.substr h₆
     absurd h₇ h₃
   else
diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean
index 1050c17..b8b067a 100644
--- a/BinaryHeap/CompleteTree/NatLemmas.lean
+++ b/BinaryHeap/CompleteTree/NatLemmas.lean
@@ -27,7 +27,7 @@ private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat)
 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
   unfold Nat.nextPowerOfTwo.go
   split
-  case isTrue h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄)
+  case isTrue h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄)
   case isFalse h₄ => rewrite[Nat.not_lt_eq power n] at h₄
                      exact Nat.le_antisymm h₃ h₄
 termination_by n - power
@@ -57,7 +57,7 @@ theorem power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPow
 theorem mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n).isPowerOfTwo :=
   have h₁ : n.isPowerOfTwo → (2*n).isPowerOfTwo := by
     simp[Nat.mul_comm]
-    apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo
+    apply Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo
   have h₂ : (2*n).isPowerOfTwo → n.isPowerOfTwo :=
     if h₂ : n.nextPowerOfTwo = n then by
       simp[power_of_two_iff_next_power_eq,h₂]
@@ -152,13 +152,6 @@ theorem sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) : a -
   have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇
   Nat.lt_of_succ_le h₈
 
-theorem add_eq_zero {a b : Nat} :  a + b = 0 ↔ a = 0 ∧ b = 0 := by
-  constructor <;> intro h₁
-  case mpr =>
-    simp[h₁]
-  case mp =>
-    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 :=
   (rfl : a + b + c = a + b + c)
diff --git a/lean-toolchain b/lean-toolchain
index a0922e9..6c721df 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.19.0
+leanprover/lean4:4.20.1