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

State before:
i j : Nat
h : Descendant i j
⊢ Descendant ((i - 1) / 2) ((j - 1) / 2)
Tactic:
induction h with
| refl => exact .refl _
| node_left i' _ IH =>
  rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at IH
  exact .trans (.parent i') IH
| node_right i' _ IH =>
  rewrite [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left _ _ (by decide)] at IH
  conv at IH =>
    lhs; change 0 + i'; rewrite [Nat.zero_add]
  exact .trans (.parent i') IH
State after:
no goals

State before:
case refl
i j : Nat
⊢ Descendant ((j - 1) / 2) ((j - 1) / 2)
Tactic:
exact .refl _
State after:
no goals

State before:
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant ((2 * i' + 1 - 1) / 2) ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at IH
State after:
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)

State before:
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
exact .trans (.parent i') IH
State after:
no goals

State before:
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant (2 * i' / 2) ((j - 1) / 2)
⊢ 0 < 2
Tactic:
decide
State after:
no goals

State before:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant ((2 * i' + 2 - 1) / 2) ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
rewrite [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left _ _ (by decide)] at IH
State after:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant (1 / 2 + i') ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)

State before:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant (1 / 2 + i') ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
conv at IH =>
  lhs; change 0 + i'; rewrite [Nat.zero_add]
State after:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)

State before:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
exact .trans (.parent i') IH
State after:
no goals

State before:
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant ((1 + 2 * i') / 2) ((j - 1) / 2)
⊢ 0 < 2
Tactic:
decide
State after:
no goals