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

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
⊢ u.rank = c.rank → u.rank + 1 ≤ hRank (mergeNodes le (u :: y) (c :: z))
Tactic:
intros heq
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤ hRank (mergeNodes le (u :: y) (c :: z))

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤ hRank (mergeNodes le (u :: y) (c :: z))
Tactic:
unfold mergeNodes
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤
    hRank
      (if u.rank < c.rank then u :: mergeNodes le y (c :: z)
      else
        if c.rank < u.rank then c :: mergeNodes le z (u :: y)
        else
          let merged := combine le u c;
          let r := merged.rank;
          if (r != hRank y) = true then
            if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
          else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤
    hRank
      (if u.rank < c.rank then u :: mergeNodes le y (c :: z)
      else
        if c.rank < u.rank then c :: mergeNodes le z (u :: y)
        else
          let merged := combine le u c;
          let r := merged.rank;
          if (r != hRank y) = true then
            if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
          else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank + 1 ≤ hRank (u :: mergeNodes le y (c :: z))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)

State before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank + 1 ≤ hRank (u :: mergeNodes le y (c :: z))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
Tactic:
. have : u.rank ≠ c.rank := by
    apply ne_of_lt
    assumption
  contradiction
State after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)

State before:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
Tactic:
. split
  . have hneq : c.rank ≠ u.rank := by
      apply ne_of_lt
      assumption
    have : c.rank = u.rank := by
      apply Eq.symm heq
    contradiction 
  . dsimp
    split
    . split
      . rw[hrank_of_cons]
        rw[rank_combine heq] at *
      . have hf : IsHeapForest' r (combine le u c :: y) := by
          constructor
          . rw[rank_combine heq] at *
            cases ht₁ with | cons lt _ _ =>
              apply Nat.lt_succ_of_lt lt
          . cases ht₁
            cases ht₂
            apply combine_IsBinTree <;> assumption
          . cases ht₁ with | cons _ _ hf =>
              cases ht₂ with | cons =>
                match hf with
                | .nil =>
                  constructor
                | .cons (t := t) (ts := ts) lt _ _ =>
                  rename_i neq
                  rw[rank_combine heq, hrank_of_cons] at *
                  unfold bne at neq
                  rw[Nat.not_beq_eq_true_eq] at neq
                  have : u.rank + 1 ≤ t.rank := by
                    apply Nat.succ_le_of_lt lt
                  constructor
                  . apply lt_of_le_of_ne <;> assumption
                  . assumption
                  . assumption
        have hf₂ : IsHeapForest' r z := by
          cases ht₂
          apply IsHeapForest'_weaken
          . assumption
          . apply Nat.le_of_lt 
            assumption
        have min_le : min (hRank (combine le u c :: y)) (hRank z) ≤ hRank (mergeNodes le (combine le u c :: y) z) := by
          apply min_hRank_mergeNodes hf hf₂
        repeat rw[hrank_of_cons] at *
        rw[Nat.min_eq] at min_le
        rw[rank_combine heq] at *
        split at min_le
        . assumption
        . unfold bne at *
          rw[Nat.not_beq_eq_true_eq] at *
          simp_all
    . split
      . have hf : IsHeapForest' r (combine le u c :: z) := by
          constructor
          . rw[rank_combine heq] at *
            cases ht₂ with | cons lt _ _ =>
              rw[← heq] at lt
              apply Nat.lt_succ_of_lt lt
          . cases ht₁
            cases ht₂
            apply combine_IsBinTree <;> assumption
          . cases ht₁ with | cons =>
              cases ht₂ with  | cons _ _ hf =>
                match hf with
                | .nil =>
                  constructor
                | .cons (t := t) (ts := ts) lt _ _ =>
                  rename_i neq
                  rw[rank_combine heq, hrank_of_cons] at *
                  unfold bne at neq
                  rw[Nat.not_beq_eq_true_eq] at neq
                  have hle : c.rank + 1 ≤ t.rank := by
                    apply Nat.succ_le_of_lt lt
                  constructor
                  . rw[← heq] at hle
                    apply lt_of_le_of_ne <;> assumption
                  . assumption
                  . assumption
        have hf₂ : IsHeapForest' r y := by
          cases ht₁
          apply IsHeapForest'_weaken
          . assumption
          . apply Nat.le_of_lt 
            assumption
        have min_le : min (hRank y) (hRank (combine le u c :: z)) ≤ hRank (mergeNodes le y (combine le u c :: z)) := by
          apply min_hRank_mergeNodes hf₂ hf
        repeat rw[hrank_of_cons] at *
        rw[Nat.min_eq] at min_le
        rw[rank_combine heq] at *
        split at min_le
        . unfold bne at *
          rw[Nat.not_beq_eq_true_eq] at *
          simp_all
        . assumption
      . rw[hrank_of_cons, rank_combine heq]
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank ≠ c.rank
Tactic:
apply ne_of_lt
State after:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank < c.rank

