internlm/Lean-Github huggingface dataset:
Theorem: project.IsHeap_merge
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != hRank (t :: ts)) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬hRank (t :: ts) ≤ hRank []
min_le : hRank [] ≤ hRank (t :: ts)
⊢ h₁.rank + 1 < hRank (t :: ts)
Tactic:
rw[hrank_of_cons] at *
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Theorem: project.IsHeap_merge
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
unfold bne at hneq
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (!h₁.rank + 1 == t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Theorem: project.IsHeap_merge
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : (!h₁.rank + 1 == t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
rw[Nat.not_beq_eq_true_eq] at hneq
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Theorem: project.IsHeap_merge
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
have : h₁.rank + 1 ≤ t.rank := by
  apply Nat.succ_le_of_lt lt
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Theorem: project.IsHeap_merge
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
apply lt_of_le_of_ne <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq₂ : (h₁.rank + 1 != hRank []) = true
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : ¬t.rank ≤ hRank []
min_le : hRank [] ≤ t.rank
⊢ h₁.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != hRank (t :: ts)) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ hRank (t :: ts)
min_le : hRank (t :: ts) ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
rw[hrank_of_cons] at *
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
rw[← heq] at lt
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
have : h₁.rank + 1 ≤ t.rank := by
  apply Nat.succ_le_of_lt lt
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
unfold bne at hneq₂
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (!h₁.rank + 1 == t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (!h₁.rank + 1 == t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
rw[Nat.not_beq_eq_true_eq] at hneq₂
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
have : h₁.rank + 1 < t.rank := by
  apply lt_of_le_of_ne <;> assumption
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this✝ : h₁.rank + 1 ≤ t.rank
this : h₁.rank + 1 < t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this✝ : h₁.rank + 1 ≤ t.rank
this : h₁.rank + 1 < t.rank
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
apply lt_of_lt_of_le <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : (h₁.rank + 1 != t.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hneq₂ : ¬h₁.rank + 1 = t.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : ¬hRank t₁ ≤ t.rank
min_le : t.rank ≤ hRank (mergeNodes le t₁ (t :: ts))
this : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
apply lt_of_le_of_ne <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof 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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inr.hxs.a.cons
α : 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₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
lt : rx < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ rx < (combine le h₁ h₂).rank
Tactic:
rw[rank_combine heq]
Proof state after:
case inr.inr.inl.inr.hxs.a.cons
α : 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₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
lt : rx < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ rx < h₁.rank + 1