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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
⊢ Array.size y = Array.size x.as
Tactic:
induction h with
| zero => rfl
| succ h IH => rw [IH, size_as_popMax]
State after:
no goals

State before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
⊢ Array.size x✝.as = Array.size x✝.as
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : Array.size y✝ = Array.size (popMax lt x✝).as
⊢ Array.size y✝ = Array.size x✝.as
Tactic:
rw [IH, size_as_popMax]
State after:
no goals