Theorem: project.min_hRank_mergeNodes
Proof state before:
α : Type u_1
le : α → α → Bool
r : ℕ
_x✝ : (xs : List (BinTree α)) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys
a✝³ :
  ∀ (y : (xs : List (BinTree α)) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun xs snd ↦
                  PSigma.casesOn snd fun ys snd ↦ PSigma.casesOn snd fun ht₁ snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y _x✝ →
      min (hRank y.1) (hRank y.2.1) ≤ hRank (mergeNodes le y.1 y.2.1)
xs : List (BinTree α)
ys✝ : (ys : List (BinTree α)) ×' (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys
a✝² :
  ∀ (y : (xs : List (BinTree α)) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun xs snd ↦
                  PSigma.casesOn snd fun ys snd ↦ PSigma.casesOn snd fun ht₁ snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := xs, snd := ys✝ } →
      min (hRank y.1) (hRank y.2.1) ≤ hRank (mergeNodes le y.1 y.2.1)
ys : List (BinTree α)
ht₁✝¹ : (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys
a✝¹ :
  ∀ (y : (xs : List (BinTree α)) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun xs snd ↦
                  PSigma.casesOn snd fun ys snd ↦ PSigma.casesOn snd fun ht₁ snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := xs, snd := { fst := ys, snd := ht₁✝¹ } } →
      min (hRank y.1) (hRank y.2.1) ≤ hRank (mergeNodes le y.1 y.2.1)
ht₁✝ : IsHeapForest' r xs
ht₂✝ : IsHeapForest' r ys
a✝ :
  ∀ (y : (xs : List (BinTree α)) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun xs snd ↦
                  PSigma.casesOn snd fun ys snd ↦ PSigma.casesOn snd fun ht₁ snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := xs, snd := { fst := ys, snd := { fst := ht₁✝, snd := ht₂✝ } } } →
      min (hRank y.1) (hRank y.2.1) ≤ hRank (mergeNodes le y.1 y.2.1)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
x✝ :
  ∀ (y : (xs : List (BinTree α)) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' r xs) ×' IsHeapForest' r ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun xs snd ↦
                  PSigma.casesOn snd fun ys snd ↦ PSigma.casesOn snd fun ht₁ snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := h₁ :: t₁, snd := { fst := h₂ :: t₂, snd := { fst := ht₁, snd := ht₂ } } } →
      min (hRank y.1) (hRank y.2.1) ≤ hRank (mergeNodes le y.1 y.2.1)
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
hf : IsHeapForest' r t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
⊢ List.length t₁ + Nat.succ (List.length t₂) < Nat.succ (List.length t₁) + Nat.succ (List.length t₂)
Tactic:
simp_arith [*]
Proof state after:
no goals