α : Type u_1
le : α → α → Bool
n a✝³ : Nat
a✝² : α
a✝¹ : HeapNode α
a✝ : Heap α
left✝ : n ≤ a✝³
h₁ : HeapNode.WellFormed le a✝² a✝¹ a✝³
h₂ : WellFormed le (a✝³ + 1) a✝
⊢ 2 ^ a✝³ + realSize a✝ = HeapNode.realSize a✝¹ + 1 + realSize a✝
α : Type u_1
le : α → α → Bool
n a✝³ : Nat
a✝² : α
a✝¹ : HeapNode α
a✝ : Heap α
left✝ : n ≤ a✝³
h₁ : HeapNode.WellFormed le a✝² a✝¹ a✝³
h₂ : WellFormed le (a✝³ + 1) a✝
⊢ size (cons a✝³ a✝² a✝¹ a✝) = realSize (cons a✝³ a✝² a✝¹ a✝)
simp [size, Nat.shiftLeft, size_eq h₂, Nat.pow_succ, Nat.mul_succ]
no goals
α : Type u_1
le : α → α → Bool
n a✝³ : Nat
a✝² : α
a✝¹ : HeapNode α
a✝ : Heap α
left✝ : n ≤ a✝³
h₁ : HeapNode.WellFormed le a✝² a✝¹ a✝³
h₂ : WellFormed le (a✝³ + 1) a✝
⊢ 2 ^ a✝³ + realSize a✝ = HeapNode.realSize a✝¹ + 1 + realSize a✝
simp [Nat.add_assoc, Nat.one_shiftLeft, h₁.realSize_eq, h₂.size_eq]