Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.to_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
⊢ y = loop lt x n
Tactic:
induction h with
| zero => rfl
| succ h IH => rw [IH]; rfl
State after:
no goals

State before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
⊢ x✝.as = loop lt x✝ 0
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 : y✝ = loop lt (popMax lt x✝) n✝
⊢ y✝ = loop lt x✝ (n✝ + 1)
Tactic:
rw [IH]
State after:
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 : y✝ = loop lt (popMax lt x✝) n✝
⊢ loop lt (popMax lt x✝) n✝ = loop lt x✝ (n✝ + 1)

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 : y✝ = loop lt (popMax lt x✝) n✝
⊢ loop lt (popMax lt x✝) n✝ = loop lt x✝ (n✝ + 1)
Tactic:
rfl
State after:
no goals