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

State before:
i : Nat
⊢ Descendant 0 i
Tactic:
induction i using Nat.strongInductionOn
State after:
case ind
n✝ : Nat
a✝ : ∀ (m : Nat), m < n✝ → Descendant 0 m
⊢ Descendant 0 n✝

State before:
case ind
n✝ : Nat
a✝ : ∀ (m : Nat), m < n✝ → Descendant 0 m
⊢ Descendant 0 n✝
Tactic:
rename_i i IH
State after:
case ind
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
⊢ Descendant 0 i

State before:
case ind
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
⊢ Descendant 0 i
Tactic:
cases Nat.eq_zero_or_pos i with
| inl hz => cases hz; exact .refl 0
| inr hpos =>
  specialize IH ((i-1)/2) (gt_parent hpos)
  exact .trans IH (.parent i)
State after:
no goals

State before:
case ind.inl
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
hz : i = 0
⊢ Descendant 0 i
Tactic:
cases hz
State after:
case ind.inl.refl
IH : ∀ (m : Nat), m < 0 → Descendant 0 m
⊢ Descendant 0 0

State before:
case ind.inl.refl
IH : ∀ (m : Nat), m < 0 → Descendant 0 m
⊢ Descendant 0 0
Tactic:
exact .refl 0
State after:
no goals

State before:
case ind.inr
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
hpos : i > 0
⊢ Descendant 0 i
Tactic:
specialize IH ((i-1)/2) (gt_parent hpos)
State after:
case ind.inr
i : Nat
hpos : i > 0
IH : Descendant 0 ((i - 1) / 2)
⊢ Descendant 0 i

State before:
case ind.inr
i : Nat
hpos : i > 0
IH : Descendant 0 ((i - 1) / 2)
⊢ Descendant 0 i
Tactic:
exact .trans IH (.parent i)
State after:
no goals