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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
⊢ y = heapifyDown lt x i
Tactic:
induction h with
| node_next_left x i y hi hl hr hx' hx _ IH =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_pos hx', if_pos hx]
  exact IH
| node_end_left x i hi hl hr hx' hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_pos hx', if_neg (Bool.eq_false_iff.mp hx)]
| node_next_right x i y hi hl hr hx' hx _ IH =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_pos hx]
  exact IH
| node_end_right x i hi hl hr hx' hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_neg (Bool.eq_false_iff.mp hx)]
| node_odd_next x i hi hl hr hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_pos hx]
| node_odd_end x i hi hl hr hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_neg (Bool.eq_false_iff.mp hx)]
| leaf x i hl =>
  have hr : 2*i+2 ≥ x.size := .step hl
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_neg (Nat.not_lt_of_le hl)]
State after:
no goals

State before:
case node_next_left
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
State after:
case node_next_left
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    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:
case node_next_left
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    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:
simp only [dif_pos hr, if_pos hx', if_pos hx]
State after:
case node_next_left
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1, isLt := (_ : 2 * i + 1 < Subarray.size x) })
      (2 * i + 1)

State before:
case node_next_left
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1, isLt := (_ : 2 * i + 1 < Subarray.size x) })
      (2 * i + 1)
Tactic:
exact IH
State after:
no goals

State before:
case node_end_left
α : Type u
lt : α → α → Bool
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
⊢ x = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
State after:
case node_end_left
α : Type u
lt : α → α → Bool
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
⊢ x =
    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:
case node_end_left
α : Type u
lt : α → α → Bool
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
⊢ x =
    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:
simp only [dif_pos hr, if_pos hx', if_neg (Bool.eq_false_iff.mp hx)]
State after:
no goals

State before:
case node_next_right
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
State after:
case node_next_right
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    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:
case node_next_right
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    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:
simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_pos hx]
State after:
case node_next_right
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1 + 1, isLt := (_ : 2 * i + 1 + 1 < Subarray.size x) })
      (2 * i + 1 + 1)

State before:
case node_next_right
α : Type u
lt : α → α → Bool
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
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1 + 1, isLt := (_ : 2 * i + 1 + 1 < Subarray.size x) })
      (2 * i + 1 + 1)
Tactic:
exact IH
State after:
no goals

State before:
case node_end_right
α : Type u
lt : α → α → Bool
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
⊢ x = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
State after:
case node_end_right
α : Type u
lt : α → α → Bool
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
⊢ x =
    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:
case node_end_right
α : Type u
lt : α → α → Bool
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
⊢ x =
    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:
simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_neg (Bool.eq_false_iff.mp hx)]
State after:
no goals

State before:
case node_odd_next
α : Type u
lt : α → α → Bool
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
⊢ Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl } = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
State after:
case node_odd_next
α : Type u
lt : α → α → Bool
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
⊢ Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl } =
    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:
case node_odd_next
α : Type u
lt : α → α → Bool
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
⊢ Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl } =
    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:
simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_pos hx]
State after:
no goals

State before:
case node_odd_end
α : Type u
lt : α → α → Bool
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
⊢ x = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
State after:
case node_odd_end
α : Type u
lt : α → α → Bool
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
⊢ x =
    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:
case node_odd_end
α : Type u
lt : α → α → Bool
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
⊢ x =
    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:
simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_neg (Bool.eq_false_iff.mp hx)]
State after:
no goals

State before:
case leaf
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
⊢ x = heapifyDown lt x i
Tactic:
have hr : 2*i+2 ≥ x.size := .step hl
State after:
case leaf
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ x = heapifyDown lt x i

State before:
case leaf
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ x = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
State after:
case leaf
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ x =
    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:
case leaf
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ x =
    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:
simp only [dif_neg (Nat.not_lt_of_le hr), dif_neg (Nat.not_lt_of_le hl)]
State after:
no goals