Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof 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))
Proof 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)