Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap (Algdata/Data/BinaryHeap/Lemmas.lean)

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
⊢ IsHeap lt y i
Tactic:
let _hy_left := fun hl => h.not_lt_left hl heap_left
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false := fun hl => not_lt_left h hl heap_left
⊢ IsHeap lt y i

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false := fun hl => not_lt_left h hl heap_left
⊢ IsHeap lt y i
Tactic:
let _hy_right := fun hr => h.not_lt_right hr heap_right
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false := fun hl => not_lt_left h hl heap_left
_hy_right : ∀ (hr : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false := fun hr => not_lt_right h hr heap_right
⊢ IsHeap lt y i

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false := fun hl => not_lt_left h hl heap_left
_hy_right : ∀ (hr : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false := fun hr => not_lt_right h hr heap_right
⊢ IsHeap lt y i
Tactic:
induction h with
| node_next_left x i y hi hl hr hx' hx h IH =>
  refine .node lt y i (h.size_eq ▸ hr) (_hy_left hl) (_hy_right hr) ?_ ?_
  . show IsHeap lt y (2*i+1)
    refine IH ?_ ?_
    . refine heap_left.left.swap _ _ ?_ (lt_child_left (2*i+1))
      exact trans (lt_child_left i) (lt_child_left (2*i+1))
    . refine heap_left.right.swap _ _ ?_ (lt_child_right (2*i+1))
      exact trans (lt_child_left i) (lt_child_right (2*i+1))
  . show IsHeap lt y (2*i+2)
    refine heap_right.of_subext (h.size_eq ▸ .refl) ?_
    intro k hk hdk
    rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| h.ascend_right (.step .refl) hdk, Subarray.getElem_swap_ne]
    . exact Nat.ne_of_lt <| trans (lt_child_right i) hdk.le
    . exact Nat.ne_of_lt <| trans (2*i+1).lt_succ_self hdk.le
| node_end_left x i _ hl hr hx' hx =>
  refine .node lt x i hr hx ?_ heap_left heap_right
  exact LawfulLTBRel.ntrans hx <| LawfulLTBRel.asymm hx'
| node_next_right x i y hi hl hr hx' hx h IH =>
  refine .node lt y i (h.size_eq ▸ hr) (_hy_left hl) (_hy_right hr) ?_ ?_
  . show IsHeap lt y (2*i+1)
    refine heap_left.of_subext (h.size_eq ▸ .refl) ?_
    intro k hk hdk
    rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| hdk.ascend_right (.step .refl) h, Subarray.getElem_swap_ne]
    . exact Nat.ne_of_lt <| trans (lt_child_left i) hdk.le
    . dsimp; intro h; cases h; exact absurd hdk (Descendant.sibling_not i)
  . show IsHeap lt y (2*i+2)
    refine IH ?_ ?_
    . refine heap_right.left.swap _ _ ?_ (lt_child_left (2*i+2))
      exact trans (lt_child_right i) (lt_child_left (2*i+2))
    . refine heap_right.right.swap _ _ ?_ (lt_child_right (2*i+2))
      exact trans (lt_child_right i) (lt_child_right (2*i+2))
| node_end_right x i _ _ hr hx' hx =>
  exact .node lt x i hr (LawfulLTBRel.ntrans hx hx') hx heap_left heap_right
| node_odd_next x i hi hl hr hx =>
  refine .node_odd lt _ i hl hr ?_
  rewrite [Subarray.getElem_swap_left, Subarray.getElem_swap_right]
  exact LawfulLTBRel.asymm hx
| node_odd_end x i _ hl hr hx =>
  exact .node_odd lt x i hl hr hx
| leaf x i hl => exact .leaf lt x i hl
State after:
no goals

State before:
case node_next_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y i
Tactic:
refine .node lt y i (h.size_eq ▸ hr) (_hy_left hl) (_hy_right hr) ?_ ?_
State after:
case node_next_left.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 1)

case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)

State before:
case node_next_left.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 1)

