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

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂) := by
  apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have ht₂ : IsHeapForest' h₁.rank (t :: ts) := by
  rw[← heq] at *
  apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts)) := by
  apply hRank_mergeNodes_cons ht₁ ht₂
  simp_all
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rename_i heq₂ _
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rw[heq₂]
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ t₂.rank < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ t₂.rank < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
apply Nat.lt_of_succ_le this
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : (h₁.rank + 1 != t.rank) = false
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : (h₁.rank + 1 != t₂.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : ¬(t₂ :: ts₂ = [] ∧ t :: ts = [])
h✝ : t₂.rank ≤ hRank (t :: ts)
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rw[hrank_of_cons] at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : (h₁.rank + 1 != t.rank) = false
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : (h₁.rank + 1 != t₂.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : ¬(t₂ :: ts₂ = [] ∧ t :: ts = [])
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
⊢ IsHeapForest' h₁.rank (t₂ :: ts₂)
Tactic:
apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)
Tactic:
rw[← heq] at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₁.rank
hf₂ : IsHeapForest' h₁.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₁.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₁.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₁.rank
hf₂ : IsHeapForest' h₁.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₁.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₁.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)
Tactic:
apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
apply hRank_mergeNodes_cons ht₁ ht₂
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank = t.rank

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank = t.rank
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝² : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ [])
h : ¬(t₁ = [] ∧ [] = [])
h✝ : ¬hRank t₁ ≤ hRank []
hle : hRank [] ≤ hRank (mergeNodes le t₁ [])
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ [])
Tactic:
rw[empty_heap_merge_right] at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝² : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) t₁
h : ¬(t₁ = [] ∧ [] = [])
h✝ : ¬hRank t₁ ≤ hRank []
hle : hRank [] ≤ hRank t₁
⊢ h₁.rank + 1 < hRank t₁

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝² : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) t₁
h : ¬(t₁ = [] ∧ [] = [])
h✝ : ¬hRank t₁ ≤ hRank []
hle : hRank [] ≤ hRank t₁
⊢ h₁.rank + 1 < hRank t₁
Tactic:
cases hf
State after:
case nil
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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✝³ : IsBinTree h₁
a✝² : rx < h₁.rank
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) []
h : ¬([] = [] ∧ [] = [])
h✝ : ¬hRank [] ≤ hRank []
hle : hRank [] ≤ hRank []
⊢ h₁.rank + 1 < hRank []

case cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² : (h₁.rank + 1 != hRank []) = false
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t✝ :: ts✝)
h : ¬(t✝ :: ts✝ = [] ∧ [] = [])
h✝ : ¬hRank (t✝ :: ts✝) ≤ hRank []
hle : hRank [] ≤ hRank (t✝ :: ts✝)
⊢ h₁.rank + 1 < hRank (t✝ :: ts✝)

State before:
case nil
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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✝³ : IsBinTree h₁
a✝² : rx < h₁.rank
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) []
h : ¬([] = [] ∧ [] = [])
h✝ : ¬hRank [] ≤ hRank []
hle : hRank [] ≤ hRank []
⊢ h₁.rank + 1 < hRank []

case cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² : (h₁.rank + 1 != hRank []) = false
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t✝ :: ts✝)
h : ¬(t✝ :: ts✝ = [] ∧ [] = [])
h✝ : ¬hRank (t✝ :: ts✝) ≤ hRank []
hle : hRank [] ≤ hRank (t✝ :: ts✝)
⊢ h₁.rank + 1 < hRank (t✝ :: ts✝)
Tactic:
. contradiction
State after:
case cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² : (h₁.rank + 1 != hRank []) = false
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t✝ :: ts✝)
h : ¬(t✝ :: ts✝ = [] ∧ [] = [])
h✝ : ¬hRank (t✝ :: ts✝) ≤ hRank []
hle : hRank [] ≤ hRank (t✝ :: ts✝)
⊢ h₁.rank + 1 < hRank (t✝ :: ts✝)

