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

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
⊢ min (hRank []) (hRank h) ≤ hRank (mergeNodes le [] h)
Tactic:
rw[Nat.min_eq]
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
⊢ (if hRank [] ≤ hRank h then hRank [] else hRank h) ≤ hRank (mergeNodes le [] h)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
⊢ (if hRank [] ≤ hRank h then hRank [] else hRank h) ≤ hRank (mergeNodes le [] h)
Tactic:
split
State after:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : hRank [] ≤ hRank h
⊢ hRank [] ≤ hRank (mergeNodes le [] h)

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : ¬hRank [] ≤ hRank h
⊢ hRank h ≤ hRank (mergeNodes le [] h)

State before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : hRank [] ≤ hRank h
⊢ hRank [] ≤ hRank (mergeNodes le [] h)

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : ¬hRank [] ≤ hRank h
⊢ hRank h ≤ hRank (mergeNodes le [] h)
Tactic:
. rw[empty_heap_merge_left]
  assumption
State after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : ¬hRank [] ≤ hRank h
⊢ hRank h ≤ hRank (mergeNodes le [] h)

State before:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r []
ht₂ : IsHeapForest' r h
h✝ : ¬hRank [] ≤ hRank h
⊢ hRank h ≤ hRank (mergeNodes le [] h)
Tactic:
. rw[empty_heap_merge_left]
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
⊢ min (hRank h) (hRank []) ≤ hRank (mergeNodes le h [])
Tactic:
rw[empty_heap_merge_right, Nat.min_eq]
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
⊢ (if hRank h ≤ hRank [] then hRank h else hRank []) ≤ hRank h

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
⊢ (if hRank h ≤ hRank [] then hRank h else hRank []) ≤ hRank h
Tactic:
split
State after:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
h✝ : hRank h ≤ hRank []
⊢ hRank h ≤ hRank h

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
h✝ : ¬hRank h ≤ hRank []
⊢ hRank [] ≤ hRank h

State before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
h✝ : hRank h ≤ hRank []
⊢ hRank h ≤ hRank h

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
h✝ : ¬hRank h ≤ hRank []
⊢ hRank [] ≤ hRank h
Tactic:
. rfl
State after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
h✝ : ¬hRank h ≤ hRank []
⊢ hRank [] ≤ hRank h

