internlm/Lean-Github huggingface dataset:
Theorem: project.min_hRank_mergeNodes
Proof state before:
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✝)
Tactic:
. contradiction
Proof state after:
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✝)
Theorem: project.min_hRank_mergeNodes
Proof state before:
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✝)
Tactic:
. rw[hrank_of_cons]
  apply Nat.le_of_lt
  assumption
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
case inr.inr.inr.inl.a.inr.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.inr.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.inr.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✝)
Theorem: project.min_hRank_mergeNodes
Proof state before:
case inr.inr.inr.inl.a.inr.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.inr.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✝)
Tactic:
. contradiction
Proof state after:
case inr.inr.inr.inl.a.inr.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✝)
Theorem: project.min_hRank_mergeNodes
Proof state before:
case inr.inr.inr.inl.a.inr.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✝)
Tactic:
. rw[hrank_of_cons]
  apply Nat.le_of_lt
  assumption
Proof state after:
no goals
Theorem: project.min_hRank_mergeNodes
Proof state before:
case inr.inr.inr.inr
α : 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 (combine le h₁ h₂ :: mergeNodes le t₁ t₂)
Tactic:
rw[hrank_of_cons]
Proof state after:
case inr.inr.inr.inr
α : 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 ≤ (combine le h₁ h₂).rank
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₂)
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.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
⊢ u.rank = c.rank → u.rank + 1 ≤ hRank (mergeNodes le (u :: y) (c :: z))
Tactic:
intros heq
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤ hRank (mergeNodes le (u :: y) (c :: z))
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤ hRank (mergeNodes le (u :: y) (c :: z))
Tactic:
unfold mergeNodes
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤
    hRank
      (if u.rank < c.rank then u :: mergeNodes le y (c :: z)
      else
        if c.rank < u.rank then c :: mergeNodes le z (u :: y)
        else
          let merged := combine le u c;
          let r := merged.rank;
          if (r != hRank y) = true then
            if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
          else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
⊢ u.rank + 1 ≤
    hRank
      (if u.rank < c.rank then u :: mergeNodes le y (c :: z)
      else
        if c.rank < u.rank then c :: mergeNodes le z (u :: y)
        else
          let merged := combine le u c;
          let r := merged.rank;
          if (r != hRank y) = true then
            if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
          else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
Tactic:
split
Proof state after:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank + 1 ≤ hRank (u :: mergeNodes le y (c :: z))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank + 1 ≤ hRank (u :: mergeNodes le y (c :: z))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
Tactic:
. have : u.rank ≠ c.rank := by
    apply ne_of_lt
    assumption
  contradiction
Proof state after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank ≠ c.rank
Tactic:
apply ne_of_lt
Proof state after:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank < c.rank
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank < c.rank
Tactic:
assumption
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
⊢ c.rank ≠ u.rank
Tactic:
apply ne_of_lt
Proof state after:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
⊢ c.rank < u.rank
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
⊢ c.rank < u.rank
Tactic:
assumption
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝¹ : ¬u.rank < c.rank
h✝ : c.rank < u.rank
hneq : c.rank ≠ u.rank
⊢ c.rank = u.rank
Tactic:
apply Eq.symm heq
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' r (combine le u c :: y)
Tactic:
constructor
Proof state after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ r < (combine le u c).rank

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsBinTree (combine le u c)

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ r < (combine le u c).rank

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsBinTree (combine le u c)

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y
Tactic:
. rw[rank_combine heq] at *
  cases ht₁ with | cons lt _ _ =>
    apply Nat.lt_succ_of_lt lt
Proof state after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsBinTree (combine le u c)

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsBinTree (combine le u c)

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y
Tactic:
. cases ht₁
  cases ht₂
  apply combine_IsBinTree <;> assumption
Proof state after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
⊢ IsHeapForest' (combine le u c).rank y