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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ mkHeap lt x = Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x
Tactic:
unfold mkHeap
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ mkHeap.loop lt x (Subarray.size x / 2) = Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ mkHeap.loop lt x (Subarray.size x / 2) = Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x
Tactic:
generalize x.size/2 = n
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ mkHeap.loop lt x n = Nat.foldRev (fun n x => heapifyDown lt x n) n x

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

State before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ mkHeap.loop lt x Nat.zero = Nat.foldRev (fun n x => heapifyDown lt x n) Nat.zero x
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), mkHeap.loop lt x n = Nat.foldRev (fun n x => heapifyDown lt x n) n x
x : Subarray α
⊢ mkHeap.loop lt x (Nat.succ n) = Nat.foldRev (fun n x => heapifyDown lt x n) (Nat.succ n) x
Tactic:
exact IH (heapifyDown lt x n)
State after:
no goals