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

State before:
i : Nat
⊢ Descendant ((i - 1) / 2) i
Tactic:
cases i with
| zero => exact .refl 0
| succ i =>
  rewrite [Nat.succ_sub_one, Nat.succ_eq_add_one]
  conv => rhs; rewrite [← Nat.div_add_mod i 2]
  cases i.mod_two_eq_zero_or_one with
  | inl hi_even =>
    rewrite [hi_even, Nat.add_zero]; exact .child_left _
  | inr hi_odd =>
    rewrite [hi_odd]; exact .child_right _
State after:
no goals

State before:
case zero

⊢ Descendant ((Nat.zero - 1) / 2) Nat.zero
Tactic:
exact .refl 0
State after:
no goals

State before:
case succ
i : Nat
⊢ Descendant ((Nat.succ i - 1) / 2) (Nat.succ i)
Tactic:
rewrite [Nat.succ_sub_one, Nat.succ_eq_add_one]
State after:
case succ
i : Nat
⊢ Descendant (i / 2) (i + 1)

State before:
case succ
i : Nat
⊢ Descendant (i / 2) (i + 1)
Tactic:
conv => rhs; rewrite [← Nat.div_add_mod i 2]
State after:
case succ
i : Nat
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)

State before:
case succ
i : Nat
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
Tactic:
cases i.mod_two_eq_zero_or_one with
| inl hi_even =>
  rewrite [hi_even, Nat.add_zero]; exact .child_left _
| inr hi_odd =>
  rewrite [hi_odd]; exact .child_right _
State after:
no goals

State before:
case succ.inl
i : Nat
hi_even : i % 2 = 0
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
Tactic:
rewrite [hi_even, Nat.add_zero]
State after:
case succ.inl
i : Nat
hi_even : i % 2 = 0
⊢ Descendant (i / 2) (2 * (i / 2) + 1)

State before:
case succ.inl
i : Nat
hi_even : i % 2 = 0
⊢ Descendant (i / 2) (2 * (i / 2) + 1)
Tactic:
exact .child_left _
State after:
no goals

State before:
case succ.inr
i : Nat
hi_odd : i % 2 = 1
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
Tactic:
rewrite [hi_odd]
State after:
case succ.inr
i : Nat
hi_odd : i % 2 = 1
⊢ Descendant (i / 2) (2 * (i / 2) + 1 + 1)

State before:
case succ.inr
i : Nat
hi_odd : i % 2 = 1
⊢ Descendant (i / 2) (2 * (i / 2) + 1 + 1)
Tactic:
exact .child_right _
State after:
no goals