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

State before:
k : Nat
motive : (i : Nat) → Descendant i k → Prop
i : Nat
h : Descendant i k
refl : motive k (_ : Descendant k k)
node_left : ∀ (i : Nat) (h : Descendant (2 * i + 1) k), motive (2 * i + 1) h → motive i (_ : Descendant i k)
node_right : ∀ (i : Nat) (h : Descendant (2 * i + 2) k), motive (2 * i + 2) h → motive i (_ : Descendant i k)
⊢ motive i h
Tactic:
induction h with
| refl i => exact refl
| node_left i h IH =>
  exact node_left i h <| IH refl node_left node_right
| node_right i h IH =>
  exact node_right i h <| IH refl node_left node_right
State after:
no goals

State before:
case refl
k i✝ i : Nat
motive : (i_1 : Nat) → Descendant i_1 i → Prop
refl : motive i (_ : Descendant i i)
node_left : ∀ (i_1 : Nat) (h : Descendant (2 * i_1 + 1) i), motive (2 * i_1 + 1) h → motive i_1 (_ : Descendant i_1 i)
node_right : ∀ (i_1 : Nat) (h : Descendant (2 * i_1 + 2) i), motive (2 * i_1 + 2) h → motive i_1 (_ : Descendant i_1 i)
⊢ motive i (_ : Descendant i i)
Tactic:
exact refl
State after:
no goals

State before:
case node_left
k i✝ i k✝ : Nat
h : Descendant (2 * i + 1) k✝
IH :
  ∀ {motive : (i : Nat) → Descendant i k✝ → Prop},
    motive k✝ (_ : Descendant k✝ k✝) →
      (∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)) →
        (∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)) →
          motive (2 * i + 1) h
motive : (i : Nat) → Descendant i k✝ → Prop
refl : motive k✝ (_ : Descendant k✝ k✝)
node_left : ∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)
node_right : ∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)
⊢ motive i (_ : Descendant i k✝)
Tactic:
exact node_left i h <| IH refl node_left node_right
State after:
no goals

State before:
case node_right
k i✝ i k✝ : Nat
h : Descendant (2 * i + 2) k✝
IH :
  ∀ {motive : (i : Nat) → Descendant i k✝ → Prop},
    motive k✝ (_ : Descendant k✝ k✝) →
      (∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)) →
        (∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)) →
          motive (2 * i + 2) h
motive : (i : Nat) → Descendant i k✝ → Prop
refl : motive k✝ (_ : Descendant k✝ k✝)
node_left : ∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)
node_right : ∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)
⊢ motive i (_ : Descendant i k✝)
Tactic:
exact node_right i h <| IH refl node_left node_right
State after:
no goals