From fe30e1dc0a0070452edce74331aa3df21a6b8f7c Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Tue, 7 Jan 2025 23:15:50 +0100 Subject: Lean 4.15 --- BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 4 ++-- BinaryHeap/CompleteTree/HeapOperations.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 2bdc382..ce9c3e2 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -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 (config := { ground := true }) 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 (config := { ground := true }) 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 => diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index 9151eb0..8e34599 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -33,7 +33,7 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : rewrite[s] simp[r] have difference_decreased := Nat.le_succ_of_le $ Nat.le_succ_of_le max_height_difference - let result := branch a left (right.heapPush le elem) (q) difference_decreased (by simp[(Nat.power_of_two_iff_next_power_eq (n+1)), r]) + let result := branch a left (right.heapPush le elem) (q) difference_decreased (Or.inl $ (Nat.power_of_two_iff_next_power_eq (n+1)).mpr r.right) result else have q : m ≤ n+1 := by apply (Nat.le_of_succ_le) diff --git a/lean-toolchain b/lean-toolchain index cb2924f..f1f4005 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.14 +leanprover/lean4:4.15.0 -- cgit v1.2.3