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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
h : IsHeap lt x i
j₁ j₂ : Fin (Subarray.size x)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
induction h with
| out_of_range _ h => refine .out_of_range _ h
| node' i hi hx₁ hx₂ _ _ IHl IHr =>
  specialize IHl (trans hj₁ (lt_child_left i)) (trans hj₂ (lt_child_left i))
  specialize IHr (trans hj₁ (lt_child_right i)) (trans hj₂ (lt_child_right i))
  refine node' i hi ?_ ?_ IHl IHr
  . intro hl; specialize hx₁ hl
    simp only [Subarray.getElem_swap]
    iterate rewrite [if_neg]
    exact hx₁
    all_goals apply Nat.ne_of_lt
    . exact trans hj₁ (lt_child_left i)
    . exact trans hj₂ (lt_child_left i)
    . exact hj₁
    . exact hj₂
  . intro hr; specialize hx₂ hr
    simp only [Subarray.getElem_swap]
    iterate rewrite [if_neg]
    exact hx₂
    all_goals apply Nat.ne_of_lt
    . exact trans hj₁ (lt_child_right i)
    . exact trans hj₂ (lt_child_right i)
    . exact hj₁
    . exact hj₂
State after:
no goals

State before:
case out_of_range
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
j₁ j₂ : Fin (Subarray.size x)
i✝ : Nat
h : i✝ ≥ Subarray.size x
hj₁ : ↑j₁ < i✝
hj₂ : ↑j₂ < i✝
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i✝
Tactic:
refine .out_of_range _ h
State after:
no goals

State before:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IHl : ↑j₁ < 2 * i + 1 → ↑j₂ < 2 * i + 1 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : ↑j₁ < 2 * i + 2 → ↑j₂ < 2 * i + 2 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
specialize IHl (trans hj₁ (lt_child_left i)) (trans hj₂ (lt_child_left i))
State after:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IHr : ↑j₁ < 2 * i + 2 → ↑j₂ < 2 * i + 2 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i

State before:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IHr : ↑j₁ < 2 * i + 2 → ↑j₂ < 2 * i + 2 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
specialize IHr (trans hj₁ (lt_child_right i)) (trans hj₂ (lt_child_right i))
State after:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i

State before:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
refine node' i hi ?_ ?_ IHl IHr
State after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false

case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false

State before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false

case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
. intro hl; specialize hx₁ hl
  simp only [Subarray.getElem_swap]
  iterate rewrite [if_neg]
  exact hx₁
  all_goals apply Nat.ne_of_lt
  . exact trans hj₁ (lt_child_left i)
  . exact trans hj₂ (lt_child_left i)
  . exact hj₁
  . exact hj₂
State after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false

State before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
. intro hr; specialize hx₂ hr
  simp only [Subarray.getElem_swap]
  iterate rewrite [if_neg]
  exact hx₂
  all_goals apply Nat.ne_of_lt
  . exact trans hj₁ (lt_child_right i)
  . exact trans hj₂ (lt_child_right i)
  . exact hj₁
  . exact hj₂
State after:
no goals

State before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Tactic:
intro hl
State after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false

State before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Tactic:
specialize hx₁ hl
State after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false

State before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Tactic:
simp only [Subarray.getElem_swap]
State after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt (if ↑j₂ = i then x[↑j₁] else if ↑j₁ = i then x[↑j₂] else x[i])
      (if ↑j₂ = 2 * i + 1 then x[↑j₁] else if ↑j₁ = 2 * i + 1 then x[↑j₂] else x[2 * i + 1]) =
    false

State before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt (if ↑j₂ = i then x[↑j₁] else if ↑j₁ = i then x[↑j₂] else x[i])
      (if ↑j₂ = 2 * i + 1 then x[↑j₁] else if ↑j₁ = 2 * i + 1 then x[↑j₂] else x[2 * i + 1]) =
    false
Tactic:
iterate rewrite [if_neg]
State after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt x[i] x[2 * i + 1] = false

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = i

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i

State before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt x[i] x[2 * i + 1] = false

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = i

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i
Tactic:
exact hx₁
State after:
case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = i

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i

State before:
case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = i

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i
Tactic:
all_goals apply Nat.ne_of_lt
State after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < 2 * i + 1

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < 2 * i + 1

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < 2 * i + 1

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < 2 * i + 1

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
. exact trans hj₁ (lt_child_left i)
State after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < 2 * i + 1

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < 2 * i + 1

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
. exact trans hj₂ (lt_child_left i)
State after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
. exact hj₁
State after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
. exact hj₂
State after:
no goals

State before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt x[i] (if ↑j₁ = 2 * i + 1 then x[↑j₂] else x[2 * i + 1]) = false

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = i

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i
Tactic:
rewrite [if_neg]
State after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt x[i] x[2 * i + 1] = false

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = 2 * i + 1

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₁ = i

case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i

State before:
case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i
Tactic:
apply Nat.ne_of_lt
State after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < 2 * i + 1
Tactic:
exact trans hj₁ (lt_child_left i)
State after:
no goals

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < 2 * i + 1
Tactic:
exact trans hj₂ (lt_child_left i)
State after:
no goals

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i
Tactic:
exact hj₁
State after:
no goals

State before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
exact hj₂
State after:
no goals

State before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
intro hr
State after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false

State before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
specialize hx₂ hr
State after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false

State before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
simp only [Subarray.getElem_swap]
State after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt (if ↑j₂ = i then x[↑j₁] else if ↑j₁ = i then x[↑j₂] else x[i])
      (if ↑j₂ = 2 * i + 2 then x[↑j₁] else if ↑j₁ = 2 * i + 2 then x[↑j₂] else x[2 * i + 2]) =
    false

State before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt (if ↑j₂ = i then x[↑j₁] else if ↑j₁ = i then x[↑j₂] else x[i])
      (if ↑j₂ = 2 * i + 2 then x[↑j₁] else if ↑j₁ = 2 * i + 2 then x[↑j₂] else x[2 * i + 2]) =
    false
Tactic:
iterate rewrite [if_neg]
State after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt x[i] x[2 * i + 2] = false

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = i

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = i

State before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt x[i] x[2 * i + 2] = false

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = i

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = i
Tactic:
exact hx₂
State after:
case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = i

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = i

State before:
case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = i

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = i
Tactic:
all_goals apply Nat.ne_of_lt
State after:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < 2 * i + 2

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < 2 * i + 2

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < i

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < 2 * i + 2

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < 2 * i + 2

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < i

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i
Tactic:
. exact trans hj₁ (lt_child_right i)
State after:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < 2 * i + 2

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < i

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < 2 * i + 2

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < i

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i
Tactic:
. exact trans hj₂ (lt_child_right i)
State after:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < i

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < i

case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i
Tactic:
. exact hj₁
State after:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i
Tactic:
. exact hj₂
State after:
no goals

State before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt x[i] (if ↑j₁ = 2 * i + 2 then x[↑j₂] else x[2 * i + 2]) = false

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = i

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = i
Tactic:
rewrite [if_neg]
State after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt x[i] x[2 * i + 2] = false

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = 2 * i + 2

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₁ = i

case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = i

State before:
case node'.refine_2.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ¬↑j₂ = i
Tactic:
apply Nat.ne_of_lt
State after:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < 2 * i + 2
Tactic:
exact trans hj₁ (lt_child_right i)
State after:
no goals

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < 2 * i + 2
Tactic:
exact trans hj₂ (lt_child_right i)
State after:
no goals

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₁ < i
Tactic:
exact hj₁
State after:
no goals

State before:
case node'.refine_2.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ ↑j₂ < i
Tactic:
exact hj₂
State after:
no goals