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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n k : Nat
hk : k < Array.size (mkHeap.loop lt x n).as
hlt : k < x.start
⊢ (mkHeap.loop lt x n).as[k] = x.as[k]
Tactic:
induction n generalizing x with
| zero => rfl
| succ n IH =>
  dsimp [mkHeap.loop] at hk ⊢
  conv at hk => rw [size_as_mkHeap_loop, size_as_heapifyDown]
  specialize @IH (heapifyDown lt x n)
    ((size_as_mkHeap_loop lt _ n).symm ▸ size_as_heapifyDown lt x n ▸ hk)
    (start_heapifyDown lt x n ▸ hlt)
  rw [IH, get_as_heapifyDown_of_lt_start lt x n k hlt]
State after:
no goals

State before:
case zero
α : Type u
lt : α → α → Bool
k : Nat
x : Subarray α
hk : k < Array.size (mkHeap.loop lt x Nat.zero).as
hlt : k < x.start
⊢ (mkHeap.loop lt x Nat.zero).as[k] = x.as[k]
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH :
  ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k < x.start → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk : k < Array.size (mkHeap.loop lt x (Nat.succ n)).as
hlt : k < x.start
⊢ (mkHeap.loop lt x (Nat.succ n)).as[k] = x.as[k]
Tactic:
dsimp [mkHeap.loop] at hk ⊢
State after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH :
  ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k < x.start → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hlt : k < x.start
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH :
  ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k < x.start → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hlt : k < x.start
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]
Tactic:
conv at hk => rw [size_as_mkHeap_loop, size_as_heapifyDown]
State after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH :
  ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k < x.start → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk✝ : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hk : k < Array.size x.as
hlt : k < x.start
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH :
  ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k < x.start → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk✝ : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hk : k < Array.size x.as
hlt : k < x.start
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]
Tactic:
specialize @IH (heapifyDown lt x n)
  ((size_as_mkHeap_loop lt _ n).symm ▸ size_as_heapifyDown lt x n ▸ hk)
  (start_heapifyDown lt x n ▸ hlt)
State after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
x : Subarray α
hk✝ : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hk : k < Array.size x.as
hlt : k < x.start
IH : (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = (heapifyDown lt x n).as[k]
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
x : Subarray α
hk✝ : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hk : k < Array.size x.as
hlt : k < x.start
IH : (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = (heapifyDown lt x n).as[k]
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]
Tactic:
rw [IH, get_as_heapifyDown_of_lt_start lt x n k hlt]
State after:
no goals