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

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
⊢ IsHeap lt (BinaryHeap.popMax lt x) 0
Tactic:
dsimp [BinaryHeap.popMax]
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
Tactic:
if hsize : x.start < x.stop then
  simp only [dif_pos hsize]
  refine is_heap_heapifyDown lt _ 0 ?_ ?_
  . refine h.left.of_subext ?_ ?_
    . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
    . intro k hk hki
      rewrite [Subarray.getElem_shrinkOne']
      refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
      . exact Nat.ne_of_lt hki.le
      . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
        simp only [Subarray.size_shrinkOne', Subarray.size_swap]
        exact .refl
  . refine h.right.of_subext ?_ ?_
    . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
    . intro k hk hki
      refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
      . exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
      . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
        simp only [Subarray.size_shrinkOne', Subarray.size_swap]
        exact .refl
else
  simp only [dif_neg hsize]; exact h
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
Tactic:
simp only [dif_pos hsize]
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (heapifyDown lt
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
      0)
    0

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (heapifyDown lt
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
      0)
    0
Tactic:
refine is_heap_heapifyDown lt _ 0 ?_ ?_
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)
Tactic:
. refine h.left.of_subext ?_ ?_
  . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
  . intro k hk hki
    rewrite [Subarray.getElem_shrinkOne']
    refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
    . exact Nat.ne_of_lt hki.le
    . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
      simp only [Subarray.size_shrinkOne', Subarray.size_swap]
      exact .refl
State after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)
Tactic:
. refine h.right.of_subext ?_ ?_
  . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
  . intro k hk hki
    refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
    . exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
    . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
      simp only [Subarray.size_shrinkOne', Subarray.size_swap]
      exact .refl
State after:
no goals

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 1)
Tactic:
refine h.left.of_subext ?_ ?_
State after:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]

State before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
. rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
State after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]

State before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
. intro k hk hki
  rewrite [Subarray.getElem_shrinkOne']
  refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
  . exact Nat.ne_of_lt hki.le
  . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
    simp only [Subarray.size_shrinkOne', Subarray.size_swap]
    exact .refl
State after:
no goals

State before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x
Tactic:
rewrite [Subarray.size_shrinkOne', Subarray.size_swap]
State after:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size x - 1 ≤ Subarray.size x

State before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size x - 1 ≤ Subarray.size x
Tactic:
exact x.size.pred_le
State after:
no goals

State before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
intro k hk hki
State after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)[k] =
    x[k]

State before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)[k] =
    x[k]
Tactic:
rewrite [Subarray.getElem_shrinkOne']
State after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })[k] =
    x[k]

State before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })[k] =
    x[k]
Tactic:
refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
State after:
case refine_1.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k

State before:
case refine_1.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
. exact Nat.ne_of_lt hki.le
State after:
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k

State before:
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
. refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
  simp only [Subarray.size_shrinkOne', Subarray.size_swap]
  exact .refl
State after:
no goals

State before:
case refine_1.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k
Tactic:
exact Nat.ne_of_lt hki.le
State after:
no goals

State before:
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
State after:
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }

State before:
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }
Tactic:
simp only [Subarray.size_shrinkOne', Subarray.size_swap]
State after:
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1

State before:
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1
Tactic:
exact .refl
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)
Tactic:
refine h.right.of_subext ?_ ?_
State after:
case refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x

case refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 2) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]

State before:
case refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x

case refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 2) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
. rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
State after:
case refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 2) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]

State before:
case refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 2) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
. intro k hk hki
  refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
  . exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
  . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
    simp only [Subarray.size_shrinkOne', Subarray.size_swap]
    exact .refl
State after:
no goals

State before:
case refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x
Tactic:
rewrite [Subarray.size_shrinkOne', Subarray.size_swap]
State after:
case refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size x - 1 ≤ Subarray.size x

State before:
case refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size x - 1 ≤ Subarray.size x
Tactic:
exact x.size.pred_le
State after:
no goals

State before:
case refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 2) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
intro k hk hki
State after:
case refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)[k] =
    x[k]

State before:
case refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)[k] =
    x[k]
Tactic:
refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
State after:
case refine_2.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k

State before:
case refine_2.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
. exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
State after:
case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k

State before:
case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
. refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
  simp only [Subarray.size_shrinkOne', Subarray.size_swap]
  exact .refl
State after:
no goals

State before:
case refine_2.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k
Tactic:
exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
State after:
no goals

State before:
case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
State after:
case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }

State before:
case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }
Tactic:
simp only [Subarray.size_shrinkOne', Subarray.size_swap]
State after:
case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1

State before:
case refine_2.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 2) k
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1
Tactic:
exact .refl
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : ¬x.start < x.stop
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
Tactic:
simp only [dif_neg hsize]
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : ¬x.start < x.stop
⊢ IsHeap lt x 0

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : ¬x.start < x.stop
⊢ IsHeap lt x 0
Tactic:
exact h
State after:
no goals