fix: style

Batteries/Data/BinaryHeap.lean

@@ -38,7 +38,7 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
 termination_by a.size - i
 
 @[simp] theorem size_heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
-  (heapifyDown lt a i).1.size = a.size := (heapifyDown lt a i).2
+    (heapifyDown lt a i).1.size = a.size := (heapifyDown lt a i).2
 
 /-- Core operation for binary heaps, expressed directly on arrays.
 Construct a heap from an unsorted array, by heapifying all the elements. -/
@@ -55,24 +55,24 @@ where
     ⟨a₂, h₂.trans a'.2⟩
 
 @[simp] theorem size_mkHeap (lt : α → α → Bool) (a : Array α) :
-  (mkHeap lt a).1.size = a.size := (mkHeap lt a).2
+    (mkHeap lt a).1.size = a.size := (mkHeap lt a).2
 
 /-- Core operation for binary heaps, expressed directly on arrays.
 Given an array which is a max-heap, push item `i` up to restore the max-heap property. -/
 def heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
     {a' : Array α // a'.size = a.size} :=
-if i0 : i.1 = 0 then ⟨a, rfl⟩ else
-  have : (i.1 - 1) / 2 < i := Nat.lt_of_le_of_lt (Nat.div_le_self ..) <|
-    Nat.sub_lt (Nat.pos_of_ne_zero i0) Nat.zero_lt_one
-  let j := ⟨(i.1 - 1) / 2, Nat.lt_trans this i.2⟩
-  if lt (a.get j) (a.get i) then
-    let a' := a.swap i j
-    let ⟨a₂, h₂⟩ := heapifyUp lt a' ⟨j.1, by rw [a.size_swap i j]; exact j.2⟩
-    ⟨a₂, h₂.trans (a.size_swap i j)⟩
-  else ⟨a, rfl⟩
+  if i0 : i.1 = 0 then ⟨a, rfl⟩ else
+    have : (i.1 - 1) / 2 < i := Nat.lt_of_le_of_lt (Nat.div_le_self ..) <|
+      Nat.sub_lt (Nat.pos_of_ne_zero i0) Nat.zero_lt_one
+    let j := ⟨(i.1 - 1) / 2, Nat.lt_trans this i.2⟩
+    if lt (a.get j) (a.get i) then
+      let a' := a.swap i j
+      let ⟨a₂, h₂⟩ := heapifyUp lt a' ⟨j.1, by rw [a.size_swap i j]; exact j.2⟩
+      ⟨a₂, h₂.trans (a.size_swap i j)⟩
+    else ⟨a, rfl⟩
 
 @[simp] theorem size_heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
-  (heapifyUp lt a i).1.size = a.size := (heapifyUp lt a i).2
+    (heapifyUp lt a i).1.size = a.size := (heapifyUp lt a i).2
 
 /-- `O(1)`. Build a new empty heap. -/
 def empty (lt) : BinaryHeap α lt := ⟨#[]⟩
@@ -84,25 +84,25 @@ instance (lt) : EmptyCollection (BinaryHeap α lt) := ⟨empty _⟩
 def singleton (lt) (x : α) : BinaryHeap α lt := ⟨#[x]⟩
 
 /-- `O(1)`. Get the number of elements in a `BinaryHeap`. -/
-def size {lt} (self : BinaryHeap α lt) : Nat := self.1.size
+def size (self : BinaryHeap α lt) : Nat := self.1.size
 
 /-- `O(1)`. Get an element in the heap by index. -/