State before:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank < c.rank
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
⊢ c.rank ≠ u.rank
Tactic:
apply ne_of_lt
State after:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
⊢ c.rank < u.rank

State before:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
⊢ c.rank < u.rank
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
hneq : c.rank ≠ u.rank
⊢ c.rank = u.rank
Tactic:
apply Eq.symm heq
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' r (combine le u c :: y)
Tactic:
constructor
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ r < (combine le u c).rank

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

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y

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

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

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y
Tactic:
. rw[rank_combine heq] at *
  cases ht₁ with | cons lt _ _ =>
    apply Nat.lt_succ_of_lt lt
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsBinTree (combine le u c)

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y

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

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

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

State before:
case a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : (u.rank + 1 != hRank y) = true
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝¹ : IsBinTree u
lt : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ r < u.rank + 1
Tactic:
apply Nat.lt_succ_of_lt lt
State after:
no goals

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

State before:
case a.cons.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
a✝⁴ : IsBinTree u
a✝³ : r < u.rank
hf : IsHeapForest' u.rank y
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ IsHeapForest' (combine le u c).rank y
Tactic:
match hf with
| .nil =>
  constructor
| .cons (t := t) (ts := ts) lt _ _ =>
  rename_i neq
  rw[rank_combine heq, hrank_of_cons] at *
  unfold bne at neq
  rw[Nat.not_beq_eq_true_eq] at neq
  have : u.rank + 1 ≤ t.rank := by
    apply Nat.succ_le_of_lt lt
  constructor
  . apply lt_of_le_of_ne <;> assumption
  . assumption
  . 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank z) = true
