From c6e82da892f8ee79881a8dafa3c01f7c7a682ae5 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Mon, 13 Jan 2025 23:32:16 +0100
Subject: Minor

---
 BinaryHeap/CompleteTree/HeapOperations.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean
index e70ff77..6a8f190 100644
--- a/BinaryHeap/CompleteTree/HeapOperations.lean
+++ b/BinaryHeap/CompleteTree/HeapOperations.lean
@@ -40,8 +40,9 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) :
                              simp_arith[p]
       have right_is_power_of_two : (m+1).isPowerOfTwo :=
         if s : n = m then
-          s.subst (motive := λx ↦ (x+1).isPowerOfTwo ∨ (m+1).isPowerOfTwo) subtree_complete
-          |> (or_self _).mp
+          match subtree_complete with
+          | .inl h₂ => (congrArg Nat.succ s).subst h₂
+          | .inr h₂ => h₂
         else if h₁ : leftIsFull then by
           rewrite[Decidable.not_and_iff_or_not (p := m<n) (q := leftIsFull)] at r
           cases r
-- 
cgit v1.2.3