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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ loop.OpSpec lt x n (loop lt x n)
Tactic:
induction n generalizing x with
| zero => exact .zero x
| succ n IH => exact .succ <| IH (popMax lt x)
State after:
no goals

State before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ loop.OpSpec lt x Nat.zero (loop lt x Nat.zero)
Tactic:
exact .zero x
State after:
no goals

State before:
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), loop.OpSpec lt x n (loop lt x n)
x : Subarray α
⊢ loop.OpSpec lt x (Nat.succ n) (loop lt x (Nat.succ n))
Tactic:
exact .succ <| IH (popMax lt x)
State after:
no goals