no goals
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : NoSibling s₁
h₂ : NoSibling s₂
⊢ size (merge le s₁ s₂) = size s₁ + size s₂
match h₁, h₂ with
| .nil, .nil | .nil, .node _ _ | .node _ _, .nil => simp [size]
| .node _ _, .node _ _ => unfold merge; dsimp; split <;> simp_arith [size]
no goals
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : NoSibling s₁
h₂ : NoSibling s₂
a✝ : α
c✝ : Heap α
⊢ size (merge le (node a✝ c✝ nil) nil) = size (node a✝ c✝ nil) + size nil
simp [size]
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : NoSibling s₁
h₂ : NoSibling s₂
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ size
      (match node a✝¹ c✝¹ nil, node a✝ c✝ nil with
      | nil, nil => nil
      | nil, node a₂ c₂ sibling => node a₂ c₂ nil
      | node a₁ c₁ sibling, nil => node a₁ c₁ nil
      | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
        if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil) =
    size (node a✝¹ c✝¹ nil) + size (node a✝ c✝ nil)
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : NoSibling s₁
h₂ : NoSibling s₂
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ size (merge le (node a✝¹ c✝¹ nil) (node a✝ c✝ nil)) = size (node a✝¹ c✝¹ nil) + size (node a✝ c✝ nil)
unfold merge
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : NoSibling s₁
h₂ : NoSibling s₂
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ size (if le a✝¹ a✝ = true then node a✝¹ (node a✝ c✝ c✝¹) nil else node a✝ (node a✝¹ c✝¹ c✝) nil) =
    size (node a✝¹ c✝¹ nil) + size (node a✝ c✝ nil)
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : NoSibling s₁
h₂ : NoSibling s₂
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ size
      (match node a✝¹ c✝¹ nil, node a✝ c✝ nil with
      | nil, nil => nil
      | nil, node a₂ c₂ sibling => node a₂ c₂ nil
      | node a₁ c₁ sibling, nil => node a₁ c₁ nil
      | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
        if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil) =
    size (node a✝¹ c✝¹ nil) + size (node a✝ c✝ nil)
dsimp
no goals
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
h₁ : NoSibling s₁
h₂ : NoSibling s₂
a✝¹ : α
c✝¹ : Heap α
a✝ : α
c✝ : Heap α
⊢ size (if le a✝¹ a✝ = true then node a✝¹ (node a✝ c✝ c✝¹) nil else node a✝ (node a✝¹ c✝¹ c✝) nil) =
    size (node a✝¹ c✝¹ nil) + size (node a✝ c✝ nil)
split <;> simp_arith [size]