State before:
case cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
h✝² : (h₁.rank + 1 != hRank []) = false
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t✝ :: ts✝)
h : ¬(t✝ :: ts✝ = [] ∧ [] = [])
h✝ : ¬hRank (t✝ :: ts✝) ≤ hRank []
hle : hRank [] ≤ hRank (t✝ :: ts✝)
⊢ h₁.rank + 1 < hRank (t✝ :: ts✝)
Tactic:
. rw[hrank_of_cons] at *
  unfold bne at *
  rw[Bool.not_eq_false', beq_iff_eq] at *
  simp at *
  contradiction
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (h₁.rank + 1 != hRank (t :: ts)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ hRank (t :: ts)
hle : hRank (t :: ts) ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
rw[hrank_of_cons] at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (h₁.rank + 1 != t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (h₁.rank + 1 != t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
unfold bne at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (!h₁.rank + 1 == t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (!h₁.rank + 1 == t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
rw[Bool.not_eq_false', beq_iff_eq] at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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₁
heq : h₁.rank = h₂.rank
a✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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₁
heq : h₁.rank = h₂.rank
a✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
simp at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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₁
heq : h₁.rank = h₂.rank
a✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
h : True
h✝ : t.rank < hRank t₁
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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₁
heq : h₁.rank = h₂.rank
a✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
h : True
h✝ : t.rank < hRank t₁
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
match hf with
| .nil =>
  contradiction
| .cons (t := t₂) (ts := ts₂) _ _ _ =>
  rw[hrank_of_cons] at *
  simp at *
  have ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂) := by
    apply IsHeapForest'_of_IsHeapForest' <;> assumption
  have ht₂ : IsHeapForest' h₁.rank (t :: ts) := by
    rw[← heq] at *
    apply IsHeapForest'_of_IsHeapForest' <;> assumption
  have : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts)) := by
    apply hRank_mergeNodes_cons ht₁ ht₂
    simp_all
  rename_i heq₂ _
  rw[heq₂]
  apply Nat.lt_of_succ_le this
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
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✝⁶ : IsBinTree h₁
a✝⁵ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁴ : IsBinTree h₂
a✝³ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
a✝² : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
h✝¹ : h₁.rank + 1 = hRank []
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le [] (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le [] (t :: ts))
h✝ : t.rank < hRank []
⊢ h₁.rank + 1 < hRank (mergeNodes le [] (t :: ts))
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = hRank (t₂ :: ts₂)
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < hRank (t₂ :: ts₂)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rw[hrank_of_cons] at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂) := by
  apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have ht₂ : IsHeapForest' h₁.rank (t :: ts) := by
  rw[← heq] at *
  apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts)) := by
  apply hRank_mergeNodes_cons ht₁ ht₂
  simp_all
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rename_i heq₂ _
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rw[heq₂]
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ t₂.rank < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ t₂.rank < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
apply Nat.lt_of_succ_le this
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
⊢ IsHeapForest' h₁.rank (t₂ :: ts₂)
Tactic:
apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)
Tactic:
rw[← heq] at *
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₁.rank
hf₂ : IsHeapForest' h₁.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₁.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₁.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₁.rank
hf₂ : IsHeapForest' h₁.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₁.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₁.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)
Tactic:
apply IsHeapForest'_of_IsHeapForest' <;> assumption
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
apply hRank_mergeNodes_cons ht₁ ht₂
State after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank = t.rank

State before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
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✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank = t.rank
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
le : α → α → Bool
_x✝ :
  (rx : ℕ) ×'
    (xs : List (BinTree α)) ×' (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁷ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y _x✝ →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
