[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
⊢ ↑i ≤ 2 * ↑i
[PROOFSTEP]
rw [Nat.succ_mul, Nat.one_mul]
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
⊢ ↑i ≤ ↑i + ↑i
[PROOFSTEP]
exact Nat.le_add_left i i
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
⊢ ↑↑j < Array.size a'
[PROOFSTEP]
rw [a.size_swap i j]
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
⊢ ↑↑j < Array.size a
[PROOFSTEP]
exact j.1.2
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
j' : Fin (Array.size a') := { val := ↑↑j, isLt := ?m.5009 }
⊢ Array.size a' - ↑↑j < Array.size a - ↑i
[PROOFSTEP]
rw [a.size_swap i j]
[GOAL]
α : Type ?u.337
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j✝ j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
j' : Fin (Array.size a') := { val := ↑↑j, isLt := ?m.5009 }
⊢ Array.size a - ↑↑j < Array.size a - ↑i
[PROOFSTEP]
exact Nat.sub_lt_sub_left i.2 <| Nat.lt_of_le_of_ne j.2 h
[GOAL]
α : Type u_1
a : Array α
i : Fin (Array.size a)
left : ℕ := 2 * ↑i + 1
right : ℕ := left + 1
left_le : ↑i ≤ left
right_le : ↑i ≤ right
i_le : i ≤ i
j : { j // i ≤ j }
h : ¬↑i = ↑↑j
a' : Array α := Array.swap a i ↑j
j' : Fin (Array.size a') := { val := ↑↑j, isLt := (_ : ↑↑j < Array.size a') }
this : Array.size a' - ↑↑j < Array.size a - ↑i
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => Array.size a - ↑snd) instWellFoundedRelation).1
    { fst := a', snd := j' } { fst := a, snd := i }
[PROOFSTEP]
assumption
[GOAL]
α : Type ?u.8277
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
i0 : ¬↑i = 0
this : (↑i - 1) / 2 < ↑i
j : Fin (Array.size a) := { val := (↑i - 1) / 2, isLt := (_ : (↑i - 1) / 2 < Array.size a) }
a' : Array α := Array.swap a i j
⊢ ↑j < Array.size a'
[PROOFSTEP]
rw [a.size_swap i j]
[GOAL]
α : Type ?u.8277
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
i0 : ¬↑i = 0
this : (↑i - 1) / 2 < ↑i
j : Fin (Array.size a) := { val := (↑i - 1) / 2, isLt := (_ : (↑i - 1) / 2 < Array.size a) }
a' : Array α := Array.swap a i j
⊢ ↑j < Array.size a
[PROOFSTEP]
exact j.2
[GOAL]
α : Type u_1
lt : α → α → Bool
a : Array α
i : Fin (Array.size a)
i0 : ¬↑i = 0
this : (↑i - 1) / 2 < ↑i
j : Fin (Array.size a) := { val := (↑i - 1) / 2, isLt := (_ : (↑i - 1) / 2 < Array.size a) }
h✝ : lt (Array.get a j) (Array.get a i) = true
a' : Array α := Array.swap a i j
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => ↑snd) instWellFoundedRelation).1
    { fst := a', snd := { val := ↑j, isLt := (_ : ↑j < Array.size a') } } { fst := a, snd := i }
[PROOFSTEP]
assumption
[GOAL]
α : Type ?u.10435
lt : α → α → Bool
self : BinaryHeap α lt
x : α
n : ℕ := size self
⊢ n < Array.size (Array.push self.arr x)
[PROOFSTEP]
rw [Array.size_push]
[GOAL]
α : Type ?u.10435
lt : α → α → Bool
self : BinaryHeap α lt
x : α
n : ℕ := size self
⊢ n < Array.size self.arr + 1
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
x : α
⊢ size (insert self x) = size self + 1
[PROOFSTEP]
simp [insert, size, size_heapifyUp]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
e : Array.size self.arr = 0
⊢ size self = size self - 1
[PROOFSTEP]
simp [size, e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
⊢ 0 < Array.size self.arr
[PROOFSTEP]
rw [e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
⊢ 0 < Nat.succ n
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
⊢ n < Array.size self.arr
[PROOFSTEP]
rw [e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
⊢ n < Nat.succ n
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
hn : n < Array.size self.arr
hn0 : 0 < n
a : Array α := Array.pop (Array.swap self.arr { val := 0, isLt := h0 } { val := n, isLt := hn })
⊢ 0 < Array.size a
[PROOFSTEP]
rwa [Array.size_pop, Array.size_swap, e]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
hn : n < Array.size self.arr
hn0 : 0 < n
a : Array α := Array.pop (Array.swap self.arr { val := 0, isLt := h0 } { val := n, isLt := hn })
⊢ size { arr := ↑(heapifyDown lt a { val := 0, isLt := (_ : 0 < Array.size a) }) } = size self - 1
[PROOFSTEP]
simp [size]
[GOAL]
α : Type ?u.11234
lt : α → α → Bool
self : BinaryHeap α lt
n : ℕ
e : Array.size self.arr = Nat.succ n
h0 : 0 < Array.size self.arr
hn : n < Array.size self.arr
hn0 : ¬0 < n
⊢ size { arr := Array.pop self.arr } = size self - 1
[PROOFSTEP]
simp [size]
[GOAL]
α : Type u_1
x : α
lt : α → α → Bool
self : BinaryHeap α lt
e : max self = some x
h : ¬0 < Array.size self.arr
⊢ False
[PROOFSTEP]
simp [BinaryHeap.max, Array.get?, h] at e 
[GOAL]
α : Type ?u.16836
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size a
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.16836
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size self.arr
[PROOFSTEP]
exact size_pos_of_max e
[GOAL]
α : Type ?u.18030
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size a
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.18030
lt : α → α → Bool
self : BinaryHeap α lt
x m : α
e : max self = some m
a : Array α := Array.set self.arr { val := 0, isLt := (_ : 0 < size self) } x
⊢ 0 < Array.size self.arr
[PROOFSTEP]
exact size_pos_of_max e
[GOAL]
α : Type ?u.19048
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size (Array.set self.arr i x)
[PROOFSTEP]
rw [self.1.size_set]
[GOAL]
α : Type ?u.19048
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size self.arr
[PROOFSTEP]
exact i.2
[GOAL]
α : Type ?u.19626
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size (Array.set self.arr i x)
[PROOFSTEP]
rw [self.1.size_set]
[GOAL]
α : Type ?u.19626
lt : α → α → Bool
self : BinaryHeap α lt
i : Fin (size self)
x : α
⊢ ↑i < Array.size self.arr
[PROOFSTEP]
exact i.2
[GOAL]
α : Type ?u.20451
a✝ : Array α
lt : α → α → Bool
gt : α → α → Bool := fun y x => lt x y
a : BinaryHeap α gt
out : Array α
x : α
e : BinaryHeap.max a = some x
⊢ BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.20451
a✝ : Array α
lt : α → α → Bool
gt : α → α → Bool := fun y x => lt x y
a : BinaryHeap α gt
out : Array α
x : α
e : BinaryHeap.max a = some x
⊢ BinaryHeap.size a - 1 < BinaryHeap.size a
[PROOFSTEP]
exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
[GOAL]
α : Type u_1
lt : α → α → Bool
a : BinaryHeap α fun y x => lt x y
out : Array α
gt : α → α → Bool := fun y x => lt x y
x : α
e : BinaryHeap.max a = some x
this : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => BinaryHeap.size a) instWellFoundedRelation).1
    { fst := BinaryHeap.popMax a, snd := push out x } { fst := a, snd := out }
[PROOFSTEP]
assumption
