Theorem: project.IsMinHeap_merge (Project/Merge.lean)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
⊢ IsMinHeap le (Heap.heap []) → IsMinHeap le (Heap.heap h) → IsMinHeap le (Heap.heap (mergeNodes le [] h))
Tactic:
intros _ hys
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
hys : IsMinHeap le (Heap.heap h)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] h))

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
hys : IsMinHeap le (Heap.heap h)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] h))
Tactic:
cases hys
State after:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))

State before:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))
Tactic:
. simp[mergeNodes]
  constructor
State after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))

State before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))
Tactic:
. constructor <;> assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
⊢ IsMinHeap le (Heap.heap h) → IsMinHeap le (Heap.heap []) → IsMinHeap le (Heap.heap (mergeNodes le h []))
Tactic:
intros hxs _
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap h)
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le h []))

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap h)
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le h []))
Tactic:
cases hxs
State after:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))

State before:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))
Tactic:
. simp[mergeNodes]
  constructor
State after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))

State before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))
Tactic:
. constructor <;> assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
⊢ IsMinHeap le (Heap.heap (h₁ :: t₁)) →
    IsMinHeap le (Heap.heap (h₂ :: t₂)) → IsMinHeap le (Heap.heap (mergeNodes le (h₁ :: t₁) (h₂ :: t₂)))
Tactic:
intros hxs hys
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le (Heap.heap (mergeNodes le (h₁ :: t₁) (h₂ :: t₂)))

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le (Heap.heap (mergeNodes le (h₁ :: t₁) (h₂ :: t₂)))
Tactic:
unfold mergeNodes
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le
    (Heap.heap
      (if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ (h₂ :: t₂)
      else
        if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
        else
          let merged := combine le h₁ h₂;
          let r := merged.rank;
          if (r != hRank t₁) = true then
            if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
          else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le
    (Heap.heap
      (if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ (h₂ :: t₂)
      else
        if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
        else
          let merged := combine le h₁ h₂;
          let r := merged.rank;
          if (r != hRank t₁) = true then
            if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
          else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Tactic:
split
State after:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : h₁.rank < h₂.rank
⊢ IsMinHeap le (Heap.heap (h₁ :: mergeNodes le t₁ (h₂ :: t₂)))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))

State before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : h₁.rank < h₂.rank
⊢ IsMinHeap le (Heap.heap (h₁ :: mergeNodes le t₁ (h₂ :: t₂)))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Tactic:
. constructor
  . cases hxs
    assumption
  . cases hxs
    apply IsMinHeap_merge <;> assumption
State after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))

State before:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Tactic:
. split
  . constructor
    . cases hys
      assumption
    . cases hys
      apply IsMinHeap_merge <;> assumption
  . dsimp
    split
    . split
      . constructor
        . apply combine_IsSearchTree
          . assumption
          . cases hxs
            assumption
          . cases hys
            assumption
        . apply IsMinHeap_merge
          . cases hxs
            assumption
          . cases hys
            assumption
      . apply IsMinHeap_merge
        . constructor
          . apply combine_IsSearchTree
            . assumption
            . cases hxs
              assumption
            . cases hys
              assumption
          . cases hxs
            assumption
        . cases hys
          assumption
    . split
      . apply IsMinHeap_merge
        . cases hxs
          assumption
        . constructor
          . apply combine_IsSearchTree
            . assumption
            . cases hxs
              assumption
            . cases hys
              assumption
          . cases hys
            assumption
      . constructor
        . apply combine_IsSearchTree
          . assumption
          . cases hxs
            assumption 
          . cases hys
            assumption
        . apply IsMinHeap_merge
          . cases hxs
            assumption
          . cases hys
            assumption
State after:
no goals

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
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₂)

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
⊢ List.length t₁ + List.length t₂ < Nat.succ (List.length t₁) + Nat.succ (List.length t₂)
Tactic:
simp_arith [*]
State after:
no goals