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

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

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

State before:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
⊢ Descendant i ((j - 1) / 2)
Tactic:
have := h.ascend
State after:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : Descendant ((2 * i + 1 - 1) / 2) ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)

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

State before:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : Descendant i ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Tactic:
exact this
State after:
no goals

State before:
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : 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
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
⊢ Descendant i ((j - 1) / 2)
Tactic:
have := h.ascend
State after:
case node_right
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
this : Descendant ((2 * i + 2 - 1) / 2) ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)

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

State before:
case node_right
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
this : Descendant i ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Tactic:
exact this
State after:
no goals

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