Theorem: project.IsHeap_merge
Proof state before:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ h₁.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
Tactic:
. have : h₁.rank + 1 ≤ t.rank := by
    apply Nat.succ_le_of_lt lt
  apply lt_of_le_of_ne this
  rw[hrank_of_cons] at *
  unfold bne at *
  rw[Nat.not_beq_eq_true_eq] at *
  assumption
Proof state after:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts