internlm/Lean-Github huggingface dataset:
Theorem: project.min_hRank_mergeNodes
Proof state before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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' t.rank ts
Tactic:
. rw[hrank_of_cons] at *
  rename_i neq
  unfold bne at neq
  rw[Nat.not_beq_eq_true_eq] at neq
  have : h₁.rank + 1 ≤  t.rank := by
    apply Nat.succ_le_of_lt lt
  apply lt_of_le_of_ne <;> assumption
Proof state after:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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' t.rank ts
Theorem: project.min_hRank_mergeNodes
Proof state before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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' t.rank ts
Tactic:
repeat assumption
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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
neq : ¬h₁.rank + 1 = t.rank
⊢ h₁.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
case a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (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✝² : r < 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' t.rank ts
Tactic:
assumption
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
⊢ IsHeapForest' r t₂
Tactic:
cases ht₂
Proof state after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' r t₂
Theorem: project.min_hRank_mergeNodes
Proof state before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' r t₂
Tactic:
apply IsHeapForest'_weaken
Proof state after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' ?cons.n t₂

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ ℕ
Theorem: project.min_hRank_mergeNodes
Proof state before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' ?cons.n t₂

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ ℕ
Tactic:
. assumption
Proof state after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ h₂.rank
Theorem: project.min_hRank_mergeNodes
Proof state before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
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
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
a✝² : IsBinTree h₂
a✝¹ : r < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ r ≤ h₂.rank
Tactic:
. apply Nat.le_of_lt
  assumption
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (combine le h₁ h₂).rank (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) 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.min_hRank_mergeNodes
Proof state before:
case inr.inr.inl.inr.a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (h₁.rank + 1) (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) 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
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ min (h₁.rank + 1) (hRank t₂)
Tactic:
rw[Nat.min_eq]
Proof state after:
case inr.inr.inl.inr.a
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : (h₁.rank + 1 != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (h₁.rank + 1) (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) 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
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ if h₁.rank + 1 ≤ hRank t₂ then h₁.rank + 1 else hRank t₂
Theorem: project.min_hRank_mergeNodes
Proof state before:
case inr.inr.inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
⊢ min h₁.rank (hRank (h₂ :: t₂)) ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
Tactic:
rw[hrank_of_cons]
Proof state after:
case inr.inr.inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
⊢ min h₁.rank h₂.rank ≤ hRank (mergeNodes le t₁ (combine le h₁ h₂ :: t₂))
Theorem: project.min_hRank_mergeNodes
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
⊢ IsHeapForest' r t₁
Tactic:
cases ht₁
Proof state after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' r t₁
Theorem: project.min_hRank_mergeNodes
Proof state before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' r t₁
Tactic:
apply IsHeapForest'_weaken
Proof state after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' ?cons.n t₁

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ ℕ
Theorem: project.min_hRank_mergeNodes
Proof state before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' ?cons.n t₁

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ ℕ
Tactic:
. assumption
Proof state after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ h₁.rank
Theorem: project.min_hRank_mergeNodes
Proof state before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
a✝² : IsBinTree h₁
a✝¹ : r < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ r ≤ h₁.rank
Tactic:
. apply Nat.le_of_lt
  assumption
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
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
hf : IsHeapForest' r t₁
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)
Tactic:
simp at *
Proof state after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r 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
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)
Theorem: project.min_hRank_mergeNodes
Proof state before:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r 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
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)
Tactic:
have heq : h₁.rank = h₂.rank := by
  apply Nat.le_antisymm <;> assumption
Proof state after:
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
hf : IsHeapForest' r 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
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)