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

State before:
i j k : Nat
hij : i ≤ j
hik : Descendant i k
hjk : Descendant j k
⊢ Descendant i j
Tactic:
induction hjk with
| refl => exact hik
| node_left j _ IH =>
  specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_left j)))
  have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_left j))
  rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at this
  exact this
| node_right j _ IH =>
  specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_right j)))
  have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_right j))
  conv at this =>
    rhs; rw [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left 1 j (by decide)]
    change 0 + j; rw [Nat.zero_add]
  exact this
State after:
no goals

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

State before:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
IH : i ≤ 2 * j + 1 → Descendant i (2 * j + 1)
hij : i ≤ j
⊢ Descendant i j
Tactic:
specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_left j)))
State after:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
⊢ Descendant i j

State before:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
⊢ Descendant i j
Tactic:
have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_left j))
State after:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
this : Descendant i ((2 * j + 1 - 1) / 2)
⊢ Descendant i j

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

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

State before:
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
this : Descendant i (2 * j / 2)
⊢ 0 < 2
Tactic:
decide
State after:
no goals

State before:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
IH : i ≤ 2 * j + 2 → Descendant i (2 * j + 2)
hij : i ≤ j
⊢ Descendant i j
Tactic:
specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_right j)))
State after:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
⊢ Descendant i j

State before:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
⊢ Descendant i j
Tactic:
have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_right j))
State after:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i ((2 * j + 2 - 1) / 2)
⊢ Descendant i j

State before:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i ((2 * j + 2 - 1) / 2)
⊢ Descendant i j
Tactic:
conv at this =>
  rhs; rw [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left 1 j (by decide)]
  change 0 + j; rw [Nat.zero_add]
State after:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i j
⊢ Descendant i j

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

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