case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)
Tactic:
. show IsHeap lt y (2*i+1)
  refine IH ?_ ?_
  . refine heap_left.left.swap _ _ ?_ (lt_child_left (2*i+1))
    exact trans (lt_child_left i) (lt_child_left (2*i+1))
  . refine heap_left.right.swap _ _ ?_ (lt_child_right (2*i+1))
    exact trans (lt_child_left i) (lt_child_right (2*i+1))
State after:
case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)

State before:
case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)
Tactic:
. show IsHeap lt y (2*i+2)
  refine heap_right.of_subext (h.size_eq ▸ .refl) ?_
  intro k hk hdk
  rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| h.ascend_right (.step .refl) hdk, Subarray.getElem_swap_ne]
  . exact Nat.ne_of_lt <| trans (lt_child_right i) hdk.le
  . exact Nat.ne_of_lt <| trans (2*i+1).lt_succ_self hdk.le
State after:
no goals

State before:
case node_next_left.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 1)
Tactic:
refine IH ?_ ?_
State after:
case node_next_left.refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1)

case node_next_left.refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)

State before:
case node_next_left.refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1)

case node_next_left.refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)
Tactic:
. refine heap_left.left.swap _ _ ?_ (lt_child_left (2*i+1))
  exact trans (lt_child_left i) (lt_child_left (2*i+1))
State after:
case node_next_left.refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)

State before:
case node_next_left.refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)
Tactic:
. refine heap_left.right.swap _ _ ?_ (lt_child_right (2*i+1))
  exact trans (lt_child_left i) (lt_child_right (2*i+1))
State after:
no goals

State before:
case node_next_left.refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1)
Tactic:
refine heap_left.left.swap _ _ ?_ (lt_child_left (2*i+1))
State after:
case node_next_left.refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 1) + 1

State before:
case node_next_left.refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 1) + 1
Tactic:
exact trans (lt_child_left i) (lt_child_left (2*i+1))
State after:
no goals

State before:
case node_next_left.refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)
Tactic:
refine heap_left.right.swap _ _ ?_ (lt_child_right (2*i+1))
State after:
case node_next_left.refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 1) + 2

State before:
case node_next_left.refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 1) + 2
Tactic:
exact trans (lt_child_left i) (lt_child_right (2*i+1))
State after:
no goals

State before:
case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)
Tactic:
refine heap_right.of_subext (h.size_eq ▸ .refl) ?_
State after:
case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]

State before:
case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]
Tactic:
intro k hk hdk
State after:
case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ y[k] = x[k]

State before:
case node_next_left.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ y[k] = x[k]
Tactic:
rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| h.ascend_right (.step .refl) hdk, Subarray.getElem_swap_ne]
State after:
case node_next_left.refine_2.hik
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := i, isLt := hi } ≠ k

case node_next_left.refine_2.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := 2 * i + 1, isLt := hl } ≠ k

State before:
case node_next_left.refine_2.hik
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := i, isLt := hi } ≠ k

case node_next_left.refine_2.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := 2 * i + 1, isLt := hl } ≠ k
Tactic:
. exact Nat.ne_of_lt <| trans (lt_child_right i) hdk.le
State after:
case node_next_left.refine_2.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := 2 * i + 1, isLt := hl } ≠ k

State before:
case node_next_left.refine_2.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := 2 * i + 1, isLt := hl } ≠ k
Tactic:
. exact Nat.ne_of_lt <| trans (2*i+1).lt_succ_self hdk.le
State after:
no goals

State before:
case node_next_left.refine_2.hik
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := i, isLt := hi } ≠ k
Tactic:
exact Nat.ne_of_lt <| trans (lt_child_right i) hdk.le
State after:
no goals

State before:
case node_next_left.refine_2.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * (2 * i + 1) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl_1 :
            2 * (2 * i + 1) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr :
            2 * (2 * i + 1) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })),
          lt y[2 * i + 1] y[2 * (2 * i + 1) + 2] = false);
    IsHeap lt y (2 * i + 1)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_left x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_left x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 2) k
