Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk (Algdata/Data/BinaryHeap/Basic.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
⊢ heapifyDown.OpSpec lt x i (heapifyDown lt x i)
Tactic:
unfold heapifyDown heapifyDownAux
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
⊢ heapifyDown.OpSpec lt x i
    (let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
⊢ heapifyDown.OpSpec lt x i
    (let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
takeout_lets
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
⊢ let lhs := 2 * i + 1;
  let rhs := lhs + 1;
  heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
⊢ let lhs := 2 * i + 1;
  let rhs := lhs + 1;
  heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
intro_let
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
⊢ let rhs := lhs + 1;
  heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
⊢ let rhs := lhs + 1;
  heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
intro_let
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
if hr : rhs < x.size then
  simp (config:={zeta:=false,beta:=false}) only [dif_pos hr]
  takeout_lets; iterate intro_let
  have _hdecreasing := ‹x.size - j < x.size - i›
  have IH := OpSpec.mk (x.swap ⟨i,hi⟩ ⟨j,hj.2⟩) j
  if hx' : lt x[rhs] x[lhs] then
    have hjl : j = lhs := if_pos hx'
    simp (config:={zeta:=false}) only [hjl] at IH ⊢
    if hx : lt x[i] x[lhs] then
      simp only [if_pos hx]
      exact node_next_left x i _ hi hl hr hx' hx IH
    else
      simp only [if_neg hx]
      exact node_end_left x i hi hl hr hx' (Bool.of_not_eq_true hx)
  else
    have hjr : j = rhs := if_neg hx'
    simp (config:={zeta:=false}) only [hjr] at IH ⊢
    if hx : lt x[i] x[rhs] then
      simp only [if_pos hx]
      exact node_next_right x i _ hi hl hr (Bool.of_not_eq_true hx') hx IH
    else
      simp only [if_neg hx]
      exact node_end_right x i hi hl hr (Bool.of_not_eq_true hx') (Bool.of_not_eq_true hx)
else if hl : lhs < x.size then
  simp (config:={zeta:=false,beta:=false}) only [dif_neg hr, dif_pos hl]
  takeout_lets; intro_let
  if hx : lt x[i] x[lhs] then
    simp only [if_pos hx]
    exact node_odd_next x i hi hl (Nat.le_of_not_lt hr) hx
  else
    simp only [if_neg hx]
    exact node_odd_end x i hi hl (Nat.le_of_not_lt hr) (Bool.of_not_eq_true hx)
else
  simp only [dif_neg hr, dif_neg hl]
  exact leaf x i (Nat.le_of_not_lt hl)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
simp (config:={zeta:=false,beta:=false}) only [dif_pos hr]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (let_fun hi := (_ : i < Subarray.size x);
    let_fun hl := (_ : lhs < Subarray.size x);
    let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
    let_fun hj := (_ : i < j ∧ j < Subarray.size x);
    if lt x[i] x[j] = true then
      let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (let_fun hi := (_ : i < Subarray.size x);
    let_fun hl := (_ : lhs < Subarray.size x);
    let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
    let_fun hj := (_ : i < j ∧ j < Subarray.size x);
    if lt x[i] x[j] = true then
      let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
takeout_lets
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
⊢ let_fun hi := (_ : i < Subarray.size x);
  let_fun hl := (_ : lhs < Subarray.size x);
  let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
  let_fun hj := (_ : i < j ∧ j < Subarray.size x);
  let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
  heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
⊢ let_fun hi := (_ : i < Subarray.size x);
  let_fun hl := (_ : lhs < Subarray.size x);
  let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
  let_fun hj := (_ : i < j ∧ j < Subarray.size x);
  let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
  heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
iterate intro_let
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this : Subarray.size x - j < Subarray.size x - i
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this : Subarray.size x - j < Subarray.size x - i
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
have _hdecreasing := ‹x.size - j < x.size - i›
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
have IH := OpSpec.mk (x.swap ⟨i,hi⟩ ⟨j,hj.2⟩) j
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
if hx' : lt x[rhs] x[lhs] then
  have hjl : j = lhs := if_pos hx'
  simp (config:={zeta:=false}) only [hjl] at IH ⊢
  if hx : lt x[i] x[lhs] then
    simp only [if_pos hx]
    exact node_next_left x i _ hi hl hr hx' hx IH
  else
    simp only [if_neg hx]
    exact node_end_left x i hi hl hr hx' (Bool.of_not_eq_true hx)
else
  have hjr : j = rhs := if_neg hx'
  simp (config:={zeta:=false}) only [hjr] at IH ⊢
  if hx : lt x[i] x[rhs] then
    simp only [if_pos hx]
    exact node_next_right x i _ hi hl hr (Bool.of_not_eq_true hx') hx IH
  else
    simp only [if_neg hx]
    exact node_end_right x i hi hl hr (Bool.of_not_eq_true hx') (Bool.of_not_eq_true hx)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
⊢ let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
  heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
intro_let
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this : Subarray.size x - j < Subarray.size x - i
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : lt x[rhs] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
have hjl : j = lhs := if_pos hx'
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
simp (config:={zeta:=false}) only [hjl] at IH ⊢
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)
Tactic:
if hx : lt x[i] x[lhs] then
  simp only [if_pos hx]
  exact node_next_left x i _ hi hl hr hx' hx IH
else
  simp only [if_neg hx]
  exact node_end_left x i hi hl hr hx' (Bool.of_not_eq_true hx)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)
Tactic:
simp only [if_pos hx]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := (_ : lhs < Subarray.size x) }) (2 * i + 1))

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := (_ : lhs < Subarray.size x) }) (2 * i + 1))
Tactic:
exact node_next_left x i _ hi hl hr hx' hx IH
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)
Tactic:
simp only [if_neg hx]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i x

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i x
Tactic:
exact node_end_left x i hi hl hr hx' (Bool.of_not_eq_true hx)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : ¬lt x[rhs] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
have hjr : j = rhs := if_neg hx'
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
simp (config:={zeta:=false}) only [hjr] at IH ⊢
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)
Tactic:
if hx : lt x[i] x[rhs] then
  simp only [if_pos hx]
  exact node_next_right x i _ hi hl hr (Bool.of_not_eq_true hx') hx IH
else
  simp only [if_neg hx]
  exact node_end_right x i hi hl hr (Bool.of_not_eq_true hx') (Bool.of_not_eq_true hx)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)
Tactic:
simp only [if_pos hx]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1 + 1, isLt := (_ : rhs < Subarray.size x) })
      (2 * i + 1 + 1))

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1 + 1, isLt := (_ : rhs < Subarray.size x) })
      (2 * i + 1 + 1))
