diff --git a/Batteries/Data/BinaryHeap.lean b/Batteries/Data/BinaryHeap.lean
index 753605b57c..a6c479f6b6 100644
--- a/Batteries/Data/BinaryHeap.lean
+++ b/Batteries/Data/BinaryHeap.lean
@@ -1,2 +1,4 @@
 module
 public import Batteries.Data.BinaryHeap.Basic
+public import Batteries.Data.BinaryHeap.Lemmas
+public import Batteries.Data.BinaryHeap.WF
diff --git a/Batteries/Data/BinaryHeap/Basic.lean b/Batteries/Data/BinaryHeap/Basic.lean
index 4a4040b907..e4ba84fae3 100644
--- a/Batteries/Data/BinaryHeap/Basic.lean
+++ b/Batteries/Data/BinaryHeap/Basic.lean
@@ -10,18 +10,21 @@ public section
 namespace Batteries
 
 /-- A max-heap data structure. -/
-structure BinaryHeap (α) (lt : α → α → Bool) where
+structure BinaryHeap (α: Type w) where
   /-- `O(1)`. Get data array for a `BinaryHeap`. -/
   arr : Array α
 
 namespace BinaryHeap
+variable {α : Type w}
 
-private def maxChild (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) : Option (Fin sz) :=
+
+/-- Given a node, return the index of its larger child, if it exists -/
+def maxChild [Ord α] (a : Vector α sz) (i : Fin sz) : Option (Fin sz) :=
   let left := 2 * i.1 + 1
   let right := left + 1
   if hleft : left < sz then
     if hright : right < sz then
-      if lt a[left] a[right] then
+      if compare a[left] a[right] |>.isLT then
         some ⟨right, hright⟩
       else
         some ⟨left, hleft⟩
@@ -31,151 +34,153 @@ private def maxChild (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) :
 
 /-- Core operation for binary heaps, expressed directly on arrays.
 Given an array which is a max-heap, push item `i` down to restore the max-heap property. -/
-def heapifyDown (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) :
+@[expose]
+def heapifyDown [Ord α] (a : Vector α sz) (i : Fin sz) :
     Vector α sz :=
-  match h : maxChild lt a i with
+  match h : maxChild a i with
   | none => a
   | some j =>
-    have : i < j := by
-      cases i; cases j
-      simp only [maxChild] at h
-      split at h
-      · split at h
-        · split at h <;> (cases h; simp +arith)
-        · cases h; simp +arith
-      · contradiction
-    if lt a[i] a[j] then
-      heapifyDown lt (a.swap i j) j
+    have : i < j := by grind [maxChild]
+    if compare a[i] a[j] |>.isLT then
+      heapifyDown (a.swap i j) j
     else a
 termination_by sz - i
 
 /-- Core operation for binary heaps, expressed directly on arrays.
 Construct a heap from an unsorted array, by heapifying all the elements. -/
-def mkHeap (lt : α → α → Bool) (a : Vector α sz) : Vector α sz :=
+@[inline]
+def mkHeap [Ord α] (a : Vector α sz) : Vector α sz :=
   loop (sz / 2) a (Nat.div_le_self ..)
 where
   /-- Inner loop for `mkHeap`. -/
   loop : (i : Nat) → (a : Vector α sz) → i ≤ sz → Vector α sz
   | 0, a, _ => a
   | i+1, a, h =>
-    let a' := heapifyDown lt a ⟨i, Nat.lt_of_succ_le h⟩
+    let a' := heapifyDown a ⟨i, Nat.lt_of_succ_le h⟩
     loop i a' (Nat.le_trans (Nat.le_succ _) h)
 
 /-- 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 : Vector α sz) (i : Fin sz) :
+@[expose]
+def heapifyUp [Ord α] (a : Vector α sz) (i : Fin sz) :
     Vector α sz :=
   match i with
   | ⟨0, _⟩ => a
   | ⟨i'+1, hi⟩ =>
     let j := i'/2
-    if lt a[j] a[i] then
-      heapifyUp lt (a.swap i j) ⟨j, by get_elem_tactic⟩
+    if compare a[j] a[i] |>.isLT then
+      heapifyUp (a.swap i j) ⟨j, by get_elem_tactic⟩
     else a
 
 /-- `O(1)`. Build a new empty heap. -/
-def empty (lt) : BinaryHeap α lt := ⟨#[]⟩
+def empty : BinaryHeap α := ⟨#[]⟩
 
-instance (lt) : Inhabited (BinaryHeap α lt) := ⟨empty _⟩
-instance (lt) : EmptyCollection (BinaryHeap α lt) := ⟨empty _⟩
+instance : Inhabited (BinaryHeap α) := ⟨empty⟩
+instance : EmptyCollection (BinaryHeap α) := ⟨empty⟩
+instance : Membership α (BinaryHeap α) where
+  mem h x := x ∈ h.arr
 
 /-- `O(1)`. Build a one-element heap. -/
-def singleton (lt) (x : α) : BinaryHeap α lt := ⟨#[x]⟩
+def singleton (x : α) : BinaryHeap α := ⟨#[x]⟩
 
 /-- `O(1)`. Get the number of elements in a `BinaryHeap`. -/
-def size (self : BinaryHeap α lt) : Nat := self.1.size
+@[expose]
+def size (self : BinaryHeap α) : Nat := self.1.size
 
 /-- `O(1)`. Get data vector of a `BinaryHeap`. -/
-def vector (self : BinaryHeap α lt) : Vector α self.size := ⟨self.1, rfl⟩
+@[expose]
+def vector (self : BinaryHeap α) : Vector α self.size := ⟨self.1, rfl⟩
 
 /-- `O(1)`. Get an element in the heap by index. -/