-def get {lt} (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i
+def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i
 
 /-- `O(log n)`. Insert an element into a `BinaryHeap`, preserving the max-heap property. -/
-def insert {lt} (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where
+def insert (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where
   arr := let n := self.size;
     heapifyUp lt (self.1.push x) ⟨n, by rw [Array.size_push]; apply Nat.lt_succ_self⟩
 
-@[simp] theorem size_insert {lt} (self : BinaryHeap α lt) (x : α) :
-  (self.insert x).size = self.size + 1 := by
+@[simp] theorem size_insert (self : BinaryHeap α lt) (x : α) :
+    (self.insert x).size = self.size + 1 := by
   simp [insert, size, size_heapifyUp]
 
 /-- `O(1)`. Get the maximum element in a `BinaryHeap`. -/
-def max {lt} (self : BinaryHeap α lt) : Option α := self.1.get? 0
+def max (self : BinaryHeap α lt) : Option α := self.1.get? 0
 
 /-- Auxiliary for `popMax`. -/
-def popMaxAux {lt} (self : BinaryHeap α lt) : {a' : BinaryHeap α lt // a'.size = self.size - 1} :=
+def popMaxAux (self : BinaryHeap α lt) : {a' : BinaryHeap α lt // a'.size = self.size - 1} :=
   match e: self.1.size with
   | 0 => ⟨self, by simp [size, e]⟩
   | n+1 =>
@@ -117,20 +117,20 @@ def popMaxAux {lt} (self : BinaryHeap α lt) : {a' : BinaryHeap α lt // a'.size
 
 /-- `O(log n)`. Remove the maximum element from a `BinaryHeap`.
 Call `max` first to actually retrieve the maximum element. -/
-def popMax {lt} (self : BinaryHeap α lt) : BinaryHeap α lt := self.popMaxAux
+def popMax (self : BinaryHeap α lt) : BinaryHeap α lt := self.popMaxAux
 
-@[simp] theorem size_popMax {lt} (self : BinaryHeap α lt) :
-  self.popMax.size = self.size - 1 := self.popMaxAux.2
+@[simp] theorem size_popMax (self : BinaryHeap α lt) :
+    self.popMax.size = self.size - 1 := self.popMaxAux.2
 
 /-- `O(log n)`. Return and remove the maximum element from a `BinaryHeap`. -/
-def extractMax {lt} (self : BinaryHeap α lt) : Option α × BinaryHeap α lt :=
+def extractMax (self : BinaryHeap α lt) : Option α × BinaryHeap α lt :=
   (self.max, self.popMax)
 
-theorem size_pos_of_max {lt} {self : BinaryHeap α lt} (e : self.max = some x) : 0 < self.size :=
+theorem size_pos_of_max {self : BinaryHeap α lt} (e : self.max = some x) : 0 < self.size :=
   Decidable.of_not_not fun h : ¬ 0 < self.1.size => by simp [BinaryHeap.max, Array.get?, h] at e
 
 /-- `O(log n)`. Equivalent to `extractMax (self.insert x)`, except that extraction cannot fail. -/
-def insertExtractMax {lt} (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt :=
+def insertExtractMax (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt :=
   match e: self.max with
   | none => (x, self)
   | some m =>
@@ -140,19 +140,19 @@ def insertExtractMax {lt} (self : BinaryHeap α lt) (x : α) : α × BinaryHeap
     else (x, self)
 
 /-- `O(log n)`. Equivalent to `(self.max, self.popMax.insert x)`. -/
-def replaceMax {lt} (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α lt :=
+def replaceMax (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α lt :=
   match e: self.max with
   | none => (none, ⟨self.1.push x⟩)
   | some m =>
     let a := self.1.set ⟨0, size_pos_of_max e⟩ x
     (some m, ⟨heapifyDown lt a ⟨0, by simp only [Array.size_set, a]; exact size_pos_of_max e⟩⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/
-def decreaseKey {lt} (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
+def decreaseKey (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
   arr := heapifyDown lt (self.1.set i x) ⟨i, by rw [self.1.size_set]; exact i.2⟩
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `self.get i ≤ x`. -/
-def increaseKey {lt} (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
+def increaseKey (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
   arr := heapifyUp lt (self.1.set i x) ⟨i, by rw [self.1.size_set]; exact i.2⟩
 
 end Batteries.BinaryHeap