a✝⁴ : IsBinTree u
a✝³ : r < u.rank
hf : IsHeapForest' u.rank y
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
h✝ : ((combine le u c).rank != hRank []) = true
⊢ IsHeapForest' (combine le u c).rank []
Tactic:
constructor
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)
Tactic:
rename_i neq
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬((combine le u c).rank != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬((combine le u c).rank != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)
Tactic:
rw[rank_combine heq, hrank_of_cons] at *
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (u.rank + 1 != t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (u.rank + 1 != t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
unfold bne at neq
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (!u.rank + 1 == t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (!u.rank + 1 == t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
rw[Nat.not_beq_eq_true_eq] at neq
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
have : u.rank + 1 ≤ t.rank := by
  apply Nat.succ_le_of_lt lt
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
constructor
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ u.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ u.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. apply lt_of_le_of_ne <;> assumption
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. assumption
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ u.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
⊢ IsHeapForest' r z
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ IsHeapForest' r z

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

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ ℕ

State before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ IsHeapForest' ?cons.n z

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ ℕ
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ r ≤ c.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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ r ≤ c.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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
hf₂ : IsHeapForest' r z
⊢ min (hRank (combine le u c :: y)) (hRank z) ≤ hRank (mergeNodes le (combine le u c :: y) z)
Tactic:
apply min_hRank_mergeNodes hf hf₂
State after:
no goals

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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
hf₂ : IsHeapForest' r z
min_le : min (hRank (combine le u c :: y)) (hRank z) ≤ hRank (mergeNodes le (combine le u c :: y) z)
⊢ u.rank + 1 ≤ hRank (mergeNodes le (combine le u c :: y) z)
Tactic:
rw[hrank_of_cons] at *
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
hf₂ : IsHeapForest' r z
min_le : min (combine le u c).rank (hRank z) ≤ hRank (mergeNodes le (combine le u c :: y) z)
⊢ u.rank + 1 ≤ hRank (mergeNodes le (combine le u c :: y) z)

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

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

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank z

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

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

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank z
Tactic:
. rw[rank_combine heq] at *
  cases ht₂ with | cons lt _ _ =>
    rw[← heq] at lt
    apply Nat.lt_succ_of_lt lt
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
⊢ IsBinTree (combine le u c)

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank z

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

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

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

State before:
case a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬(u.rank + 1 != hRank y) = true
h✝ : (u.rank + 1 != hRank z) = true
a✝¹ : IsBinTree c
lt : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ r < u.rank + 1
Tactic:
rw[← heq] at lt
State after:
case a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬(u.rank + 1 != hRank y) = true
h✝ : (u.rank + 1 != hRank z) = true
a✝¹ : IsBinTree c
lt : r < u.rank
a✝ : IsHeapForest' c.rank z
⊢ r < u.rank + 1

State before:
case a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬(u.rank + 1 != hRank y) = true
h✝ : (u.rank + 1 != hRank z) = true
a✝¹ : IsBinTree c
lt : r < u.rank
a✝ : IsHeapForest' c.rank z
⊢ r < u.rank + 1
Tactic:
apply Nat.lt_succ_of_lt lt
State after:
no goals

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

State before:
case a.cons.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
a✝⁴ : IsBinTree u
a✝³ : r < u.rank
a✝² : IsHeapForest' u.rank y
a✝¹ : IsBinTree c
a✝ : r < c.rank
hf : IsHeapForest' c.rank z
⊢ IsHeapForest' (combine le u c).rank z
Tactic:
match hf with
| .nil =>
  constructor
| .cons (t := t) (ts := ts) lt _ _ =>
  rename_i neq
  rw[rank_combine heq, hrank_of_cons] at *
  unfold bne at neq
  rw[Nat.not_beq_eq_true_eq] at neq
  have hle : c.rank + 1 ≤ t.rank := by
    apply Nat.succ_le_of_lt lt
  constructor
  . rw[← heq] at hle
    apply lt_of_le_of_ne <;> assumption
  . assumption
  . 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
a✝⁴ : IsBinTree u
a✝³ : r < u.rank
a✝² : IsHeapForest' u.rank y
a✝¹ : IsBinTree c
a✝ : r < c.rank
hf : IsHeapForest' c.rank z
h✝ : ((combine le u c).rank != hRank []) = true
⊢ IsHeapForest' (combine le u c).rank []
Tactic:
constructor
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)
Tactic:
rename_i neq
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬((combine le u c).rank != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬((combine le u c).rank != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)
Tactic:
rw[rank_combine heq, hrank_of_cons] at *
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (u.rank + 1 != t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (u.rank + 1 != t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
unfold bne at neq
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (!u.rank + 1 == t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (!u.rank + 1 == t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
rw[Nat.not_beq_eq_true_eq] at neq
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
have hle : c.rank + 1 ≤ t.rank := by
  apply Nat.succ_le_of_lt lt
State after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
constructor
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ u.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ u.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. rw[← heq] at hle
  apply lt_of_le_of_ne <;> assumption
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. assumption
State after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts

State before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ c.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
⊢ IsHeapForest' r y
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' r y

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

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ ℕ

State before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' ?cons.n y

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ 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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ ℕ
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ r ≤ u.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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ r ≤ u.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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
hf₂ : IsHeapForest' r y
⊢ min (hRank y) (hRank (combine le u c :: z)) ≤ hRank (mergeNodes le y (combine le u c :: z))
Tactic:
apply min_hRank_mergeNodes hf₂ hf
State after:
no goals

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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
hf₂ : IsHeapForest' r y
min_le : min (hRank y) (hRank (combine le u c :: z)) ≤ hRank (mergeNodes le y (combine le u c :: z))
⊢ u.rank + 1 ≤ hRank (mergeNodes le y (combine le u c :: z))
Tactic:
rw[hrank_of_cons] at *
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
hf₂ : IsHeapForest' r y
min_le : min (hRank y) (combine le u c).rank ≤ hRank (mergeNodes le y (combine le u c :: z))
⊢ u.rank + 1 ≤ hRank (mergeNodes le y (combine le u c :: z))