Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.exists_get (Algdata/Data/BinaryHeap/Basic.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
⊢ ∃ l hl, y[k] = x[l]
Tactic:
if hd : Descendant i k then
  have ⟨l, hl, _, hl'⟩ := h.exists_get_descendant k hk hd
  exact ⟨l, hl, hl'⟩
else
  simp only [h.get_not_descendant k hd]
  exact ⟨k, hk, rfl⟩
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : Descendant i k
⊢ ∃ l hl, y[k] = x[l]
Tactic:
have ⟨l, hl, _, hl'⟩ := h.exists_get_descendant k hk hd
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : Descendant i k
l : Nat
hl : l < Subarray.size x
left✝ : Descendant i l
hl' : y[k] = x[l]
⊢ ∃ l hl, y[k] = x[l]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : Descendant i k
l : Nat
hl : l < Subarray.size x
left✝ : Descendant i l
hl' : y[k] = x[l]
⊢ ∃ l hl, y[k] = x[l]
Tactic:
exact ⟨l, hl, hl'⟩
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : ¬Descendant i k
⊢ ∃ l hl, y[k] = x[l]
Tactic:
simp only [h.get_not_descendant k hd]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : ¬Descendant i k
⊢ ∃ l hl, x[k] = x[l]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : ¬Descendant i k
⊢ ∃ l hl, x[k] = x[l]
Tactic:
exact ⟨k, hk, rfl⟩
State after:
no goals