α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (match Heap.node a₁ c₁ s₁, Heap.node a₂ c₂ s₂ with
    | Heap.nil, Heap.nil => Heap.nil
    | Heap.nil, Heap.node a₂ c₂ sibling => Heap.node a₂ c₂ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.nil => Heap.node a₁ c₁ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil
      else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le (merge le (Heap.node a₁ c₁ s₁) (Heap.node a₂ c₂ s₂))
unfold merge
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (match Heap.node a₁ c₁ s₁, Heap.node a₂ c₂ s₂ with
    | Heap.nil, Heap.nil => Heap.nil
    | Heap.nil, Heap.node a₂ c₂ sibling => Heap.node a₂ c₂ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.nil => Heap.node a₁ c₁ Heap.nil
    | Heap.node a₁ c₁ sibling, Heap.node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil
      else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)
dsimp
case inl
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : le a₁ a₂ = true
⊢ WF le (Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil)

case inr
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : ¬le a₁ a₂ = true
⊢ WF le (Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
⊢ WF le
    (if le a₁ a₂ = true then Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil else Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)
split <;> rename_i h
no goals
case inl
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : le a₁ a₂ = true
⊢ WF le (Heap.node a₁ (Heap.node a₂ c₂ c₁) Heap.nil)
exact node ⟨fun [_] => h, h₂, h₁⟩
no goals
case inr
α✝ : Type u_1
le : α✝ → α✝ → Bool
a₁ : α✝
c₁ : Heap α✝
a₂ : α✝
c₂ s₁ s₂ : Heap α✝
h₁ : NodeWF le a₁ c₁
h₂ : NodeWF le a₂ c₂
h : ¬le a₁ a₂ = true
⊢ WF le (Heap.node a₂ (Heap.node a₁ c₁ c₂) Heap.nil)
exact node ⟨fun [_] => TotalBLE.total.resolve_left h, h₁, h₂⟩