Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.size_eq (Algdata/Data/BinaryHeap/Basic.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
⊢ Subarray.size y = Subarray.size x
Tactic:
simp only [Subarray.size, h.stop_eq, h.start_eq]
State after:
no goals