From e3e52fe33b0c6704cc5471e32ac76ebe522b8e83 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Wed, 21 Aug 2024 22:16:32 +0200 Subject: Minor: Remove tactics mode for Nat.ble adapters --- BinaryHeap.lean | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/BinaryHeap.lean b/BinaryHeap.lean index 4a5bd26..774a3c3 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -61,15 +61,14 @@ instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ n > 0) where | (_+1), {tree, ..}, index => tree.get' index /--Helper for the common case of using natural numbers for sorting.-/ -theorem nat_ble_to_heap_le_total : total_le Nat.ble := by - unfold total_le - simp only [Nat.ble_eq] - exact Nat.le_total +theorem nat_ble_to_heap_le_total : total_le Nat.ble := + λa b ↦ Nat.ble_eq.substr $ Nat.ble_eq.substr (Nat.le_total a b) /--Helper for the common case of using natural numbers for sorting.-/ -theorem nat_ble_to_heap_transitive_le : transitive_le Nat.ble := by - unfold transitive_le - intros a b c - repeat rw[Nat.ble_eq] - rw[and_imp] - exact Nat.le_trans +theorem nat_ble_to_heap_transitive_le : transitive_le Nat.ble := + λ a b c ↦ + Nat.le_trans (n := a) (m := b) (k := c) + |> Nat.ble_eq.substr + |> Nat.ble_eq.substr + |> Nat.ble_eq.substr + |> and_imp.mpr -- cgit v1.2.3