⊢ ↑{ val := 2 * i + 1, isLt := hl } ≠ k
Tactic:
exact Nat.ne_of_lt <| trans (2*i+1).lt_succ_self hdk.le
State after:
no goals

State before:
case node_end_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi✝ : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = false
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_end_left x i hi✝ hl hr hx' hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_end_left x i hi✝ hl hr hx' hx) hr_1 heap_right
⊢ IsHeap lt x i
Tactic:
refine .node lt x i hr hx ?_ heap_left heap_right
State after:
case node_end_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi✝ : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = false
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_end_left x i hi✝ hl hr hx' hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_end_left x i hi✝ hl hr hx' hx) hr_1 heap_right
⊢ lt x[i] x[2 * i + 2] = false

State before:
case node_end_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi✝ : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = false
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_end_left x i hi✝ hl hr hx' hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_end_left x i hi✝ hl hr hx' hx) hr_1 heap_right
⊢ lt x[i] x[2 * i + 2] = false
Tactic:
exact LawfulLTBRel.ntrans hx <| LawfulLTBRel.asymm hx'
State after:
no goals

State before:
case node_next_right
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y i
Tactic:
refine .node lt y i (h.size_eq ▸ hr) (_hy_left hl) (_hy_right hr) ?_ ?_
State after:
case node_next_right.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 1)

case node_next_right.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)

State before:
case node_next_right.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 1)

case node_next_right.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)
Tactic:
. show IsHeap lt y (2*i+1)
  refine heap_left.of_subext (h.size_eq ▸ .refl) ?_
  intro k hk hdk
  rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| hdk.ascend_right (.step .refl) h, Subarray.getElem_swap_ne]
  . exact Nat.ne_of_lt <| trans (lt_child_left i) hdk.le
  . dsimp; intro h; cases h; exact absurd hdk (Descendant.sibling_not i)
State after:
case node_next_right.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)

State before:
case node_next_right.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)
Tactic:
. show IsHeap lt y (2*i+2)
  refine IH ?_ ?_
  . refine heap_right.left.swap _ _ ?_ (lt_child_left (2*i+2))
    exact trans (lt_child_right i) (lt_child_left (2*i+2))
  . refine heap_right.right.swap _ _ ?_ (lt_child_right (2*i+2))
    exact trans (lt_child_right i) (lt_child_right (2*i+2))
State after:
no goals

State before:
case node_next_right.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 1)
Tactic:
refine heap_left.of_subext (h.size_eq ▸ .refl) ?_
State after:
case node_next_right.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 1) k → y[k] = x[k]

State before:
case node_next_right.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 1) k → y[k] = x[k]
Tactic:
intro k hk hdk
State after:
case node_next_right.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ y[k] = x[k]

State before:
case node_next_right.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ y[k] = x[k]
Tactic:
rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| hdk.ascend_right (.step .refl) h, Subarray.getElem_swap_ne]
State after:
case node_next_right.refine_1.hik
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := i, isLt := hi } ≠ k

case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := 2 * i + 2, isLt := hr } ≠ k

State before:
case node_next_right.refine_1.hik
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := i, isLt := hi } ≠ k

case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := 2 * i + 2, isLt := hr } ≠ k
Tactic:
. exact Nat.ne_of_lt <| trans (lt_child_left i) hdk.le
State after:
case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := 2 * i + 2, isLt := hr } ≠ k

State before:
case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := 2 * i + 2, isLt := hr } ≠ k
Tactic:
. dsimp; intro h; cases h; exact absurd hdk (Descendant.sibling_not i)
State after:
no goals

State before:
case node_next_right.refine_1.hik
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := i, isLt := hi } ≠ k
Tactic:
exact Nat.ne_of_lt <| trans (lt_child_left i) hdk.le
State after:
no goals