rx : ℕ
xs✝ : (xs : List (BinTree α)) ×' (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁶ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := xs✝ } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
xs : List (BinTree α)
ry✝ : (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁵ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := ry✝ } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
ry : ℕ
ys✝ : (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁴ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := { fst := ry, snd := ys✝ } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
ys : List (BinTree α)
hxs✝¹ : (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹³ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := { fst := ry, snd := { fst := ys, snd := hxs✝¹ } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
hxs✝ : IsHeapForest' rx xs
hys✝ : IsHeapForest' ry ys
a✝¹² :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rx,
          snd := { fst := xs, snd := { fst := ry, snd := { fst := ys, snd := { fst := hxs✝, snd := hys✝ } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
x✝² :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rx,
          snd :=
            { fst := h₁ :: t₁, snd := { fst := ry, snd := { fst := h₂ :: t₂, snd := { fst := hxs, snd := hys } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.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
heq : h₁.rank = h₂.rank
rank✝ : ℕ
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝¹¹ : rank✝ < t✝.rank
a✝¹⁰ : IsBinTree t✝
a✝⁹ : IsHeapForest' t✝.rank ts✝
x✝¹ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rank✝,
          snd :=
            { fst := t✝ :: ts✝,
              snd :=
                { fst := ry,
                  snd :=
                    { fst := h₂ :: t₂, snd := { fst := (_ : IsHeapForest' rank✝ (t✝ :: ts✝)), snd := hys } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h✝⁵ : rx = rank✝
a✝⁸ : rx < t✝.rank
h✝⁴ : h₁ :: t₁ = t✝ :: ts✝
head_eq✝¹ : h₁ = t✝
a✝⁷ : IsBinTree h₁
hf✝ : IsHeapForest' h₁.rank ts✝
a✝⁶ : rx < h₁.rank
tail_eq✝¹ : t₁ = ts✝
hf : IsHeapForest' h₁.rank t₁
h✝³ : HEq hxs (_ : IsHeapForest' rx (h₁ :: t₁))
rank : ℕ
t : BinTree α
ts : List (BinTree α)
a✝⁵ : rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
x✝ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rank✝,
          snd :=
            { fst := t✝ :: ts✝,
              snd :=
                { fst := rank,
                  snd :=
                    { fst := t :: ts,
                      snd :=
                        { fst := (_ : IsHeapForest' rank✝ (t✝ :: ts✝)),
                          snd := (_ : IsHeapForest' rank (t :: ts)) } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h✝² : ry = rank
a✝² : ry < t.rank
h✝¹ : h₂ :: t₂ = t :: ts
head_eq✝ : h₂ = t
a✝¹ : IsBinTree h₂
hf₂✝ : IsHeapForest' h₂.rank ts
a✝ : ry < h₂.rank
tail_eq✝ : t₂ = ts
hf₂ : IsHeapForest' h₂.rank t₂
h✝ : HEq hys (_ : IsHeapForest' ry (h₂ :: t₂))
⊢ (invImage
        (fun a ↦
          PSigma.casesOn a
            fun rx snd ↦
              PSigma.casesOn snd
                fun xs snd ↦
                  PSigma.casesOn snd
                    fun ry snd ↦
                      PSigma.casesOn snd fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
        instWellFoundedRelation).1
    { fst := h₁.rank,
      snd := { fst := t₁, snd := { fst := h₂.rank, snd := { fst := t₂, snd := { fst := hf, snd := hf₂ } } } } }
    { fst := rank✝,
      snd :=
        { fst := t✝ :: ts✝,
          snd :=
            { fst := rank,
              snd :=
                { fst := t :: ts,
                  snd :=
                    { fst := (_ : IsHeapForest' rank✝ (t✝ :: ts✝)), snd := (_ : IsHeapForest' rank (t :: ts)) } } } } }
Tactic:
simp_wf
State after:
α : Type u_1
le : α → α → Bool
_x✝ :
  (rx : ℕ) ×'
    (xs : List (BinTree α)) ×' (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁷ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y _x✝ →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
rx : ℕ
xs✝ : (xs : List (BinTree α)) ×' (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁶ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := xs✝ } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
xs : List (BinTree α)
ry✝ : (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁵ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := ry✝ } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
ry : ℕ
ys✝ : (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁴ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := { fst := ry, snd := ys✝ } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
ys : List (BinTree α)
hxs✝¹ : (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹³ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := { fst := ry, snd := { fst := ys, snd := hxs✝¹ } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
hxs✝ : IsHeapForest' rx xs
hys✝ : IsHeapForest' ry ys
a✝¹² :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rx,
          snd := { fst := xs, snd := { fst := ry, snd := { fst := ys, snd := { fst := hxs✝, snd := hys✝ } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
x✝² :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rx,
          snd :=
            { fst := h₁ :: t₁, snd := { fst := ry, snd := { fst := h₂ :: t₂, snd := { fst := hxs, snd := hys } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.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
heq : h₁.rank = h₂.rank
rank✝ : ℕ
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝¹¹ : rank✝ < t✝.rank
a✝¹⁰ : IsBinTree t✝
a✝⁹ : IsHeapForest' t✝.rank ts✝
x✝¹ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rank✝,
          snd :=
            { fst := t✝ :: ts✝,
              snd :=
                { fst := ry,
                  snd :=
                    { fst := h₂ :: t₂, snd := { fst := (_ : IsHeapForest' rank✝ (t✝ :: ts✝)), snd := hys } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h✝⁵ : rx = rank✝
a✝⁸ : rx < t✝.rank
h✝⁴ : h₁ :: t₁ = t✝ :: ts✝
head_eq✝¹ : h₁ = t✝
a✝⁷ : IsBinTree h₁
hf✝ : IsHeapForest' h₁.rank ts✝
a✝⁶ : rx < h₁.rank
tail_eq✝¹ : t₁ = ts✝
hf : IsHeapForest' h₁.rank t₁
h✝³ : HEq hxs (_ : IsHeapForest' rx (h₁ :: t₁))
rank : ℕ
t : BinTree α
ts : List (BinTree α)
a✝⁵ : rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
x✝ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rank✝,
          snd :=
            { fst := t✝ :: ts✝,
              snd :=
                { fst := rank,
                  snd :=
                    { fst := t :: ts,
                      snd :=
                        { fst := (_ : IsHeapForest' rank✝ (t✝ :: ts✝)),
                          snd := (_ : IsHeapForest' rank (t :: ts)) } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h✝² : ry = rank
a✝² : ry < t.rank
h✝¹ : h₂ :: t₂ = t :: ts
head_eq✝ : h₂ = t
a✝¹ : IsBinTree h₂
hf₂✝ : IsHeapForest' h₂.rank ts
a✝ : ry < h₂.rank
tail_eq✝ : t₂ = ts
hf₂ : IsHeapForest' h₂.rank t₂
h✝ : HEq hys (_ : IsHeapForest' ry (h₂ :: t₂))
⊢ List.length t₁ + List.length t₂ < Nat.succ (List.length ts✝) + Nat.succ (List.length ts)

State before:
α : Type u_1
le : α → α → Bool
_x✝ :
  (rx : ℕ) ×'
    (xs : List (BinTree α)) ×' (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁷ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y _x✝ →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
rx : ℕ
xs✝ : (xs : List (BinTree α)) ×' (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁶ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := xs✝ } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
xs : List (BinTree α)
ry✝ : (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁵ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := ry✝ } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
ry : ℕ
ys✝ : (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹⁴ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := { fst := ry, snd := ys✝ } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
ys : List (BinTree α)
hxs✝¹ : (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys
a✝¹³ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y { fst := rx, snd := { fst := xs, snd := { fst := ry, snd := { fst := ys, snd := hxs✝¹ } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
hxs✝ : IsHeapForest' rx xs
hys✝ : IsHeapForest' ry ys
a✝¹² :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rx,
          snd := { fst := xs, snd := { fst := ry, snd := { fst := ys, snd := { fst := hxs✝, snd := hys✝ } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
x✝² :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rx,
          snd :=
            { fst := h₁ :: t₁, snd := { fst := ry, snd := { fst := h₂ :: t₂, snd := { fst := hxs, snd := hys } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.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
heq : h₁.rank = h₂.rank
rank✝ : ℕ
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝¹¹ : rank✝ < t✝.rank
a✝¹⁰ : IsBinTree t✝
a✝⁹ : IsHeapForest' t✝.rank ts✝
x✝¹ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rank✝,
          snd :=
            { fst := t✝ :: ts✝,
              snd :=
                { fst := ry,
                  snd :=
                    { fst := h₂ :: t₂, snd := { fst := (_ : IsHeapForest' rank✝ (t✝ :: ts✝)), snd := hys } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h✝⁵ : rx = rank✝
a✝⁸ : rx < t✝.rank
h✝⁴ : h₁ :: t₁ = t✝ :: ts✝
head_eq✝¹ : h₁ = t✝
a✝⁷ : IsBinTree h₁
hf✝ : IsHeapForest' h₁.rank ts✝
a✝⁶ : rx < h₁.rank
tail_eq✝¹ : t₁ = ts✝
hf : IsHeapForest' h₁.rank t₁
h✝³ : HEq hxs (_ : IsHeapForest' rx (h₁ :: t₁))
rank : ℕ
t : BinTree α
ts : List (BinTree α)
a✝⁵ : rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
x✝ :
  ∀
    (y :
      (rx : ℕ) ×'
        (xs : List (BinTree α)) ×'
          (ry : ℕ) ×' (ys : List (BinTree α)) ×' (_ : IsHeapForest' rx xs) ×' IsHeapForest' ry ys),
    (invImage
            (fun a ↦
              PSigma.casesOn a
                fun rx snd ↦
                  PSigma.casesOn snd
                    fun xs snd ↦
                      PSigma.casesOn snd
                        fun ry snd ↦
                          PSigma.casesOn snd
                            fun ys snd ↦ PSigma.casesOn snd fun hxs snd ↦ List.length xs + List.length ys)
            instWellFoundedRelation).1
        y
        { fst := rank✝,
          snd :=
            { fst := t✝ :: ts✝,
              snd :=
                { fst := rank,
                  snd :=
                    { fst := t :: ts,
                      snd :=
                        { fst := (_ : IsHeapForest' rank✝ (t✝ :: ts✝)),
                          snd := (_ : IsHeapForest' rank (t :: ts)) } } } } } →
      IsHeapForest' (min y.1 y.2.2.1) (mergeNodes le y.2.1 y.2.2.2.1)
h✝² : ry = rank
a✝² : ry < t.rank
h✝¹ : h₂ :: t₂ = t :: ts
head_eq✝ : h₂ = t
a✝¹ : IsBinTree h₂
hf₂✝ : IsHeapForest' h₂.rank ts
a✝ : ry < h₂.rank
tail_eq✝ : t₂ = ts
hf₂ : IsHeapForest' h₂.rank t₂
h✝ : HEq hys (_ : IsHeapForest' ry (h₂ :: t₂))
⊢ List.length t₁ + List.length t₂ < Nat.succ (List.length ts✝) + Nat.succ (List.length ts)
Tactic:
simp_arith [*]
State after:
no goals