Theorem: Algdata.BinaryHeap.Descendant.trans (Algdata/Data/BinaryHeap/Index.lean)

State before:
i j k : Nat
hij : Descendant i j
hjk : Descendant j k
⊢ Descendant i k
Tactic:
induction hij with
| refl => exact hjk
| node_left i _ IH => exact .node_left i IH
| node_right i _ IH => exact .node_right i IH
State after:
no goals

State before:
case refl
i j k : Nat
hjk : Descendant j k
⊢ Descendant j k
Tactic:
exact hjk
State after:
no goals

State before:
case node_left
i✝ j k : Nat
hjk : Descendant j k
i : Nat
h✝ : Descendant (2 * i + 1) j
IH : Descendant (2 * i + 1) k
⊢ Descendant i k
Tactic:
exact .node_left i IH
State after:
no goals

State before:
case node_right
i✝ j k : Nat
hjk : Descendant j k
i : Nat
h✝ : Descendant (2 * i + 2) j
IH : Descendant (2 * i + 2) k
⊢ Descendant i k
Tactic:
exact .node_right i IH
State after:
no goals