State before:
case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ↑{ val := 2 * i + 2, isLt := hr } ≠ k
Tactic:
dsimp
State after:
case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ¬2 * i + 2 = k

State before:
case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
⊢ ¬2 * i + 2 = k
Tactic:
intro h
State after:
case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h✝) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h✝) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
h : 2 * i + 2 = k
⊢ False

State before:
case node_next_right.refine_1.hjk
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h✝) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h✝) hr_1 heap_right
k : Nat
hk : k < Subarray.size y
hdk : Descendant (2 * i + 1) k
h : 2 * i + 2 = k
⊢ False
Tactic:
cases h
State after:
case node_next_right.refine_1.hjk.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
hk : 2 * i + 2 < Subarray.size y
hdk : Descendant (2 * i + 1) (2 * i + 2)
⊢ False

State before:
case node_next_right.refine_1.hjk.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
hk : 2 * i + 2 < Subarray.size y
hdk : Descendant (2 * i + 1) (2 * i + 2)
⊢ False
Tactic:
exact absurd hdk (Descendant.sibling_not i)
State after:
no goals

State before:
case node_next_right.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt y (2 * i + 2)
Tactic:
refine IH ?_ ?_
State after:
case node_next_right.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1)

case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)

State before:
case node_next_right.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1)

case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)
Tactic:
. refine heap_right.left.swap _ _ ?_ (lt_child_left (2*i+2))
  exact trans (lt_child_right i) (lt_child_left (2*i+2))
State after:
case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)

State before:
case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)
Tactic:
. refine heap_right.right.swap _ _ ?_ (lt_child_right (2*i+2))
  exact trans (lt_child_right i) (lt_child_right (2*i+2))
State after:
no goals

State before:
case node_next_right.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1)
Tactic:
refine heap_right.left.swap _ _ ?_ (lt_child_left (2*i+2))
State after:
case node_next_right.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 2) + 1

State before:
case node_next_right.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 2) + 1
Tactic:
exact trans (lt_child_right i) (lt_child_left (2*i+2))
State after:
no goals

State before:
case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)
Tactic:
refine heap_right.right.swap _ _ ?_ (lt_child_right (2*i+2))
State after:
case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 2) + 2

State before:
case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 2) + 2
Tactic:
exact trans (lt_child_right i) (lt_child_right (2*i+2))
State after:
no goals

State before:
case node_end_right
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi✝ : i < Subarray.size x
hl✝ : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = false
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl => not_lt_left (node_end_right x i hi✝ hl✝ hr hx' hx) hl heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_end_right x i hi✝ hl✝ hr hx' hx) hr_1 heap_right
⊢ IsHeap lt x i
Tactic:
exact .node lt x i hr (LawfulLTBRel.ntrans hx hx') hx heap_left heap_right
State after:
no goals

State before:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = true
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) i
Tactic:
refine .node_odd lt _ i hl hr ?_
State after:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = true
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false

State before:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = true
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false
Tactic:
rewrite [Subarray.getElem_swap_left, Subarray.getElem_swap_right]
State after:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = true
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt x[↑{ val := 2 * i + 1, isLt := hl }] x[↑{ val := i, isLt := hi }] = false

State before:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = true
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt x[↑{ val := 2 * i + 1, isLt := hl }] x[↑{ val := i, isLt := hi }] = false
Tactic:
exact LawfulLTBRel.asymm hx
State after:
no goals

State before:
case node_odd_end
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi✝ : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_odd_end x i hi✝ hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_odd_end x i hi✝ hl hr hx) hr_1 heap_right
⊢ IsHeap lt x i
Tactic:
exact .node_odd lt x i hl hr hx
State after:
no goals

State before:
case leaf
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (leaf x i hl) hl_1 heap_left
_hy_right : ∀ (hr : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr => not_lt_right (leaf x i hl) hr heap_right
⊢ IsHeap lt x i
Tactic:
exact .leaf lt x i hl
State after:
no goals