internlm/Lean-Github huggingface dataset:
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
intro h
Proof state after:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
constructor
Proof state after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x

case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x

case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro hmem
  have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
  specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
  cases h
Proof state after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro i j
  specialize h i.succ j.succ
  simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
  exact h
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x
Tactic:
intro hmem
Proof state after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
⊢ False
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
⊢ False
Tactic:
have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
Proof state after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
⊢ False
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
⊢ False
Tactic:
specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
Proof state after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
h :
  { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (List.length x.data)) } =
    { val := 0, isLt := (_ : 0 < Nat.succ (size x)) }
⊢ False
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
h :
  { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (List.length x.data)) } =
    { val := 0, isLt := (_ : 0 < Nat.succ (size x)) }
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
intro i j
Proof state after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
i j : Fin (size x)
⊢ x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
i j : Fin (size x)
⊢ x[↑i] = x[↑j] → i = j
Tactic:
specialize h i.succ j.succ
Proof state after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : (cons a x)[↑(Fin.succ i)] = (cons a x)[↑(Fin.succ j)] → Fin.succ i = Fin.succ j
⊢ x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : (cons a x)[↑(Fin.succ i)] = (cons a x)[↑(Fin.succ j)] → Fin.succ i = Fin.succ j
⊢ x[↑i] = x[↑j] → i = j
Tactic:
simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
Proof state after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : x[↑i] = x[↑j] → i = j
⊢ x[↑i] = x[↑j] → i = j
Theorem: Array.nodup_iff_getElem_inj
Proof state before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : x[↑i] = x[↑j] → i = j
⊢ x[↑i] = x[↑j] → i = j
Tactic:
exact h
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
⊢ heapifyDown.OpSpec lt x i (heapifyDown lt x i)
Tactic:
unfold heapifyDown heapifyDownAux
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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]
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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›
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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
Proof 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)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof 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
Proof 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)