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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n k : Nat
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
Tactic:
induction n generalizing x with
| zero => exact ⟨k,hk,rfl⟩
| succ n IH =>
  dsimp [mkHeap.loop]
  have ⟨l',hl',IH⟩ := IH (heapifyDown lt x n) (size_heapifyDown lt x n ▸ hk)
  simp only [IH]
  exact exists_get_heapifyDown lt x n l' (size_heapifyDown lt x n ▸ hl')
State after:
no goals

State before:
case zero
α : Type u
lt : α → α → Bool
k : Nat
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt x Nat.zero)[k] = x[l]
Tactic:
exact ⟨k,hk,rfl⟩
State after:
no goals

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt x (Nat.succ n))[k] = x[l]
Tactic:
dsimp [mkHeap.loop]
State after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]
Tactic:
have ⟨l',hl',IH⟩ := IH (heapifyDown lt x n) (size_heapifyDown lt x n ▸ hk)
State after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]
Tactic:
simp only [IH]
State after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (heapifyDown lt x n)[l'] = x[l]

State before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (heapifyDown lt x n)[l'] = x[l]
Tactic:
exact exists_get_heapifyDown lt x n l' (size_heapifyDown lt x n ▸ hl')
State after:
no goals