internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (Array.swap x.as (Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) })
        (Subarray.castIndex x
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }))[x.stop - 1] =
    x[0]
Tactic:
simp only [Array.getElem_swap, Subarray.castIndex]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (if x.start + (Subarray.size x - 1) = x.stop - 1 then x.as[x.start + 0]
    else if x.start + 0 = x.stop - 1 then x.as[x.start + (Subarray.size x - 1)] else x.as[x.stop - 1]) =
    x[0]
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (if x.start + (Subarray.size x - 1) = x.stop - 1 then x.as[x.start + 0]
    else if x.start + 0 = x.stop - 1 then x.as[x.start + (Subarray.size x - 1)] else x.as[x.stop - 1]) =
    x[0]
Tactic:
rw [if_pos]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.as[x.start + 0] = x[0]

case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.start + (Subarray.size x - 1) = x.stop - 1
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.as[x.start + 0] = x[0]

case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.start + (Subarray.size x - 1) = x.stop - 1
Tactic:
rfl
Proof state after:
case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.start + (Subarray.size x - 1) = x.stop - 1
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.start + (Subarray.size x - 1) = x.stop - 1
Tactic:
rewrite [Subarray.size, ← Nat.add_sub_assoc (Nat.sub_pos_of_lt hs), Nat.add_sub_cancel' x.h₁]
Proof state after:
case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - Nat.succ 0 = x.stop - 1
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - Nat.succ 0 = x.stop - 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Tactic:
simp only [Subarray.stop_shrinkOne', Subarray.stop_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥ x.stop - 1
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥ x.stop - 1
Tactic:
exact .refl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk, 0 < k ∧ (popMax lt x)[i] = x[k]
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            let_fun this := (_ : 0 < x.stop - x.start);
            let x :=
              Subarray.swap x { val := 0, isLt := this }
                { val := Subarray.size x - 1,
                  isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
            heapifyDown lt (Subarray.shrinkOne' x h) 0
          else x)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            let_fun this := (_ : 0 < x.stop - x.start);
            let x :=
              Subarray.swap x { val := 0, isLt := this }
                { val := Subarray.size x - 1,
                  isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
            heapifyDown lt (Subarray.shrinkOne' x h) 0
          else x)[i] =
        x[k]
Tactic:
dsimp
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Tactic:
have : i + 1 < x.stop - x.start := Nat.add_lt_of_lt_sub hi
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this : i + 1 < x.stop - x.start
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this : i + 1 < x.stop - x.start
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Tactic:
have : x.start < x.stop := calc
  x.start < i+1+x.start := Nat.lt_add_of_pos_left i.zero_lt_succ
  _       < x.stop := Nat.add_lt_of_lt_sub this
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Tactic:
simp only [dif_pos this]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
have hzero : 0 < x.size := Nat.sub_pos_of_lt this
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
have hlast : x.size-1 < x.size := Nat.pred_lt' <| Nat.add_lt_of_lt_sub hi
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
have ⟨k,hk,h⟩ :=
  exists_get_heapifyDown lt ((x.swap ⟨0,hzero⟩ ⟨x.size-1,hlast⟩).shrinkOne' this) 0 i <| by
    simp only [Subarray.size_shrinkOne', Subarray.size_swap]
    exact hi
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
simp only [h, Subarray.getElem_shrinkOne', Subarray.getElem_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
clear h
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
conv at hk => simp only [Subarray.size_shrinkOne', Subarray.size_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
simp only [if_neg (Nat.ne_of_gt hk)]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
if hzk : 0 = k then
  simp only [if_pos hzk]
  exists x.size-1, hlast
  exact ⟨Nat.lt_of_le_of_lt k.zero_le hk, rfl⟩
else
  simp only [if_neg hzk]
  exists k, (Nat.lt_of_lt_of_le hk x.size.pred_le)
  exact ⟨Nat.pos_of_ne_zero (Ne.symm hzk), rfl⟩
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
Tactic:
simp only [Subarray.size_shrinkOne', Subarray.size_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i < Subarray.size x - 1
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i < Subarray.size x - 1
Tactic:
exact hi
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
simp only [if_pos hzk]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ ∃ k hk, 0 < k ∧ x[Subarray.size x - 1] = x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ ∃ k hk, 0 < k ∧ x[Subarray.size x - 1] = x[k]
Tactic:
exists x.size-1, hlast
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ 0 < Subarray.size x - 1 ∧ x[Subarray.size x - 1] = x[Subarray.size x - 1]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ 0 < Subarray.size x - 1 ∧ x[Subarray.size x - 1] = x[Subarray.size x - 1]
Tactic:
exact ⟨Nat.lt_of_le_of_lt k.zero_le hk, rfl⟩
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
simp only [if_neg hzk]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ x[k] = x[k_1]