Tactic:
exact node_next_right x i _ hi hl hr (Bool.of_not_eq_true hx') hx IH
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : ¬lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)
Tactic:
simp only [if_neg hx]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : ¬lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i x

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : ¬lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i x
Tactic:
exact node_end_right x i hi hl hr (Bool.of_not_eq_true hx') (Bool.of_not_eq_true hx)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
if hl : lhs < x.size then
simp (config:={zeta:=false,beta:=false}) only [dif_neg hr, dif_pos hl]
takeout_lets; intro_let
if hx : lt x[i] x[lhs] then
simp only [if_pos hx]
exact node_odd_next x i hi hl (Nat.le_of_not_lt hr) hx
else
simp only [if_neg hx]
exact node_odd_end x i hi hl (Nat.le_of_not_lt hr) (Bool.of_not_eq_true hx)
else
simp only [dif_neg hr, dif_neg hl]
exact leaf x i (Nat.le_of_not_lt hl)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
simp (config:={zeta:=false,beta:=false}) only [dif_neg hr, dif_pos hl]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (let_fun hi := (_ : i < Subarray.size x);
    if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (let_fun hi := (_ : i < Subarray.size x);
    if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Tactic:
takeout_lets
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ let_fun hi := (_ : i < Subarray.size x);
  heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ let_fun hi := (_ : i < Subarray.size x);
  heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Tactic:
intro_let
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Tactic:
if hx : lt x[i] x[lhs] then
  simp only [if_pos hx]
  exact node_odd_next x i hi hl (Nat.le_of_not_lt hr) hx
else
  simp only [if_neg hx]
  exact node_odd_end x i hi hl (Nat.le_of_not_lt hr) (Bool.of_not_eq_true hx)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Tactic:
simp only [if_pos hx]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })
Tactic:
exact node_odd_next x i hi hl (Nat.le_of_not_lt hr) hx
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Tactic:
simp only [if_neg hx]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i x

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i x
Tactic:
exact node_odd_end x i hi hl (Nat.le_of_not_lt hr) (Bool.of_not_eq_true hx)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : ¬lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
simp only [dif_neg hr, dif_neg hl]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : ¬lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i x

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : ¬lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i x
Tactic:
exact leaf x i (Nat.le_of_not_lt hl)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
_x✝ : (_ : Subarray α) ×' Nat
a✝¹ :
  ∀ (y : (_ : Subarray α) ×' Nat),
    (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1 y _x✝ →
      heapifyDown.OpSpec lt y.1 y.2 (heapifyDown lt y.1 y.2)
x : Subarray α
i : Nat
a✝ :
  ∀ (y : (_ : Subarray α) ×' Nat),
    (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1 y
        { fst := x, snd := i } →
      heapifyDown.OpSpec lt y.1 y.2 (heapifyDown lt y.1 y.2)
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
j : Nat := if h : lt x[rhs] x[lhs] = true then lhs else rhs
_hdecreasing : Subarray.size x - j < Subarray.size x - i
⊢ (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1
    {
      fst :=
        Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) } { val := j, isLt := (_ : j < Subarray.size x) },
      snd := j }
    { fst := x, snd := i }
Tactic:
exact _hdecreasing
State after:
no goals