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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ (mkHeap.loop lt x n).start = x.start
Tactic:
induction n generalizing x with
| zero => rfl
| succ n IH => dsimp [mkHeap.loop]; rw [IH, start_heapifyDown]
State after:
no goals

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

State before:
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), (mkHeap.loop lt x n).start = x.start
x : Subarray α
⊢ (mkHeap.loop lt x (Nat.succ n)).start = x.start
Tactic:
dsimp [mkHeap.loop]
State after:
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), (mkHeap.loop lt x n).start = x.start
x : Subarray α
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).start = x.start

State before:
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), (mkHeap.loop lt x n).start = x.start
x : Subarray α
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).start = x.start
Tactic:
rw [IH, start_heapifyDown]
State after:
no goals