-def get (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1[i]'(i.2)
+def get (self : BinaryHeap α) (i : Fin self.size) : α := self.1[i]'(i.2)
 
 /-- `O(log n)`. Insert an element into a `BinaryHeap`, preserving the max-heap property. -/
-def insert (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where
-  arr := heapifyUp lt (self.vector.push x) ⟨_, Nat.lt_succ_self _⟩ |>.toArray
-
-@[simp] theorem size_insert (self : BinaryHeap α lt) (x : α) :
-    (self.insert x).size = self.size + 1 := by
-  simp [size, insert]
+def insert [Ord α] (self : BinaryHeap α) (x : α) : BinaryHeap α where
+  arr := heapifyUp (self.vector.push x) ⟨_, Nat.lt_succ_self _⟩ |>.toArray
 
 /-- `O(1)`. Get the maximum element in a `BinaryHeap`. -/
-def max (self : BinaryHeap α lt) : Option α := self.1[0]?
+def max (self : BinaryHeap α) : Option α := self.1[0]?
 
-/-- `O(log n)`. Remove the maximum element from a `BinaryHeap`.
+/-- `O(log n)`. Remove the maximum element from a `BinaryHeap`
 Call `max` first to actually retrieve the maximum element. -/
-def popMax (self : BinaryHeap α lt) : BinaryHeap α lt :=
+@[expose]
+def popMax [Ord α] (self : BinaryHeap α) : BinaryHeap α :=
   if h0 : self.size = 0 then self else
     have hs : self.size - 1 < self.size := Nat.pred_lt h0
     have h0 : 0 < self.size := Nat.zero_lt_of_ne_zero h0
     let v := self.vector.swap _ _ h0 hs |>.pop
     if h : 0 < self.size - 1 then
-      ⟨heapifyDown lt v ⟨0, h⟩ |>.toArray⟩
+      ⟨heapifyDown v ⟨0, h⟩ |>.toArray⟩
     else
       ⟨v.toArray⟩
 
-@[simp] theorem size_popMax (self : BinaryHeap α lt) :
+@[simp] theorem size_popMax [Ord α] (self : BinaryHeap α) :
     self.popMax.size = self.size - 1 := by
   simp only [popMax, size]
   split
-  · simp +arith [*]
-  · split <;> simp +arith
+  · simp [*]
+  · split <;> simp
 
 /-- `O(log n)`. Return and remove the maximum element from a `BinaryHeap`. -/
-def extractMax (self : BinaryHeap α lt) : Option α × BinaryHeap α lt :=
+def extractMax [Ord α] (self : BinaryHeap α) : Option α × BinaryHeap α :=
   (self.max, self.popMax)
 
-theorem size_pos_of_max {self : BinaryHeap α lt} (h : self.max = some x) : 0 < self.size := by
+theorem size_pos_of_max {self : BinaryHeap α} (h : self.max = some x) : 0 < self.size := by
   simp only [max, getElem?_def] at h
   split at h
   · assumption
   · contradiction
 
 /-- `O(log n)`. Equivalent to `extractMax (self.insert x)`, except that extraction cannot fail. -/
-def insertExtractMax (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt :=
+def insertExtractMax [Ord α] (self : BinaryHeap α) (x : α) : α × BinaryHeap α :=
   match e : self.max with
   | none => (x, self)
   | some m =>
-    if lt x m then
+    if compare x m |>.isLT then
       let v := self.vector.set 0 x (size_pos_of_max e)
-      (m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
+      (m, ⟨heapifyDown v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
     else (x, self)
 
 /-- `O(log n)`. Equivalent to `(self.max, self.popMax.insert x)`. -/
-def replaceMax (self : BinaryHeap α lt) (x : α) : Option α × BinaryHeap α lt :=
+def replaceMax [Ord α] (self : BinaryHeap α) (x : α) : Option α × BinaryHeap α :=
   match e : self.max with
   | none => (none, ⟨self.vector.push x |>.toArray⟩)
   | some m =>
     let v := self.vector.set 0 x (size_pos_of_max e)
-    (some m, ⟨heapifyDown lt v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
+    (some m, ⟨heapifyDown v ⟨0, size_pos_of_max e⟩ |>.toArray⟩)
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `x ≤ self.get i`. -/
-def decreaseKey (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
-  arr := heapifyDown lt (self.vector.set i x) i |>.toArray
+def decreaseKey [Ord α] (self : BinaryHeap α) (i : Fin self.size) (x : α) : BinaryHeap α where
+  arr := heapifyDown (self.vector.set i x) i |>.toArray
 
 /-- `O(log n)`. Replace the value at index `i` by `x`. Assumes that `self.get i ≤ x`. -/
-def increaseKey (self : BinaryHeap α lt) (i : Fin self.size) (x : α) : BinaryHeap α lt where
-  arr := heapifyUp lt (self.vector.set i x) i |>.toArray
+def increaseKey [Ord α] (self : BinaryHeap α) (i : Fin self.size) (x : α) : BinaryHeap α where
+  arr := heapifyUp (self.vector.set i x) i |>.toArray
 
 end Batteries.BinaryHeap
 
 /-- `O(n)`. Convert an unsorted vector to a `BinaryHeap`. -/
-def Batteries.Vector.toBinaryHeap (lt : α → α → Bool) (v : Vector α n) :
-    Batteries.BinaryHeap α lt where
-  arr := BinaryHeap.mkHeap lt v |>.toArray
+def Batteries.Vector.toBinaryHeap [Ord α] (v : Vector α n) :
+    Batteries.BinaryHeap α where
+  arr := BinaryHeap.mkHeap v |>.toArray
 
 open Batteries in
 /-- `O(n)`. Convert an unsorted array to a `BinaryHeap`. -/
-def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : Batteries.BinaryHeap α lt where
-  arr := BinaryHeap.mkHeap lt ⟨a, rfl⟩ |>.toArray
+def Array.toBinaryHeap [Ord α] (a : Array α) : Batteries.BinaryHeap α where
+  arr := BinaryHeap.mkHeap ⟨a, rfl⟩ |>.toArray
 
 open Batteries in
+
+private def revOrd [Ord α] : Ord α where
+  compare x y := compare y x
+
 /-- `O(n log n)`. Sort an array using a `BinaryHeap`. -/
-@[specialize] def Array.heapSort (a : Array α) (lt : α → α → Bool) : Array α :=
-  loop (a.toBinaryHeap (flip lt)) #[]
+@[inline, specialize]
+def Array.heapSort [Ord α] (a : Array α) : Array α :=
+  loop (instOrd := revOrd) (@Array.toBinaryHeap _ revOrd a ) #[]
 where
   /-- Inner loop for `heapSort`. -/
-  loop (a : Batteries.BinaryHeap α (flip lt)) (out : Array α) : Array α :=
+  loop [instOrd : Ord α] (a : Batteries.BinaryHeap α) (out : Array α) : Array α :=
     match e: a.max with
     | none => out
     | some x =>
diff --git a/Batteries/Data/BinaryHeap/Lemmas.lean b/Batteries/Data/BinaryHeap/Lemmas.lean
new file mode 100644
index 0000000000..98238717d5
--- /dev/null
+++ b/Batteries/Data/BinaryHeap/Lemmas.lean
@@ -0,0 +1,453 @@
+module
+public import Batteries.Data.BinaryHeap.Basic
+public import Batteries.Data.BinaryHeap.WF
+import all Batteries.Data.BinaryHeap.WF
+import all Batteries.Data.BinaryHeap.Basic
+
+namespace Batteries.BinaryHeap
+
+
+/-- If maxChild returns none, there are no children in bounds. -/
+theorem maxChild_none_iff [Ord α] (a : Vector α sz) (i : Fin sz) :
+    maxChild a i = none ↔ sz ≤ 2 * i.val + 1 := by
+  grind only [maxChild]
+
+/-- maxChild returns some iff there is at least one child. -/
+theorem maxChild_some_iff [Ord α] (a : Vector α sz) (i : Fin sz) :
+    (maxChild a i).isSome ↔ 2 * i.val + 1 < sz := by
+  grind only [maxChild, = Option.isSome_none, = Option.isSome_some]
+
+/-- If maxChild returns some j, then j is a child of i. -/
+theorem maxChild_isChild [Ord α] (a : Vector α sz) (i : Fin sz) (j : Fin sz)
+    (h : maxChild a i = some j) :
+    j.val = 2 * i.val + 1 ∨ j.val = 2 * i.val + 2 := by
+  grind only [maxChild, = Option.isSome_none, = Option.isSome_some]
+
+/-- maxChild returns an index greater than i. -/
+theorem maxChild_gt [Ord α] (a : Vector α sz) (i : Fin sz) (j : Fin sz)
+    (h : maxChild a i = some j) : i < j := by
+  grind only [maxChild, Lean.Grind.toInt_fin]
+
+
+theorem maxChild_ge_left [Ord α] [Std.OrientedOrd α] (a : Vector α sz) (i j : Fin sz)
+    (hmc : maxChild a i = some j) (hleft : 2 * i.val + 1 < sz) :
+    compare a[j] a[2 * i.val + 1] |>.isGE := by
+  grind only [Std.OrientedOrd.eq_swap, Ordering.swap_lt, Ordering.isGE, Ordering.isLT, maxChild,
+  Fin.getElem_fin]
+
+theorem maxChild_ge_right [Ord α] [Std.OrientedOrd α] (a : Vector α sz)
+    (i j : Fin sz) (hmc : maxChild a i = some j) (hright : 2 * i.val + 2 < sz) :
+    compare a[↑j] a[2 * ↑i + 2] |>.isGE := by
+  grind only [= Fin.getElem_fin, Std.OrientedOrd.eq_swap, Ordering.swap_lt,
+    Ordering.isGE, Ordering.isLT, maxChild]
+
+/-- heapifyDown doesn't modify positions before the starting index. -/
+theorem heapifyDown_preserves_prefix [Ord α] (a : Vector α sz) (i k : Fin sz) (hk : k < ↑i) :
+    (heapifyDown a i)[k] = a[k] := by
+  induction a, i using heapifyDown.induct
+    <;> grind only [heapifyDown, = Fin.getElem_fin, = Vector.getElem_swap]
+
+
+section heapifyDown
+
+/-- `heapifyDown` does not modify elements outside the subtree rooted at `i`. -/
+theorem heapifyDown_get_of_not_inSubtree [Ord α] {a : Vector α sz} {i : Fin sz}
+    {k : Fin sz} (hnsub : ¬InSubtree i k) :
+    (heapifyDown a i)[k] = a[k] := by
+  -- I cannot split on the result of the maxChild call inside of heapifyDown directly because of
+  -- some dependence issue relating to getElem.
+  -- this is a workaround
+  cases hmc : maxChild a i
+  all_goals unfold heapifyDown; conv => lhs; arg 1; simp only; rw [hmc]; simp only;
+
+  rename_i j
+  split <;> try rfl
+  have hij : i < j := by grind only [maxChild_gt]
+
+  have hnsub_j : ¬InSubtree j k := by
+    grind only [InSubtree.not_of_lt, maxChild_isChild,
+      InSubtree.lt_of_ne, InSubtree.trans, InSubtree]
+
+  rw [heapifyDown_get_of_not_inSubtree hnsub_j]
+  grind only [= Fin.getElem_fin, Vector.getElem_swap_of_ne, InSubtree]
+termination_by sz - i
+
+/-- `heapifyDown` preserves `WF.children` for nodes completely outside the affected subtree. -/
+theorem heapifyDown_get_of_not_inSubtree' [Ord α] {a : Vector α sz} {i : Fin sz}
+    {k : Nat} (hk : k < sz) (hnsub : ¬InSubtree i k) :
+    (heapifyDown a i)[k] = a[k] :=
+  heapifyDown_get_of_not_inSubtree (k := ⟨k, hk⟩) hnsub
+
+/-- `heapifyDown` preserves `WF.children` for nodes completely outside the affected subtree. -/
+theorem heapifyDown_preserves_wf_children_of_not_inSubtree [Ord α]
+    {a b : Vector α sz} {i k : Fin sz}
+    (hnsub_k : ¬InSubtree i k) (hk_eq : a[k] = b[k])
+    (hleft_eq : ∀ h : 2 * k.val + 1 < sz, a[2 * k.val + 1] = b[2 * k.val + 1])
+    (hright_eq : ∀ h : 2 * k.val + 2 < sz, a[2 * k.val + 2] = b[2 * k.val + 2])
+    (hwf : WF.children b k)
+    (hnsub_left : i ≠ 2 * k.val + 1 := by omega)
+    (hnsub_right : i ≠ 2 * k.val + 2)
+    :
+    WF.children (heapifyDown a i) k := by
+  obtain ⟨hwf_left, hwf_right⟩ := hwf
+  constructor
+  case' left =>  let childIdx := 2 * k.val + 1
+  case' right => let childIdx := 2 * k.val + 2
+  all_goals
+    intro hbound
+    rw [heapifyDown_get_of_not_inSubtree hnsub_k,
+        heapifyDown_get_of_not_inSubtree' hbound (by grind only)]
+    simp_all
+
+/-- heapifyDown at j preserves WF.children k when i < k < j and j is a child of i -/
+theorem heapifyDown_swap_preserves_wf_children_of_lt [Ord α] {a : Vector α sz} {i j k : Fin sz}
+    (hchild : j.val = 2 * i.val + 1 ∨ j.val = 2 * i.val + 2)
+    (hik : i < k) (hkj : k < j) (hwf : WF.children a k) :
+    WF.children (heapifyDown (a.swap ↑i ↑j) ↑j) ↑k :=
+  heapifyDown_preserves_wf_children_of_not_inSubtree
+    (InSubtree.not_of_lt (by omega))
+    (Vector.getElem_swap_of_ne (by omega) (by omega))
+    (fun _ => Vector.getElem_swap_of_ne (by omega) (by omega))
+    (fun _ => Vector.getElem_swap_of_ne (by omega) (by omega))
+    hwf
+    (by omega)
+    (by omega)
+
+
+theorem heapifyDown_preserves_wf_children_outside [Ord α] {v : Vector α sz} {i k : Fin sz}
+    (hki : k < i) (hwf : WF.children v k)
+    (hleft_ne : i.val ≠ 2 * k.val + 1 ) (hright_ne : i.val ≠ 2 * k.val + 2) :
+    WF.children (heapifyDown v i) k :=
+  heapifyDown_preserves_wf_children_of_not_inSubtree
+    (InSubtree.not_of_lt hki) rfl (fun _ => rfl) (fun _ => rfl) hwf ‹_› ‹_›
+
+/-- If v dominates all values in the subtree, v dominates the result at root -/
+theorem heapifyDown_root_bounded [Ord α] [Std.TransOrd α]
+    {a : Vector α sz} {j : Fin sz} {v : α}
+    (hge : ∀ k : Fin sz, InSubtree j.val k.val → (compare v a[k]).isGE) :
+    (compare v (heapifyDown a j)[j]).isGE := by
+  grind only [heapifyDown, InSubtree, Fin.getElem_fin, maxChild_isChild,
+    = heapifyDown_preserves_prefix, = Vector.getElem_swap]
+
+/-- heapifyDown at i preserves WF.children at parent of i when value decreased -/
+theorem heapifyDown_preserves_wf_parent [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {v : Vector α sz} {i : Fin sz} {x : α}
+    (htd : WF.topDown v) (h_le : compare x v[i] |>.isLE) (hi : 0 < i.val) :
+    WF.children (heapifyDown (v.set i x) i) ⟨(i.val - 1) / 2, by omega⟩ := by
+  let parent : Fin sz := ⟨(i.val - 1) / 2, by omega⟩
+  have h_parent_lt_i : parent < i := by grind only [Lean.Grind.toInt_fin]
+  have hk_not_sub : ¬InSubtree i parent := InSubtree.not_of_lt h_parent_lt_i
+  obtain ⟨hwf_parent_l, hwf_parent_r⟩ := htd parent
+  have h_parent_child : i.val = 2 * parent.val + 1 ∨ i.val = 2 * parent.val + 2 := by grind only
+  constructor
+  case' left  => let childIdx := 2 * parent.val + 1
+  case' right => let childIdx := 2 * parent.val + 2
+  all_goals
+    intro hside
+    rw [heapifyDown_get_of_not_inSubtree hk_not_sub]
+    have : parent.val ≠ i.val := by omega
+    simp only [Fin.getElem_fin]
+    rw [Vector.getElem_set_ne (i := i.val) (j := parent.val) _ _ (by omega)]
+    by_cases heq : childIdx = i.val
+    · simp only [parent, heq, childIdx]
+      exact heapifyDown_root_bounded (WF.parent_dominates_set_subtree htd h_le hi)
+    . have hsub : ¬InSubtree i.val childIdx :=  by grind only [InSubtree.not_of_lt]
+      rw [heapifyDown_get_of_not_inSubtree' hside hsub]
+      rw [Vector.getElem_set_ne _ _ (by simp_all only [ne_eq]; omega)]
+      simp_all [childIdx, parent]
+
+
+theorem heapifyDown_perm [Ord α] {a : Vector α sz} {i : Fin sz} :
+    (heapifyDown a i).Perm a
+  := by
+    induction a, i using heapifyDown.induct with grind only
+      [Vector.swap_perm, heapifyDown, Vector.Perm.rfl, Vector.Perm.trans]
+
+/-- a[j] dominates everything in (a.swap i j)'s subtree at j when i < j and a[i] < a[j] -/
+theorem swap_child_dominates [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {a : Vector α sz} {i j : Fin sz} (h_ij : i < j) (h_lt : (compare a[i] a[j]).isLT)
+    (hbelow : WF.below a i) (k : Fin sz) (hsub : InSubtree j k) :
+    (compare a[j] (a.swap i j)[k]).isGE := by
+  by_cases hk_eq_j : k.val = j.val
+  · unfold Ordering.isGE
+    rw [Std.OrientedOrd.eq_swap]
+    simp_all
+  · have hi' : k.val ≠ i.val := InSubtree.ne_of_lt h_ij hsub
+    simp_all [WF.parent_ge_subtree, hbelow j h_ij, Vector.getElem_swap_of_ne,
+      WF.below_mono (Fin.le_of_lt h_ij) hbelow]
+
+theorem heapifyDown_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {a : Vector α sz} {i : Fin sz}
+    (hbelow : WF.below a i) :
+    WF.children (heapifyDown a i) i ∧ WF.below (heapifyDown a i) i := by
+  induction a, i using heapifyDown.induct with
+  | case1 a i h => grind only [WF.children, WF.below, maxChild]
+  | case2 a i j hmaxChild h_ij h_ai_aj ih =>
+    obtain ⟨ih_at, ih_below⟩ := ih (WF.below_swap (hbelow := hbelow) (hij := h_ij))
+    have hnsub_i : ¬InSubtree j.val i.val := InSubtree.not_of_lt h_ij
+    have hchild := maxChild_isChild a i j hmaxChild
+
+    have hchildren : WF.children (heapifyDown a i) i := by
+      constructor
+
+      all_goals
+        intro hside
+        unfold heapifyDown
+
+        -- I cannot reduce the match statement inside heapifyDown directly via hmaxChild
+        -- because of some dependence issue. This is a workaround
+        simp only
+        conv => lhs; arg 1; arg 1; arg 1; rw [hmaxChild]
+        conv => lhs; arg 1; arg 2; arg 1; rw [hmaxChild]
+        simp only [h_ai_aj, ↓reduceIte]
+
+        simp only [heapifyDown_get_of_not_inSubtree hnsub_i, Fin.getElem_fin,
+          Vector.getElem_swap_left]
+
+        cases hchild
+
+      case left.inl | right.inr =>
+        grind only [Fin.getElem_fin,
+          heapifyDown_root_bounded (swap_child_dominates h_ij h_ai_aj hbelow)]
+      case left.inr =>
+        have hnsub_l : ¬InSubtree j.val (2 * i.val + 1) := InSubtree.not_of_lt (by omega)
+        grind only [Fin.getElem_fin, = Vector.getElem_swap,
+          InSubtree, = maxChild_ge_left, heapifyDown_get_of_not_inSubtree' hside hnsub_l]
+      case right.inl =>
+        have hnsub_r : ¬InSubtree j.val (2 * i.val + 2) := by grind only [InSubtree.not_of_lt]
+        grind only [Fin.getElem_fin, = Vector.getElem_swap,
+          InSubtree, = maxChild_ge_right, heapifyDown_get_of_not_inSubtree' hside hnsub_r]
+
+    have hbelow : WF.below (heapifyDown a i) i  := by
+      unfold heapifyDown
+      intro k
+      split
+      . grind only
+      . cases Nat.lt_trichotomy j k <;> grind only [heapifyDown_swap_preserves_wf_children_of_lt,
+        WF.children, WF.below, = Fin.getElem_fin]
+
+    exact ⟨hchildren, hbelow⟩
+  | case3 a i j hmaxChild hij h_lt =>
+    have h_ge : (compare a[i] a[j]).isGE
+      := by grind only [Ordering.isGE, Ordering.isLT]
+    grind only [heapifyDown, WF.children, = Fin.getElem_fin,
+      InSubtree.not_of_lt, !Std.TransOrd.isGE_trans, = maxChild_ge_left,
+      = maxChild_ge_right]
+
+end heapifyDown
+
+section heapifyUp
+
+/-- heapifyUp fixes the heap when the only violation is at i
+    and i's children are already ≤ i's parent -/
+theorem heapifyUp_wf_bottomUp [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {a : Vector α sz} {i : Fin sz}
+    (hexcept : WF.exceptAt a i)
+    (hchildren : WF.childLeParent a i) :
+    WF.bottomUp (heapifyUp a i) := by
+  induction a, i using heapifyUp.induct with
+  | case1 a =>
+    simp only [heapifyUp]
+    exact WF.bottomUp_of_exceptAt_zero a (by omega) hexcept
+  | case2 a i hisucc j h_lt ih =>
+    have h_le : compare a[j] a[i+1] |>.isLE := by
+      grind only [Ordering.isLT, Ordering.isLE, = Fin.getElem_fin]
+    simp only [heapifyUp, h_lt, ↓reduceIte, j]
+    apply ih
+    · exact WF.exceptAt_swap a ⟨i+1, by omega⟩ h_le hexcept hchildren
+    · exact WF.childLeParent_swap a ⟨i+1, by omega⟩ h_le hexcept
+  | case3 a i hisucc j h_nlt =>
+    simp_all only [heapifyUp, j]
+    apply WF.bottomUp_of_exceptAt_and_parent a ⟨i+1, by omega⟩ hexcept
+    exact WF.parent_of_isGE a
+      ⟨i+1, by omega⟩
+      (by grind only)
+      (by grind only [Ordering.isLT, Ordering.isGE])
+
+theorem heapifyUp_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {a : Vector α sz} {i : Fin sz} (hexcept : WF.exceptAt a i) (hchildren : WF.childLeParent a i) :
+    WF.topDown (heapifyUp a i) := by
+  rw [WF.iff_bottomUp]
+  simp_all [heapifyUp_wf_bottomUp]
+
+theorem heapifyUp_perm [Ord α] {a : Vector α sz} {i : Fin sz} :
+    (heapifyUp a i).Perm a
+  := by
+    induction a, i using heapifyUp.induct
+    all_goals
+      unfold heapifyUp
+      grind only [Vector.Perm.trans, Vector.swap_perm, heapifyUp, Vector.Perm.rfl]
+end heapifyUp
+
+theorem mkHeap.loop_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {n : Nat} {a : Vector α sz} {h : n ≤ sz}
+    (hinv : ∀ k : Fin sz, n ≤ k.val → WF.children a k) :
+    ∀ k : Fin sz, WF.children (mkHeap.loop n a h) k := by
+  induction n generalizing a with
+  | zero => simp_all [mkHeap.loop]
+  | succ i ih =>
+    have hi_lt : i < sz := by omega
+    obtain ⟨hwf_at, hwf_below⟩:= heapifyDown_wf (a := a) (i := ⟨i, hi_lt⟩) hinv
+    have hinv' : ∀ k : Fin sz, i ≤ k.val → WF.children (heapifyDown a ⟨i, hi_lt⟩) k := by
+      intro k hk
+      by_cases hk_eq : k = i
+      · grind only
+      · have hlt : i < k := by omega
+        exact hwf_below k hlt
+    exact ih hinv'
+
+public section
+
+@[simp]
+theorem size_empty : (@empty α).size = 0 := by
+  simp_all [empty, size]
+
+@[simp, grind .]
+theorem empty_wf [Ord α] :  WF (empty : BinaryHeap α) := by
+  simp [empty, WF, vector, WF.topDown_empty]
+
+@[simp, grind .]
+theorem singleton_wf [Ord α] {x : α} : WF (singleton x) := by
+  simp [WF, singleton, vector, WF.topDown_singleton]
+
+@[simp, grind .]
+theorem mkHeap_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] {a : Vector α sz} :
+    WF.topDown (mkHeap a) := by
+  unfold mkHeap
+  apply mkHeap.loop_wf
+  intro _ _
+  constructor
+  all_goals
+    intro _
+    exfalso
+    omega
+
+@[simp]
+theorem size_insert [Ord α] (heap : BinaryHeap α) (x : α) :
+    (heap.insert x).size = heap.size + 1 := by
+  simp [size, insert]
+
+@[grind .]
+theorem insert_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] {heap : BinaryHeap α}
+    {x : α} (h_wf : heap.WF) :
+    (heap.insert x).WF := by
+  skip
+  unfold insert
+  have h_sz : heap.vector.size < (heap.vector.push x).size := by grind only [size_insert]
+  have h_ea : WF.exceptAt (heap.vector.push x) ⟨heap.vector.size, h_sz⟩ := by
+    intro i _
+    unfold WF at h_wf
+    rw [WF.iff_bottomUp] at h_wf
+    unfold WF.bottomUp at h_wf
+    have : i < heap.vector.size := by grind only
+    intro h_nz
+    grind [h_wf ⟨i.val, by omega⟩ h_nz]
+  have h_clp : WF.childLeParent (heap.vector.push x) ⟨heap.vector.size, h_sz⟩ := by
+    grind only [WF.childLeParent]
+  simp only [WF, WF.iff_bottomUp]
+  have := heapifyUp_wf_bottomUp h_ea h_clp
+  rw [← Vector.mk_toArray (xs := (heapifyUp _ _))] at this
+  grind only [vector, size]
+
+theorem mem_def {x : α} {h : BinaryHeap α} : x ∈ h ↔ x ∈ h.arr := Iff.rfl
+
+theorem mem_insert [Ord α] {heap : BinaryHeap α} :
+    y ∈ heap.insert x ↔ y = x ∨ y ∈ heap := by
+  unfold insert
+  simp [mem_def]
+  have := heapifyUp_perm (a := heap.vector.push x) (i := ⟨heap.size, by omega⟩)
+  rw [Vector.Perm.mem_iff this (a := y)]
+  grind only [vector, Vector.push_mk, Vector.mem_mk, Array.mem_push]
+
+theorem mem_iff_get {heap : BinaryHeap α} :
+    a ∈ heap ↔ ∃ i : Fin heap.size, heap.get i = a := by
+  simp_all [mem_def, get, Array.mem_iff_getElem, size]
+  constructor
+  . rintro ⟨x, y, z⟩
+    exact ⟨⟨x, y⟩, z⟩
+  . rintro ⟨⟨x, y⟩, z⟩
+    exact ⟨x, y, z⟩
+
+@[grind .]
+theorem max_ge_all [Ord α] [Std.TransOrd α]
+    {heap : BinaryHeap α} {y: α} (hwf : WF heap) (h_in: y ∈ heap) (h_ne : heap.size > 0) :
+    let root := heap.max.get (by simp_all [max, size])
+    compare root y |>.isGE := by
+  obtain ⟨idx, h_sz, h_ge⟩ := Array.mem_iff_getElem.mp h_in
+  have :=  WF.root_ge_all hwf h_ne ⟨idx, h_sz⟩
+  simp_all [vector, max]
+
+@[simp]
+theorem max_eq_none_iff {heap : BinaryHeap α} : heap.max = none ↔ heap.size = 0 := by
+  simp [max, size]
+
+@[grind .]
+theorem popMax_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {heap : BinaryHeap α} (h_wf : WF heap) :
+    WF (heap.popMax) := by
+  unfold popMax
+  have htd : WF.topDown heap.vector := by simp_all [WF]
+  simp only
+  split
+  . simp_all [WF]
+  . split <;> apply WF.topDown_toArray
+    . have hbelow : WF.below (heap.vector.swap 0 (heap.size - 1) |>.pop) 0 := by
+        grind only [WF.below_swap_pop htd]
+      simp_all [WF.topDown_iff_at_below_zero.mp, heapifyDown_wf (i := ⟨0, by omega⟩) hbelow]
+    . grind only [WF.children, WF.topDown]
+
+@[grind .]
+theorem decreaseKey_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] {heap : BinaryHeap α}
+    {i : Fin heap.size} (h_wf : WF heap) (h_leq : compare x (heap.get i) |>.isLE) :
+    WF (heap.decreaseKey i x) := by
+  unfold decreaseKey
+
+  apply WF.topDown_toArray
+  have htd : WF.topDown heap.vector := by simp_all [WF]
+
+  have hbelow : WF.below (heap.vector.set i x) i := WF.set_smaller_wf_below htd
+  have ⟨hchildren_i, hbelow_i⟩ := heapifyDown_wf hbelow
+
+  intro k
+  rcases Nat.lt_trichotomy k.val i.val with hki | hki_eq | hik
+  · by_cases hk_parent : k.val = (i.val - 1) / 2 ∧ 0 < i.val
+    · have hk_eq : k = ⟨(i.val - 1) / 2, by omega⟩ := by ext; exact hk_parent.1
+      rw [hk_eq]
+      exact heapifyDown_preserves_wf_parent htd h_leq hk_parent.2
+    · have hleft_ne : i.val ≠ 2 * k.val + 1 := by omega
+      have hright_ne : i.val ≠ 2 * k.val + 2 := by omega
+      have hwf_set : WF.children (heap.vector.set i x) k :=
+              WF.set_preserves_wf_children_of_ne (htd k) (by omega) hleft_ne hright_ne
+      exact heapifyDown_preserves_wf_children_outside hki hwf_set hleft_ne hright_ne
+  · exact Fin.ext hki_eq ▸ hchildren_i
+  · exact hbelow_i k hik
+
+
+@[grind .]
+theorem increaseKey_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] {heap : BinaryHeap α}
+    {i : Fin heap.size} (h_wf : WF heap) (h_ge : compare x (heap.get i) |>.isGE) :
+    WF (heap.increaseKey i x) := by
+  unfold increaseKey
+  generalize hv : heap.vector = v
+  have htd : WF.topDown v := by simp_all [WF]
+  have hbu : WF.bottomUp v := by rw [← WF.iff_bottomUp]; exact htd
+  have h_ge' : compare x v[i] |>.isGE := by
+    simp_all [get, ← hv, vector]
+  apply WF.topDown_toArray
+  rw [WF.iff_bottomUp]
+  simp_all [WF.exceptAt_set_larger, WF.childLeParent_set_larger, heapifyUp_wf_bottomUp]
+
+end
+end BinaryHeap
+
+public section
+open Batteries.BinaryHeap
+
+theorem Array.toBinaryHeap_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] {a : Array α} :
+    WF (a.toBinaryHeap) := by
+  simp [WF.topDown_toArray, Array.toBinaryHeap]
+
+theorem Vector.toBinaryHeap_wf [Ord α] [Std.TransOrd α] [Std.OrientedOrd α] {a : Vector α sz} :
+    WF (Batteries.Vector.toBinaryHeap a) := by
+  simp [WF.topDown_toArray, Vector.toBinaryHeap]
+end
diff --git a/Batteries/Data/BinaryHeap/WF.lean b/Batteries/Data/BinaryHeap/WF.lean
new file mode 100644
index 0000000000..44db6bcf31
--- /dev/null
+++ b/Batteries/Data/BinaryHeap/WF.lean
@@ -0,0 +1,333 @@
+module
+public import Batteries.Data.BinaryHeap.Basic
+
+namespace Batteries.BinaryHeap
+
+/-- The size of the underlying vector is preserved when constructing a `BinaryHeap`. -/
+theorem vector_size {v : Vector α sz} :
+    (BinaryHeap.mk v.toArray).vector.size = sz := by
+  simp [Vector.size, Vector.size_toArray, size]
+
+/-- Index `k` lies in the subtree rooted at index `root` in the implicit binary heap tree. -/
+@[grind]
+inductive InSubtree (root : Nat) : Nat → Prop
+  | refl : InSubtree root root
+  | left : InSubtree root k → InSubtree root (2 * k + 1)
+  | right : InSubtree root k → InSubtree root (2 * k + 2)
+
+
+namespace InSubtree
+
+theorem le  (ins : InSubtree j k) : j ≤ k := by
+  induction ins <;> omega
+
+theorem not_of_lt (hlt : k < j): ¬InSubtree j k := by
+  intro hsub
+  have := hsub.le
+  omega
+
+theorem lt_of_ne (hsub : InSubtree j k) (hne : j ≠ k) : j < k := by grind only [hsub.le]
+
+theorem trans (hij : InSubtree i j) (hjk : InSubtree j k) : InSubtree i k := by
+  induction hjk with grind only [InSubtree]
+
+theorem ne_of_lt (h: i < j) (hins : InSubtree j k) : k ≠ i := by
+  have : j ≤ k := InSubtree.le hins
+  omega
+
+/-- Every index lies in the subtree rooted at 0. -/
+theorem zero_root (a : Nat) : InSubtree 0 a := by
+  induction a using Nat.strongRecOn with
+  | _ n ih =>
+    match n with
+    | 0 => exact .refl
+    | n + 1 =>
+      if h : n % 2 = 0 then
+        have : n + 1 = 2 * (n / 2) + 1 := by omega
+        exact this ▸ .left (ih (n / 2) (by omega))
+      else
+        have : n + 1 = 2 * (n / 2) + 2 := by omega
+        exact this ▸ .right (ih (n / 2) (by omega))
+end InSubtree
+
+
+/-- The primary local correctness property for the heap. A node should be >= both its children
+    (if it has them).
+-/
+@[expose]
+public def WF.children [Ord α] (a : Vector α sz) (i : Fin sz) : Prop :=
+  let left := 2 * i.val + 1
+  let right := left + 1
+  (∀ _ : left < sz, compare a[i] a[left] |>.isGE) ∧
+  (∀ _ : right < sz, compare a[i] a[right] |>.isGE)
+
+/-- The vector underlying a `BinaryHeap` is well-formed iff every node is ≥ any children it has -/
+@[expose]
+public def WF.topDown [Ord α] (v : Vector α sz) : Prop :=
+  ∀ i : Fin sz, WF.children v i
+
+/-- The well-formedness property of a binary heap -/
+@[expose]
+public def WF [Ord α] (self : BinaryHeap α) : Prop :=
+  WF.topDown self.vector
+
+namespace WF
+variable {α : Type w} {sz : Nat}
+/-- All nodes at indices greater than `i` are well-formed (according to WF.children)
+    Used when verifying `heapifyDown` -/
+def below [Ord α] (a : Vector α sz) (i : Nat) : Prop :=
+  ∀ j : Fin sz, i < j.val → WF.children a j
+
+/-- WF.below is monotone: larger threshold means weaker condition. -/
+theorem below_mono {a : Vector α sz} {i j : Nat}  [Ord α]
+    (hij : i ≤ j) (hbelow : WF.below a i) : WF.below a j := by
+  grind only [WF.below]
+
+/-- if i < j, and the heap is well formed below i, then a[i] and a[j] can be swapped
+  and the heap will still be well-formed below j --/
+theorem below_swap [Ord α] {a : Vector α sz} {i j : Fin sz}
+    {hbelow : WF.below a i} {hij : i < j} :
+    WF.below (a.swap i j) j := by
+  intro k hk_gt_j
+  have hk_gt_i : i.val < k.val := Nat.lt_trans ‹_› ‹_›
+  obtain ⟨_, _⟩ := hbelow k hk_gt_i
+  grind only [= Fin.getElem_fin, = Vector.getElem_swap, WF.children]
+
+/-- Setting a smaller value preserves WF.below -/
+theorem set_smaller_wf_below [Ord α] {v : Vector α sz} {i : Fin sz} {x : α}
+    (htd : WF.topDown v) :
+    WF.below (v.set i x) i := by
+  intro j hj
+  obtain ⟨hwf_jl, hwf_jr⟩ := htd j
+  grind only [Vector.getElem_set, Fin.getElem_fin, WF.children]
+
+/-- For k < i where neither child equals i, set at i preserves WF.children at k -/
+theorem set_preserves_wf_children_of_ne [Ord α] {v : Vector α sz} {i k : Fin sz} {x : α}
+    (hwf : WF.children v k) (hki : k.val ≠ i.val)
+    (hleft_ne : i.val ≠ 2 * k.val + 1) (hright_ne : i.val ≠ 2 * k.val + 2) :
+    WF.children (v.set i x) k := by
+  obtain ⟨hwf_left, hwf_right⟩ := hwf
+  grind only [Vector.getElem_set, Fin.getElem_fin, WF.children]
+
+theorem topDown_empty [Ord α] : WF.topDown (#v[] : Vector α 0) := by
+  simp [topDown]
+
+
+theorem topDown_singleton [Ord α] {x : α} : WF.topDown #v[x] := by
+  simp [topDown, children]
+
+
+/-- WF.topDown follows from WF.children at 0 and WF.below at 0 -/
+theorem topDown_iff_at_below_zero [Ord α] {a : Vector α sz} {h0 : 0 < sz} :
+   WF.children a ⟨0, h0⟩ ∧  WF.below a 0 ↔ WF.topDown a := by
+  constructor
+  . rintro ⟨_, hbelow⟩
+    intro j
+    by_cases h : j.val = 0
+    . grind only
+    . exact hbelow j (by omega)
+  . grind only [children, topDown, below]
+
+/-- A node dominates all descendants in its subtree in a well-formed heap. -/
+theorem parent_ge_subtree [Ord α] [Std.TransOrd α]
+    {a : Vector α sz} {j k : Nat} {hk : k < sz} {hj : j < sz} (hwf_at : WF.children a ⟨j, hj⟩)
+    (hwf_below : WF.below a j) (hsub : InSubtree j k) :
+    (compare a[j] a[k]).isGE := by
+  induction hsub
+  case refl => grind only [Ordering.isGE]
+  all_goals
+    obtain ⟨hwf_m, _⟩ : WF.children a ⟨‹_›, by omega⟩ := by
+      grind only [WF.below, InSubtree.not_of_lt]
+    grind only [= Fin.getElem_fin, !Std.TransOrd.isGE_trans]
+
+/-- Parent dominates all descendants after setting a smaller value -/
+theorem parent_dominates_set_subtree [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {v : Vector α sz} {i : Fin sz} {x : α}
+    (htd : WF.topDown v) (h_le : compare x v[i] |>.isLE) (hi : 0 < i.val)
+    (m : Fin sz) (hsub : InSubtree i.val m.val) :
+    (compare v[(i.val - 1) / 2] (v.set i x)[m]).isGE := by
+  let parent : Fin sz := ⟨(i.val - 1) / 2, by omega⟩
+  have h_parent_child : i.val = 2 * parent.val + 1 ∨ i.val = 2 * parent.val + 2 := by grind only
+  obtain ⟨hwf_parent_l, hwf_parent_r⟩ := htd parent
+  have h_parent_ge_i : (compare v[parent] v[i]).isGE := by grind only [= Fin.getElem_fin]
+  by_cases hm_eq : m.val = i.val
+  · grind only [Std.OrientedOrd.eq_swap, = Fin.getElem_fin, !Std.TransOrd.isGE_trans,
+    = Vector.getElem_set, !Ordering.isGE_swap]
+  · have : i.val ≠ m.val := by omega
+    simp_all only [Fin.getElem_fin, ne_eq, not_false_eq_true, Vector.getElem_set_ne]
+    have h_parent_to_i : InSubtree parent.val i.val := by grind only [InSubtree]
+    exact WF.parent_ge_subtree
+      (hwf_at := htd parent)
+      (hwf_below := fun j _ => htd j)
+      (hsub := InSubtree.trans h_parent_to_i hsub)
+
+/-- The root element is greater than or equal to all heap elements. -/
+theorem root_ge_all [Ord α] [Std.TransOrd α]
+    {a : Vector α sz} (hwf : WF.topDown a) (hne : 0 < sz) (k : Fin sz) :
+    (compare a[0] a[k]).isGE :=
+  parent_ge_subtree
+    (hwf_at := hwf ⟨0, hne⟩)
+    (hwf_below := fun j _ => hwf j)
+    (hsub := InSubtree.zero_root k.val)
+
+/-- "Dual" correctness property to WF.children. A node should be <= its parent
+    Used when verifying heapifyUp -/
+def parent [Ord α] (a : Vector α sz) (i : Fin sz) : Prop :=
+  ∀ _ : 0 < i.val, compare a[i] a[(i.val - 1)/2] |>.isLE
+
+/-- The comparison gives us the parent property -/
+theorem parent_of_isGE [Ord α] [Std.OrientedOrd α] (a : Vector α sz) (i : Fin sz) (hi : 0 < i.val)
+    (h : compare a[(i.val - 1) / 2] a[i] |>.isGE) :
+    WF.parent a i := by
+  grind only [Std.OrientedOrd.eq_swap, !Ordering.isGE_swap, WF.parent]
+
+/-- The children of node `i` are <= node `i`'s parent
+    Part of the invariant required/maintained by heapifyUp
+-/
+def childLeParent [Ord α] (a: Vector α sz) (i : Fin sz) : Prop :=
+  let parent := (i.val - 1) / 2
+  let left := 2 * i.val + 1
+  let right := left + 1
+  (∀ _ : left < sz, compare a[left] a[parent] |>.isLE) ∧
+  (∀ _ : right < sz, compare a[right] a[parent] |>.isLE)
+
+
+/-- Every other node (except possibly i) is <= its parent (if it has one)
+    Part of the invariant required/maintained by heapifyUp
+-/
+def exceptAt [Ord α] (a : Vector α sz) (i : Fin sz) : Prop :=
+  ∀ j : Fin sz, i ≠ j → WF.parent a j
+
+/-- If exceptAt i and childLeParent i, swap preserves exceptAt at parent -/
+theorem exceptAt_swap [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    (a : Vector α sz) (i : Fin sz)
+    (h_le : compare a[(i.val - 1) / 2] a[i] |>.isLE)
+    (hexcept : WF.exceptAt a i)
+    (hchildren : WF.childLeParent a i) :
+    WF.exceptAt (a.swap i ((i.val - 1) / 2)) ⟨(i.val - 1) / 2, by omega⟩ := by
+  intro k hkj hk_pos
+  by_cases hki : k.val = i.val
+  · simp_all
+  · by_cases hk_child_of_i : (k.val - 1) / 2 = i.val
+    · obtain ⟨hleft, hright⟩ := hchildren
+      have hk_is_child : k.val = 2 * i.val + 1 ∨ k.val = 2 * i.val + 2 := by omega
+      have hk_ne_parent : k.val ≠ (i.val - 1) / 2 := by omega
+      rcases hk_is_child with hk_left | hk_right
+      · simp_all [show 2 * i.val + 1 < sz by omega]
+      · simp_all [show 2 * i.val + 2 < sz by omega]
+    · unfold exceptAt parent at *
+      grind only [Fin.ext_iff, Fin.isLt, = Fin.getElem_fin, = Vector.getElem_swap,
+        !Std.TransOrd.isLE_trans]
+
+/-- If exceptAt a i, swap preserves childLeParent at parent -/
+theorem childLeParent_swap [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    (a : Vector α sz) (i : Fin sz)
+    (h_le : compare a[(i.val - 1) / 2] a[i] |>.isLE)
+    (hexcept : WF.exceptAt a i) :
+    WF.childLeParent (a.swap i ((i.val - 1) / 2)) ⟨(i.val - 1) / 2, by omega⟩ := by
+  unfold WF.childLeParent at *
+  let j := (i.val - 1) / 2
+  constructor
+  case' left  => let targetIdx := 2 * j + 1
+  case' right => let targetIdx := 2 * j + 2
+  all_goals
+    intro hside
+    unfold WF.exceptAt WF.parent at hexcept
+    by_cases hli : targetIdx = i.val
+    · have hji : j ≠ i.val := by omega
+      grind only [= Fin.getElem_fin, = Vector.getElem_swap]
+    · have hparent_eq : (targetIdx - 1) / 2 = j := by omega
+      have h1 := hexcept ⟨targetIdx, hside⟩ (by grind only [Fin.ext_iff]) (by grind only)
+      by_cases hj_pos : 0 < j <;>
+        grind only [= Fin.getElem_fin, = Vector.getElem_swap, !Std.TransOrd.isLE_trans]
+
+/- Dual global correctness property to `WF`. The vector underlying a BinomialHeap is well-formed
+  iff all nodes are ≤ their parent.
+  Used when verifying heapifyUp.
+-/
+def bottomUp [Ord α] (v : Vector α sz) : Prop :=
+  ∀ i : Fin sz, WF.parent v i
+
+/- WF and WF.bottomUp are equivalent -/
+theorem iff_bottomUp [Ord α] [Std.OrientedOrd α] (a : Vector α sz) :
+    WF.topDown a ↔ WF.bottomUp a := by
+  constructor
+  · intro hTop i
+    have := hTop ⟨(i.val - 1) / 2, by omega⟩
+    grind only [Ordering.isGE_swap, Std.OrientedOrd.eq_swap, WF.children,
+      WF.parent, = Fin.getElem_fin]
+  · intro hBottom i
+    constructor <;> intro hchild
+    case' mpr.left => have := hBottom ⟨2 * i.val + 1, hchild⟩
+    case' mpr.right => have := hBottom ⟨2 * i.val + 2, hchild⟩
+    all_goals grind only [Std.OrientedOrd.eq_swap, parent, = Fin.getElem_fin,
+      !Ordering.isGE_swap]
+
+/-- If exception is at 0, then bottomUp holds -/
+theorem bottomUp_of_exceptAt_zero [Ord α] (a : Vector α sz) (h : 0 < sz)
+    (hexcept : WF.exceptAt a ⟨0, h⟩) :
+    WF.bottomUp a := by
+  grind only [WF.parent, Fin.ext_iff, WF.bottomUp, WF.exceptAt]
+
+/-- If parent property holds at i and exceptAt i, then bottomUp -/
+theorem bottomUp_of_exceptAt_and_parent [Ord α] (a : Vector α sz) (i : Fin sz)
+    (hexcept : WF.exceptAt a i) (hparent : WF.parent a i) :
+    WF.bottomUp a := by
+  grind only [bottomUp, parent, exceptAt]
+
+
+theorem topDown_toArray {v : Vector α sz} [Ord α] (h_td : WF.topDown v) : WF ⟨v.toArray⟩ := by
+  rintro ⟨ival, _⟩
+  obtain ⟨hleft, hright⟩ := h_td ⟨ival, by simp_all [size]⟩
+  constructor <;> intro _
+  . exact hleft (by grind only [!vector_size])
+  . exact hright (by grind only [!vector_size])
+
+/-- Setting a larger value preserves WF.exceptAt -/
+theorem exceptAt_set_larger [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {v : Vector α sz} {i : Fin sz} {x : α}
+    (hbu : WF.bottomUp v) (h_ge : compare x v[i] |>.isGE) :
+    WF.exceptAt (v.set i x) i := by
+  intro j hji hj_pos
+  by_cases hparent_eq : (j.val - 1) / 2 = i.val
+  all_goals
+    have hj_parent := hbu j hj_pos
+    grind only [Std.OrientedOrd.eq_swap, = Fin.getElem_fin, = Vector.getElem_set,
+      !Ordering.isGE_swap, !Std.TransOrd.isLE_trans]
+
+/-- Setting a larger value preserves WF.childLeParent when original heap is well-formed -/
+theorem childLeParent_set_larger [Ord α] [Std.TransOrd α] [Std.OrientedOrd α]
+    {v : Vector α sz} {i : Fin sz} {x : α}
+    (htd : WF.topDown v) (hbu : WF.bottomUp v) (h_ge : compare x v[i] |>.isGE) :
+    WF.childLeParent (v.set i x) i := by
+  unfold WF.childLeParent
+  let parent := (i.val - 1) / 2
+  obtain ⟨htd_left, htd_right⟩ := htd i
+  constructor
+  case' left  => intro hchild; have h_child := htd_left hchild
+  case' right => intro hchild; have h_child := htd_right hchild
+  all_goals
+    by_cases hi : i.val = 0
+    · -- i = 0, so parent = 0 = i
+      have hset_parent : (v.set i x)[parent] = x := by simp_all [parent]
+      grind only [!Std.TransOrd.isLE_trans, Std.OrientedOrd.eq_swap, !Ordering.isGE_swap,
+        Vector.getElem_set]
+    · -- i ≠ 0, so parent ≠ i
+      have h_parent := hbu i (by omega)
+      grind only [!Std.TransOrd.isLE_trans, Std.OrientedOrd.eq_swap, !Ordering.isGE_swap,
+        WF.parent, Vector.getElem_set]
+
+theorem below_swap_pop [Ord α] {a : Vector α sz} (wf : WF.topDown a)
+    (h0 : 0 < sz) :
+    WF.below (a.swap 0 (sz - 1)|>.pop) 0 := by
+  intro j hj
+  constructor
+  · intro hleft
+    have := (wf ⟨j.val, by omega⟩).1 (by omega : 2 * j.val + 1 < sz)
+    grind only [Vector.getElem_swap, Vector.getElem_pop, Fin.getElem_fin]
+  · intro hright
+    have := (wf ⟨j.val, by omega⟩).2 (by omega : 2 * j.val + 2 < sz)
+    grind only [Vector.getElem_swap, Vector.getElem_pop, Fin.getElem_fin]
+
+end WF
+end Batteries.BinaryHeap