α : Type u_1
le : α → α → Bool
s : Heap α
⊢ size
      (match s with
      | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
      | h => h) =
    size s
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ size (combine le s) = size s
unfold combine
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ size (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝)) =
    size (node a✝¹ child✝¹ (node a✝ child✝ s✝))

case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ size s = size s
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ size
      (match s with
      | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
      | h => h) =
    size s
split
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ size (merge le (merge le (node a₁ c₁ (node a₂ c₂ s)) (node a₂ c₂ s)) (combine le s)) =
    size (node a₁ c₁ (node a₂ c₂ s))
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ size (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝)) =
    size (node a✝¹ child✝¹ (node a✝ child✝ s✝))
rename_i a₁ c₁ a₂ c₂ s
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ size c₁ + size c₂ + 2 + size s = size (node a₁ c₁ (node a₂ c₂ s))
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ size (merge le (merge le (node a₁ c₁ (node a₂ c₂ s)) (node a₂ c₂ s)) (combine le s)) =
    size (node a₁ c₁ (node a₂ c₂ s))
rw [size_merge le (noSibling_merge _ _ _) (noSibling_combine _ _),
  size_merge_node, size_combine le s]
no goals
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ size c₁ + size c₂ + 2 + size s = size (node a₁ c₁ (node a₂ c₂ s))
simp_arith [size]
no goals
case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ size s = size s
rfl