Theorem: Algdata.BinaryHeap.size_mkHeap_loop (Algdata/Data/BinaryHeap/Basic.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ Subarray.size (mkHeap.loop lt x n) = Subarray.size x
Tactic:
dsimp [Subarray.size]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ (mkHeap.loop lt x n).stop - (mkHeap.loop lt x n).start = x.stop - x.start

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ (mkHeap.loop lt x n).stop - (mkHeap.loop lt x n).start = x.stop - x.start
Tactic:
rw [start_mkHeap_loop, stop_mkHeap_loop]
State after:
no goals