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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i k : Nat
hk : k < Subarray.size (heapifyDown lt x i)
hki : k < i
⊢ (heapifyDown lt x i)[k] = x[k]
Tactic:
refine get_heapifyDown_not_descendant lt x i k ?_
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i k : Nat
hk : k < Subarray.size (heapifyDown lt x i)
hki : k < i
⊢ ¬Descendant i k

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i k : Nat
hk : k < Subarray.size (heapifyDown lt x i)
hki : k < i
⊢ ¬Descendant i k
Tactic:
intro h
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i k : Nat
hk : k < Subarray.size (heapifyDown lt x i)
hki : k < i
h : Descendant i k
⊢ False

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i k : Nat
hk : k < Subarray.size (heapifyDown lt x i)
hki : k < i
h : Descendant i k
⊢ False
Tactic:
exact absurd h.le (Nat.not_le_of_gt hki)
State after:
no goals