α : Type u_1
le : α → α → Bool
a : α
n : Nat
s : HeapNode α
h : WellFormed le a s n
⊢ Heap.WellFormed le 0 (HeapNode.toHeap.go s (rank s) Heap.nil)
α : Type u_1
le : α → α → Bool
a : α
n : Nat
s : HeapNode α
h : WellFormed le a s n
⊢ Heap.WellFormed le 0 (HeapNode.toHeap s)
rw [toHeap, rankTR_eq]
no goals
α : Type u_1
le : α → α → Bool
a : α
n : Nat
s : HeapNode α
h : WellFormed le a s n
⊢ Heap.WellFormed le 0 (HeapNode.toHeap.go s (rank s) Heap.nil)
exact go h trivial
α : Type u_1
le : α → α → Bool
a✝ : α
n✝ : Nat
s✝ : HeapNode α
h✝ : WellFormed le a✝ s✝ n✝
res : Heap α
a : α
c s : HeapNode α
n : Nat
left✝ : ∀ [inst : TotalBLE le], le a✝ a = true
h : WellFormed le a c (rank s)
h' : WellFormed le a✝ s n
hr : Heap.WellFormed le (rank (node a c s)) res
⊢ WellFormed le a c (rank (node a c s) - 1)
α : Type u_1
le : α → α → Bool
a✝ : α
n✝ : Nat
s✝ : HeapNode α
h✝ : WellFormed le a✝ s✝ n✝
res : Heap α
a : α
c s : HeapNode α
n : Nat
left✝ : ∀ [inst : TotalBLE le], le a✝ a = true
h : WellFormed le a c n
h' : WellFormed le a✝ s n
hr : Heap.WellFormed le (rank (node a c s)) res
⊢ WellFormed le a c (rank (node a c s) - 1)
rw [← h'.rank_eq] at h
no goals
α : Type u_1
le : α → α → Bool
a✝ : α
n✝ : Nat
s✝ : HeapNode α
h✝ : WellFormed le a✝ s✝ n✝
res : Heap α
a : α
c s : HeapNode α
n : Nat
left✝ : ∀ [inst : TotalBLE le], le a✝ a = true
h : WellFormed le a c (rank s)
h' : WellFormed le a✝ s n
hr : Heap.WellFormed le (rank (node a c s)) res
⊢ WellFormed le a c (rank (node a c s) - 1)
exact h