internlm/Lean-Github huggingface dataset:
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
heq : h₁.rank = h₂.rank
⊢ IsHeapForest' r (combine le h₁ h₂ :: t₂)
Tactic:
constructor
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₁)
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
⊢ r < (combine le h₁ h₂).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₁)
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
⊢ IsBinTree (combine le h₁ h₂)

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₁)
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' (combine le h₁ h₂).rank t₂
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₁)
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
⊢ r < (combine le h₁ h₂).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₁)
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
⊢ IsBinTree (combine le h₁ h₂)

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₁)
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' (combine le h₁ h₂).rank t₂
Tactic:
. cases ht₁
  rw[rank_combine heq] at *
  apply Nat.lt_succ_of_lt
  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₁)
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
⊢ IsBinTree (combine le h₁ h₂)

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₁)
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' (combine le h₁ h₂).rank t₂
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₁)
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
⊢ IsBinTree (combine le h₁ h₂)

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₁)
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' (combine le h₁ h₂).rank t₂
Tactic:
. cases ht₁
  cases ht₂
  apply combine_IsBinTree <;> 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₁)
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' (combine le h₁ h₂).rank t₂
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₁)
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' (combine le h₁ h₂).rank t₂
Tactic:
. rw[rank_combine heq] at *
  cases ht₂ with | cons _ _ hf₂ =>
    match hf₂ with
    | .nil => 
      constructor
    | .cons (t := t) (ts := ts) lt _ _ => 
      rename_i hneq
      rw[hrank_of_cons] at *
      constructor
      . rw[← heq] at lt
        unfold bne at hneq
        rw[Nat.not_beq_eq_true_eq] at hneq
        apply lt_of_le_of_ne <;> assumption
      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₁)
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
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
case a.cons
α : 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₁)
h✝³ : (h₁.rank + 1 != 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✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₂
a✝ : r < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' (h₁.rank + 1) t₂
Tactic:
match hf₂ with
| .nil => 
  constructor
| .cons (t := t) (ts := ts) lt _ _ => 
  rename_i hneq
  rw[hrank_of_cons] at *
  constructor
  . rw[← heq] at lt
    unfold bne at hneq
    rw[Nat.not_beq_eq_true_eq] at hneq
    apply lt_of_le_of_ne <;> assumption
  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₁)
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✝¹ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₂
a✝ : r < 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.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₁)
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✝¹ : (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' (h₁.rank + 1) (t :: ts)
Tactic:
rename_i hneq
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₁)
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✝ : (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
hneq : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
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₁)
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✝ : (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
hneq : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
rw[hrank_of_cons] 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
constructor
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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' t.rank ts
Tactic:
. rw[← heq] at lt
  unfold bne at hneq
  rw[Nat.not_beq_eq_true_eq] at hneq
  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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = true
⊢ IsHeapForest' t.rank ts
Tactic:
repeat assumption
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₁)
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✝ : (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
hneq : (h₁.rank + 1 != t.rank) = 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
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₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (combine le h₁ h₂).rank ≤ hRank (mergeNodes le t₁ (combine le h₁ 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₁.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.inr.inl.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 t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (h₁.rank + 1) ≤ hRank (mergeNodes le t₁ (combine le h₁ 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
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ min (hRank t₁) (h₁.rank + 1)
Tactic:
rw[Nat.min_eq]
Proof state after:
case inr.inr.inr.inl.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 t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (h₁.rank + 1) ≤ hRank (mergeNodes le t₁ (combine le h₁ 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
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ if hRank t₁ ≤ h₁.rank + 1 then hRank t₁ else h₁.rank + 1
Theorem: project.min_hRank_mergeNodes
Proof state before:
case inr.inr.inr.inl.a.inl.inl.cons
α : 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₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf : IsHeapForest' r t₁
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
ih : min (hRank t₁) (h₁.rank + 1) ≤ hRank (mergeNodes le t₁ (combine le h₁ 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
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : hRank t₁ ≤ h₁.rank + 1
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf₃ : IsHeapForest' h₁.rank t₁
⊢ h₁.rank ≤ hRank t₁
Tactic:
cases hf₃
Proof state after:
case inr.inr.inr.inl.a.inl.inl.cons.nil
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝¹ : IsBinTree h₁
a✝ : r < h₁.rank
hf : IsHeapForest' r []
ih : min (hRank []) (h₁.rank + 1) ≤ hRank (mergeNodes le [] (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank []) = false
h✝ : hRank [] ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank []

case inr.inr.inr.inl.a.inl.inl.cons.cons
α : Type u_1
le : α → α → Bool
r : ℕ
xs ys : List (BinTree α)
h₁ h₂ : BinTree α
t₂ : List (BinTree α)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝⁵ : (h₁.rank + 1 != hRank t₂) = true
hf₂ : IsHeapForest' r (combine le h₁ h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
h✝² : h₁.rank ≤ h₂.rank
a✝⁴ : IsBinTree h₁
a✝³ : r < h₁.rank
t✝ : BinTree α
ts✝ : List (BinTree α)
a✝² : IsBinTree t✝
a✝¹ : IsHeapForest' t✝.rank ts✝
a✝ : h₁.rank < t✝.rank
hf : IsHeapForest' r (t✝ :: ts✝)
ih : min (hRank (t✝ :: ts✝)) (h₁.rank + 1) ≤ hRank (mergeNodes le (t✝ :: ts✝) (combine le h₁ h₂ :: t₂))
h✝¹ : (h₁.rank + 1 != hRank (t✝ :: ts✝)) = false
h✝ : hRank (t✝ :: ts✝) ≤ h₁.rank + 1
⊢ h₁.rank ≤ hRank (t✝ :: ts✝)