From 79f078a13a931b7f90871cc8df8ded85dc4b6a38 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Wed, 15 Jan 2025 23:53:49 +0100 Subject: Minor, readability --- BinaryHeap/CompleteTree/HeapOperations.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index a8ac1be..5ddccd5 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -65,7 +65,14 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : match subtree_complete with | .inl h₂ => absurd h₂ h₁ | .inr h₂ => power_of_two_mul_two_lt h₂ max_height_difference h₁ - let result := branch a (left.heapPush le elem) right (Nat.le_succ_of_le p) still_in_range (Or.inr right_is_power_of_two) + let result := + branch + a + (left.heapPush le elem) + right + (Nat.le_succ_of_le p) + still_in_range + (Or.inr right_is_power_of_two) have letMeSpellItOutForYou : n + 1 + m + 1 = n + m + 1 + 1 := (Nat.add_assoc n 1 m).subst (motive := λx↦n+1+m+1=x+1) rfl |> (Nat.add_comm 1 m).subst (motive := λx↦n+1+m+1=n+(x)+1) -- cgit v1.2.3