State before:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys h : List (BinTree α)
ht₁ : IsHeapForest' r h
ht₂ : IsHeapForest' r []
h✝ : ¬hRank h ≤ hRank []
⊢ hRank [] ≤ hRank h
Tactic:
. simp at *
  apply Nat.le_of_lt
  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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤ hRank (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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤
    hRank
      (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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤
    hRank
      (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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤ hRank (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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤
    hRank
      (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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤ hRank (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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤
    hRank
      (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:
. repeat rw[hrank_of_cons]
  rw[Nat.min_eq]
  split
  . rfl
  . simp at *
    apply Nat.le_of_lt
    assumption
State after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤
    hRank
      (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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ min (hRank (h₁ :: t₁)) (hRank (h₂ :: t₂)) ≤
    hRank
      (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
  . repeat rw[hrank_of_cons]
    rw[Nat.min_eq]
    split
    . assumption
    . rfl
  . dsimp
    split
    . split
      . simp at *
        have heq : h₁.rank = h₂.rank := by
          apply Nat.le_antisymm <;> assumption
        repeat rw[hrank_of_cons]
        rw[rank_combine heq]
        rw[Nat.min_eq]
        split <;> apply Nat.le_succ
      . repeat rw[hrank_of_cons] 
        have hf : IsHeapForest' r (combine le h₁ h₂ :: t₁) := by
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          constructor
          . rw[rank_combine heq] at *
            cases ht₁
            apply Nat.lt_succ_of_lt 
            assumption
          . cases ht₁
            cases ht₂
            apply combine_IsBinTree <;> assumption
          . cases ht₁ with | cons _ _ hf =>
              rw[rank_combine heq] at *
              match hf with
              | .nil => 
                constructor
              | .cons (t := t) (ts := ts) lt _ _ =>
                constructor
                . rw[hrank_of_cons] at *
                  rename_i neq
                  unfold bne at neq
                  rw[Nat.not_beq_eq_true_eq] at neq
                  have : h₁.rank + 1 ≤  t.rank := by
                    apply Nat.succ_le_of_lt lt
                  apply lt_of_le_of_ne <;> assumption
                repeat assumption
        have hf₂ : IsHeapForest' r t₂ := by
          cases ht₂
          apply IsHeapForest'_weaken
          . assumption
          . apply Nat.le_of_lt
            assumption
        have ih := min_hRank_mergeNodes hf hf₂
        transitivity (min (hRank (combine le h₁ h₂ :: t₁)) (hRank t₂))
        . rw[hrank_of_cons] at *
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          rw[rank_combine heq] at *
          repeat rw[Nat.min_eq]
          split
          . split
            . apply Nat.le_succ
            . simp at *
              rename_i heq₂ _ hlt
              unfold bne at heq₂
              rw [Bool.not_eq_false', beq_iff_eq] at heq₂
              simp [← heq₂] at hlt 
          . split
            . apply Nat.le_succ
            . rename_i heq₂ _ hnle
              unfold bne at heq₂
              rw [Bool.not_eq_false', beq_iff_eq] at heq₂
              simp [← heq₂] at hnle
        . apply ih
    . split
      . repeat rw[hrank_of_cons]
        have hf : IsHeapForest' r t₁ := by
          cases ht₁
          apply IsHeapForest'_weaken
          . assumption
          . apply Nat.le_of_lt
            assumption
        have hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂) := by
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          constructor
          . cases ht₁
            rw[rank_combine heq] at *
            apply Nat.lt_succ_of_lt
            assumption
          . cases ht₁
            cases ht₂
            apply combine_IsBinTree <;> assumption
          . rw[rank_combine heq] at *
            cases ht₂ with | cons _ _ hf₂ =>
              match hf₂ with
              | .nil => 
                constructor
              | .cons (t := t) (ts := ts) lt _ _ => 
                rename_i hneq
                rw[hrank_of_cons] at *
                constructor
                . rw[← heq] at lt
                  unfold bne at hneq
                  rw[Nat.not_beq_eq_true_eq] at hneq
                  apply lt_of_le_of_ne <;> assumption
                repeat assumption
        have ih := min_hRank_mergeNodes hf hf₂
        transitivity (min (hRank t₁) (hRank (combine le h₁ h₂ :: t₂)))
        . rw[hrank_of_cons] at *
          simp at *
          have heq : h₁.rank = h₂.rank := by
            apply Nat.le_antisymm <;> assumption
          rw[rank_combine heq] at *
          repeat rw[Nat.min_eq]
          split
          . split
            . cases ht₁ with | cons _ _ hf₃ =>
                cases hf₃
                . contradiction
                . rw[hrank_of_cons]
                  apply Nat.le_of_lt
                  assumption
            . apply Nat.le_succ
          . split
            . cases ht₁ with | cons _ _ hf₃ =>
                cases hf₃
                . contradiction
                . rw[hrank_of_cons]
                  apply Nat.le_of_lt
                  assumption
            . apply Nat.le_succ
        . apply ih
      . repeat rw[hrank_of_cons]
        simp at *
        have heq : h₁.rank = h₂.rank := by
          apply Nat.le_antisymm <;> assumption
        rw[rank_combine heq]
        rw[Nat.min_eq]
        split <;> apply Nat.le_succ
State after:
no goals

State before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
⊢ min h₁.rank h₂.rank ≤ hRank (h₁ :: mergeNodes le t₁ (h₂ :: t₂))
Tactic:
rw[hrank_of_cons]
State after:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
⊢ min h₁.rank h₂.rank ≤ h₁.rank

State before:
case inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ min h₁.rank h₂.rank ≤ hRank (h₂ :: mergeNodes le t₂ (h₁ :: t₁))
Tactic:
rw[hrank_of_cons]
State after:
case inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ min h₁.rank h₂.rank ≤ h₂.rank

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
h✝² : ((combine le h₁ h₂).rank != hRank t₂) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝¹ : h₂.rank ≤ h₁.rank
h✝ : h₁.rank ≤ h₂.rank
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
State after:
no goals

State before:
case inr.inr.inl.inl
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
h✝² : ((combine le h₁ h₂).rank != hRank t₂) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝¹ : h₂.rank ≤ h₁.rank
h✝ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
⊢ min h₁.rank h₂.rank ≤ hRank (combine le h₁ h₂ :: mergeNodes le t₁ t₂)
Tactic:
rw[hrank_of_cons]
State after:
case inr.inr.inl.inl
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
h✝² : ((combine le h₁ h₂).rank != hRank t₂) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝¹ : h₂.rank ≤ h₁.rank
h✝ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
⊢ min h₁.rank h₂.rank ≤ (combine le h₁ h₂).rank

State before:
case inr.inr.inl.inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ min h₁.rank (hRank (h₂ :: t₂)) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) t₂)
Tactic:
rw[hrank_of_cons]
State after:
case inr.inr.inl.inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ min h₁.rank h₂.rank ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) t₂)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₁)
Tactic:
simp at *
State after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₁)

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₁)
Tactic:
have heq : h₁.rank = h₂.rank := by
  apply Nat.le_antisymm <;> assumption
State after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₁)

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₁)
Tactic:
constructor
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ r < (combine le h₁ h₂).rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ r < (combine le h₁ h₂).rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
Tactic:
. rw[rank_combine heq] at *
  cases ht₁
  apply Nat.lt_succ_of_lt 
  assumption
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
Tactic:
. cases ht₁
  cases ht₂
  apply combine_IsBinTree <;> assumption
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
Tactic:
. cases ht₁ with | cons _ _ hf =>
    rw[rank_combine heq] at *
    match hf with
    | .nil => 
      constructor
    | .cons (t := t) (ts := ts) lt _ _ =>
      constructor
      . rw[hrank_of_cons] at *
        rename_i neq
        unfold bne at neq
        rw[Nat.not_beq_eq_true_eq] at neq
        have : h₁.rank + 1 ≤  t.rank := by
          apply Nat.succ_le_of_lt lt
        apply lt_of_le_of_ne <;> assumption
      repeat assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
State after:
no goals

State before:
case a.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
Tactic:
rw[rank_combine heq] at *
State after:
case a.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₁.rank + 1) t₁

