Theorem: Algdata.BinaryHeap.IsHeap.descend (Algdata/Data/BinaryHeap/Lemmas.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i j : Nat
h : IsHeap lt x i
hd : Descendant i j
⊢ IsHeap lt x j
Tactic:
induction hd with
| refl => exact h
| node_left j _ IH => exact IH h.left
| node_right j _ IH => exact IH h.right
State after:
no goals

State before:
case refl
α : Type u
lt : α → α → Bool
x : Subarray α
i j : Nat
h : IsHeap lt x j
⊢ IsHeap lt x j
Tactic:
exact h
State after:
no goals

State before:
case node_left
α : Type u
lt : α → α → Bool
x : Subarray α
i j✝ j : Nat
h✝ : Descendant (2 * j + 1) j✝
IH : IsHeap lt x (2 * j + 1) → IsHeap lt x j✝
h : IsHeap lt x j
⊢ IsHeap lt x j✝
Tactic:
exact IH h.left
State after:
no goals

State before:
case node_right
α : Type u
lt : α → α → Bool
x : Subarray α
i j✝ j : Nat
h✝ : Descendant (2 * j + 2) j✝
IH : IsHeap lt x (2 * j + 2) → IsHeap lt x j✝
h : IsHeap lt x j
⊢ IsHeap lt x j✝
Tactic:
exact IH h.right
State after:
no goals