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 α)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₁) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inl.hys.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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
h✝³ : (h₁.rank + 1 != hRank t₂) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' (h₁.rank + 1) t₂
Tactic:
match hf with 
| .nil =>
  constructor
| .cons (t := t) (ts := ts) lt _ _ =>
  rw[← heq] at lt
  have b : h₁.rank + 1 ≤ t.rank := by
    apply Nat.succ_le_of_lt lt
  rw[hrank_of_cons] at *
  constructor
  . unfold bne at *
    rw[Nat.not_beq_eq_true_eq] at *
    apply lt_of_le_of_ne <;> assumption
  repeat 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₁)
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✝ : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
h✝ : (h₁.rank + 1 != hRank []) = true
⊢ IsHeapForest' (h₁.rank + 1) []
Tactic:
constructor
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₁)
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✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₂.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
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₁)
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✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
have b : 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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
b : h₁.rank + 1 ≤ t.rank
⊢ IsHeapForest' (h₁.rank + 1) (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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
b : h₁.rank + 1 ≤ t.rank
⊢ IsHeapForest' (h₁.rank + 1) (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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != t.rank) = true
b : h₁.rank + 1 ≤ t.rank
⊢ IsHeapForest' (h₁.rank + 1) (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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != t.rank) = true
b : h₁.rank + 1 ≤ t.rank
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
constructor
Proof state after:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != t.rank) = true
b : h₁.rank + 1 ≤ t.rank
⊢ h₁.rank + 1 < t.rank

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

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

case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != t.rank) = true
b : h₁.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
repeat 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₁)
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✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ h₁.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : (h₁.rank + 1 != t.rank) = true
b : h₁.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
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₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
h✝¹ : ((combine le h₁ h₂).rank != hRank t₁) = false
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inr.a.cons.cons
α : 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
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₂
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
have ih := IsHeap_merge hf hf₂
Proof state after:
case inr.inr.inr.inr.a.cons.cons
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inr.a.cons.cons
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
have hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂) := by 
  rw[← heq] at hf₂
  apply min_hRank_mergeNodes hf hf₂
Proof state after:
case inr.inr.inr.inr.a.cons.cons
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inr.a.cons.cons
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
by_cases (t₁ = [] ∧ t₂ = [])
Proof state after:
case pos
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : t₁ = [] ∧ t₂ = []
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)

case neg
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case pos
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : t₁ = [] ∧ t₂ = []
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)

case neg
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
. have he₁ := h.left
  have he₂ := h.right
  simp[he₁, he₂]
  constructor
Proof state after:
case neg
α : 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
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
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
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
Tactic:
rw[← heq] at hf₂
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
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
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
h✝¹ : (h₁.rank + 1 != hRank t₁) = false
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₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
Tactic:
apply min_hRank_mergeNodes hf hf₂
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
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 t₁ ≤ hRank (mergeNodes le t₁ [])
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ [])
Tactic:
rw[empty_heap_merge_right] 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
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 t₁ ≤ hRank t₁
⊢ h₁.rank + 1 < hRank t₁
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
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 t₁ ≤ hRank t₁
⊢ h₁.rank + 1 < hRank t₁
Tactic:
match hf with
| .nil =>
  contradiction
| .cons (t := t) (ts := ts) _ _ _ =>
  rw[hrank_of_cons] at *
  unfold bne at *
  rw[Bool.not_eq_false', beq_iff_eq] at *
  simp at *
  contradiction
Proof state after:
no goals