State before:
case a.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₁.rank + 1) t₁
Tactic:
match hf with
| .nil => 
  constructor
| .cons (t := t) (ts := ts) lt _ _ =>
  constructor
  . rw[hrank_of_cons] at *
    rename_i neq
    unfold bne at neq
    rw[Nat.not_beq_eq_true_eq] at neq
    have : h₁.rank + 1 ≤  t.rank := by
      apply Nat.succ_le_of_lt lt
    apply lt_of_le_of_ne <;> assumption
  repeat assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
h✝ : (h₁.rank + 1 != hRank []) = true
⊢ IsHeapForest' (h₁.rank + 1) []
Tactic:
constructor
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
constructor
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ h₁.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ h₁.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
Tactic:
. rw[hrank_of_cons] at *
  rename_i neq
  unfold bne at neq
  rw[Nat.not_beq_eq_true_eq] at neq
  have : h₁.rank + 1 ≤  t.rank := by
    apply Nat.succ_le_of_lt lt
  apply lt_of_le_of_ne <;> assumption
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
Tactic:
repeat assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬h₁.rank + 1 = t.rank
⊢ h₁.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
State after:
no goals

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₁
a✝² : r < h₁.rank
hf : IsHeapForest' h₁.rank t₁
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
Tactic:
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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
⊢ IsHeapForest' r t₂
Tactic:
cases ht₂
State after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' r t₂

