Theorem: Algdata.BinaryHeap.IsHeap.node_odd (Algdata/Data/BinaryHeap/Lemmas.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ IsHeap lt x i
Tactic:
have hleft : IsHeap lt x (2*i+1) := by
  refine .leaf lt x _ (Nat.le_trans hr ?_)
  conv =>
    rhs
    rewrite [Nat.two_mul (2*i+1), Nat.add_assoc _ _ 1, Nat.add_comm (2*i+1) 1, ←Nat.add_assoc _ 1 _]
    change 2*i+2+(2*i+1)
  exact Nat.le_add_right (2*i+2) (2*i+1)
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
⊢ IsHeap lt x i

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
⊢ IsHeap lt x i
Tactic:
have hright : IsHeap lt x (2*i+2) :=
  .out_of_range _ hr
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ IsHeap lt x i

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ IsHeap lt x i
Tactic:
refine .node' i _ (fun _ => hx) ?_ hleft hright
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
. intro hr'; exact absurd hr' (Nat.not_lt_of_le hr)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ IsHeap lt x (2 * i + 1)
Tactic:
refine .leaf lt x _ (Nat.le_trans hr ?_)
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * (2 * i + 1) + 1

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * (2 * i + 1) + 1
Tactic:
conv =>
  rhs
  rewrite [Nat.two_mul (2*i+1), Nat.add_assoc _ _ 1, Nat.add_comm (2*i+1) 1, ←Nat.add_assoc _ 1 _]
  change 2*i+2+(2*i+1)
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * i + 2 + (2 * i + 1)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * i + 2 + (2 * i + 1)
Tactic:
exact Nat.le_add_right (2*i+2) (2*i+1)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
intro hr'
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false
Tactic:
exact absurd hr' (Nat.not_lt_of_le hr)
State after:
no goals