Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
_x✝ : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))
a✝¹ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        _x✝ →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
hx hy : List (HeapNodeAux α (Heap α))
a✝ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        { fst := hx, snd := hy } →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
x✝ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        { fst := h₁ :: t₁, snd := h₂ :: t₂ } →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ¬((combine le h₁ h₂).rank != hRank t₂) = true
⊢ (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1
    { fst := t₁, snd := t₂ } { fst := h₁ :: t₁, snd := h₂ :: t₂ }
Tactic:
simp_wf
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
_x✝ : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))
a✝¹ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        _x✝ →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
hx hy : List (HeapNodeAux α (Heap α))
a✝ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        { fst := hx, snd := hy } →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
x✝ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        { fst := h₁ :: t₁, snd := h₂ :: t₂ } →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ¬((combine le h₁ h₂).rank != hRank t₂) = true
⊢ List.length t₁ + List.length t₂ < Nat.succ (List.length t₁) + Nat.succ (List.length t₂)