State before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' r t₂
Tactic:
apply IsHeapForest'_weaken
State after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' ?cons.n t₂

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ ℕ

State before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' ?cons.n t₂

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ ℕ
Tactic:
. assumption
State after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ h₂.rank

State before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ h₂.rank
Tactic:
. apply Nat.le_of_lt
  assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (combine le h₁ h₂).rank (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
State after:
no goals

State before:
case inr.inr.inl.inr.a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (h₁.rank + 1) (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ min (h₁.rank + 1) (hRank t₂)
Tactic:
rw[Nat.min_eq]
State after:
case inr.inr.inl.inr.a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (h₁.rank + 1) (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ if h₁.rank + 1 ≤ hRank t₂ then h₁.rank + 1 else hRank t₂

State before:
case inr.inr.inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ min h₁.rank (hRank (h₂ :: t₂)) ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
Tactic:
rw[hrank_of_cons]
State after:
case inr.inr.inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ min h₁.rank h₂.rank ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ IsHeapForest' r t₁
Tactic:
cases ht₁
State after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' r t₁

State before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' r t₁
Tactic:
apply IsHeapForest'_weaken
State after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' ?cons.n t₁

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ ℕ

State before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' ?cons.n t₁

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ ℕ
Tactic:
. assumption
State after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ h₁.rank

State before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ h₁.rank
Tactic:
. apply Nat.le_of_lt
  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
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
hf : IsHeapForest' r t₁
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)
Tactic:
simp at *
State after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)
Tactic:
have heq : h₁.rank = h₂.rank := by
  apply Nat.le_antisymm <;> assumption
State after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)
Tactic:
constructor
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ r < (combine le h₁ h₂).rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₂

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ r < (combine le h₁ h₂).rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₂
Tactic:
. cases ht₁
  rw[rank_combine heq] at *
  apply Nat.lt_succ_of_lt
  assumption
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₂

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₂
Tactic:
. cases ht₁
  cases ht₂
  apply combine_IsBinTree <;> assumption
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₂

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' (combine le h₁ h₂).rank t₂
Tactic:
. rw[rank_combine heq] at *
  cases ht₂ with | cons _ _ hf₂ =>
    match hf₂ with
    | .nil => 
      constructor
    | .cons (t := t) (ts := ts) lt _ _ => 
      rename_i hneq
      rw[hrank_of_cons] at *
      constructor
      . rw[← heq] at lt
        unfold bne at hneq
        rw[Nat.not_beq_eq_true_eq] at hneq
        apply lt_of_le_of_ne <;> assumption
      repeat assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
State after:
no goals

State before:
case a.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
h✝³ : (h₁.rank + 1 != hRank t₂) = true
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₂
a✝ : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' (h₁.rank + 1) t₂
Tactic:
match hf₂ with
| .nil => 
  constructor
| .cons (t := t) (ts := ts) lt _ _ => 
  rename_i hneq
  rw[hrank_of_cons] at *
  constructor
  . rw[← heq] at lt
    unfold bne at hneq
    rw[Nat.not_beq_eq_true_eq] at hneq
    apply lt_of_le_of_ne <;> assumption
  repeat assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₂
a✝ : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝ : (h₁.rank + 1 != hRank []) = true
⊢ IsHeapForest' (h₁.rank + 1) []
Tactic:
constructor
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
rename_i hneq
State after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
rw[hrank_of_cons] at *
State after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
constructor
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ h₁.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ h₁.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' t.rank ts
Tactic:
. rw[← heq] at lt
  unfold bne at hneq
  rw[Nat.not_beq_eq_true_eq] at hneq
  apply lt_of_le_of_ne <;> assumption
State after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' t.rank ts
Tactic:
repeat assumption
State after:
no goals

State before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
hf : IsHeapForest' r t₁
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' t.rank ts
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (combine le h₁ h₂).rank ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
State after:
no goals

