diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-21 22:16:32 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-21 22:16:32 +0200 |
| commit | e3e52fe33b0c6704cc5471e32ac76ebe522b8e83 (patch) | |
| tree | 2df0666087701c713748d22949adb27f87dded8a | |
| parent | 6cb35171621051aec03906656ffa266f5947380d (diff) | |
Minor: Remove tactics mode for Nat.ble adapters
| -rw-r--r-- | BinaryHeap.lean | 19 |
1 files 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 |