α : Type u_1
le : α → α → Bool
a a✝² : α
a✝¹ a✝ : HeapNode α
w✝ : Nat
left✝ : ∀ [inst : TotalBLE le], le a a✝² = true
c : WellFormed le a✝² a✝¹ w✝
s : WellFormed le a a✝ w✝
⊢ 2 ^ w✝ + realSize a✝ + 1 = 2 ^ w✝ * 1 + 2 ^ w✝
α : Type u_1
le : α → α → Bool
a a✝² : α
a✝¹ a✝ : HeapNode α
w✝ : Nat
left✝ : ∀ [inst : TotalBLE le], le a a✝² = true
c : WellFormed le a✝² a✝¹ w✝
s : WellFormed le a a✝ w✝
⊢ realSize (node a✝² a✝¹ a✝) + 1 = 2 ^ (w✝ + 1)
rw [realSize, realSize_eq c, Nat.pow_succ, Nat.mul_succ]
no goals
α : Type u_1
le : α → α → Bool
a a✝² : α
a✝¹ a✝ : HeapNode α
w✝ : Nat
left✝ : ∀ [inst : TotalBLE le], le a a✝² = true
c : WellFormed le a✝² a✝¹ w✝
s : WellFormed le a a✝ w✝
⊢ 2 ^ w✝ + realSize a✝ + 1 = 2 ^ w✝ * 1 + 2 ^ w✝
simp [Nat.add_assoc, realSize_eq s]