State before:
case inr.inr.inr.inl.a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₂) = true
hf : IsHeapForest' r t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (h₁.rank + 1) ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ min (hRank t₁) (h₁.rank + 1)
Tactic:
rw[Nat.min_eq]
State after:
case inr.inr.inr.inl.a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₂) = true
hf : IsHeapForest' r t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (h₁.rank + 1) ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ if hRank t₁ ≤ h₁.rank + 1 then hRank t₁ else h₁.rank + 1

State before:
case inr.inr.inr.inl.a.inl.inl.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf : IsHeapForest' r t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (h₁.rank + 1) ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
h✝² : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : hRank t₁ ≤ h₁.rank + 1
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf₃ : IsHeapForest' h₁.rank t₁
⊢ h₁.rank ≤ hRank t₁
Tactic:
cases hf₃
State after:
case inr.inr.inr.inl.a.inl.inl.cons.nil
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' r []
ih : min (hRank []) (h₁.rank + 1) ≤ hRank (mergeNodes le [] (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank []) = false
h✝ : hRank [] ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank []

case inr.inr.inr.inl.a.inl.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)

State before:
case inr.inr.inr.inl.a.inl.inl.cons.nil
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' r []
ih : min (hRank []) (h₁.rank + 1) ≤ hRank (mergeNodes le [] (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank []) = false
h✝ : hRank [] ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank []

case inr.inr.inr.inl.a.inl.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)
Tactic:
. contradiction
State after:
case inr.inr.inr.inl.a.inl.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)

State before:
case inr.inr.inr.inl.a.inl.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)
Tactic:
. rw[hrank_of_cons]
  apply Nat.le_of_lt
  assumption
State after:
no goals

State before:
case inr.inr.inr.inl.a.inr.inl.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf : IsHeapForest' r t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (h₁.rank + 1) ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
h✝² : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
h✝¹ : ¬h₁.rank ≤ h₂.rank
h✝ : hRank t₁ ≤ h₁.rank + 1
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf₃ : IsHeapForest' h₁.rank t₁
⊢ h₁.rank ≤ hRank t₁
Tactic:
cases hf₃
State after:
case inr.inr.inr.inl.a.inr.inl.cons.nil
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' r []
ih : min (hRank []) (h₁.rank + 1) ≤ hRank (mergeNodes le [] (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank []) = false
h✝ : hRank [] ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank []

case inr.inr.inr.inl.a.inr.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)

State before:
case inr.inr.inr.inl.a.inr.inl.cons.nil
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' r []
ih : min (hRank []) (h₁.rank + 1) ≤ hRank (mergeNodes le [] (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank []) = false
h✝ : hRank [] ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank []

case inr.inr.inr.inl.a.inr.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)
Tactic:
. contradiction
State after:
case inr.inr.inr.inl.a.inr.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)

State before:
case inr.inr.inr.inl.a.inr.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : ¬h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)
Tactic:
. rw[hrank_of_cons]
  apply Nat.le_of_lt
  assumption
State after:
no goals

State before:
case inr.inr.inr.inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ min h₁.rank h₂.rank ≤ hRank (combine le h₁ h₂ :: mergeNodes le t₁ t₂)
Tactic:
rw[hrank_of_cons]
State after:
case inr.inr.inr.inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (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
⊢ min h₁.rank h₂.rank ≤ (combine le h₁ h₂).rank

State before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : ((combine le h₁ h₂).rank != hRank t₁) = false
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
State after:
no goals

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₂)
⊢ (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
    { fst := t₁, snd := { fst := combine le h₁ h₂ :: t₂, snd := { fst := hf, snd := hf₂ } } }
    { fst := h₁ :: t₁, snd := { fst := h₂ :: t₂, snd := { fst := ht₁, snd := ht₂ } } }
Tactic:
simp_wf
State after:
α : 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₂)

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 [*]
State after:
no goals