internlm/Lean-Github huggingface dataset:
Theorem: project.hRank_mergeNodes_cons
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 : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
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
hf : IsHeapForest' r (combine le u c :: y)
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ r ≤ c.rank
Tactic:
. apply Nat.le_of_lt 
  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
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
hf₂ : IsHeapForest' r z
⊢ min (hRank (combine le u c :: y)) (hRank z) ≤ hRank (mergeNodes le (combine le u c :: y) z)
Tactic:
apply min_hRank_mergeNodes hf hf₂
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case inr.inr.inl.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
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
hf₂ : IsHeapForest' r z
min_le : min (hRank (combine le u c :: y)) (hRank z) ≤ hRank (mergeNodes le (combine le u c :: y) z)
⊢ u.rank + 1 ≤ hRank (mergeNodes le (combine le u c :: y) z)
Tactic:
rw[hrank_of_cons] at *
Proof state after:
case inr.inr.inl.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
h✝² : ¬c.rank < u.rank
h✝¹ : ((combine le u c).rank != hRank y) = true
h✝ : ¬((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: y)
hf₂ : IsHeapForest' r z
min_le : min (combine le u c).rank (hRank z) ≤ hRank (mergeNodes le (combine le u c :: y) z)
⊢ u.rank + 1 ≤ hRank (mergeNodes le (combine le u c :: 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
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 :: z)
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 z
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 z
Tactic:
. rw[rank_combine heq] at *
  cases ht₂ with | cons lt _ _ =>
    rw[← heq] at 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 z
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 z
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 z
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
⊢ IsHeapForest' (combine le u c).rank z
Tactic:
. cases ht₁ with | cons =>
    cases ht₂ with  | cons _ _ hf =>
      match hf with
      | .nil =>
        constructor
      | .cons (t := t) (ts := ts) lt _ _ =>
        rename_i neq
        rw[rank_combine heq, hrank_of_cons] at *
        unfold bne at neq
        rw[Nat.not_beq_eq_true_eq] at neq
        have hle : c.rank + 1 ≤ t.rank := by
          apply Nat.succ_le_of_lt lt
        constructor
        . rw[← heq] at hle
          apply lt_of_le_of_ne <;> assumption
        . assumption
        . assumption
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a.cons
α : 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)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬(u.rank + 1 != hRank y) = true
h✝ : (u.rank + 1 != hRank z) = true
a✝¹ : IsBinTree c
lt : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ r < u.rank + 1
Tactic:
rw[← heq] at lt
Proof state after:
case a.cons
α : 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)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬(u.rank + 1 != hRank y) = true
h✝ : (u.rank + 1 != hRank z) = true
a✝¹ : IsBinTree c
lt : r < u.rank
a✝ : IsHeapForest' c.rank z
⊢ r < u.rank + 1
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a.cons
α : 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)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬(u.rank + 1 != hRank y) = true
h✝ : (u.rank + 1 != hRank z) = true
a✝¹ : IsBinTree c
lt : r < u.rank
a✝ : IsHeapForest' c.rank z
⊢ r < u.rank + 1
Tactic:
apply Nat.lt_succ_of_lt lt
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a.cons
α : 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 (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
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' (combine le u c).rank z
Tactic:
cases ht₂ with  | cons _ _ hf =>
  match hf with
  | .nil =>
    constructor
  | .cons (t := t) (ts := ts) lt _ _ =>
    rename_i neq
    rw[rank_combine heq, hrank_of_cons] at *
    unfold bne at neq
    rw[Nat.not_beq_eq_true_eq] at neq
    have hle : c.rank + 1 ≤ t.rank := by
      apply Nat.succ_le_of_lt lt
    constructor
    . rw[← heq] at hle
      apply lt_of_le_of_ne <;> assumption
    . assumption
    . assumption
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a.cons.cons
α : 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 α)
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
a✝⁴ : IsBinTree u
a✝³ : r < u.rank
a✝² : IsHeapForest' u.rank y
a✝¹ : IsBinTree c
a✝ : r < c.rank
hf : IsHeapForest' c.rank z
⊢ IsHeapForest' (combine le u c).rank z
Tactic:
match hf with
| .nil =>
  constructor
| .cons (t := t) (ts := ts) lt _ _ =>
  rename_i neq
  rw[rank_combine heq, hrank_of_cons] at *
  unfold bne at neq
  rw[Nat.not_beq_eq_true_eq] at neq
  have hle : c.rank + 1 ≤ t.rank := by
    apply Nat.succ_le_of_lt lt
  constructor
  . rw[← heq] at hle
    apply lt_of_le_of_ne <;> assumption
  . assumption
  . 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 α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
a✝⁴ : IsBinTree u
a✝³ : r < u.rank
a✝² : IsHeapForest' u.rank y
a✝¹ : IsBinTree c
a✝ : r < c.rank
hf : IsHeapForest' c.rank z
h✝ : ((combine le u c).rank != hRank []) = true
⊢ IsHeapForest' (combine le u c).rank []
Tactic:
constructor
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 α)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝ : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)
Tactic:
rename_i neq
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬((combine le u c).rank != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬((combine le u c).rank != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ((combine le u c).rank != hRank (t :: ts)) = true
⊢ IsHeapForest' (combine le u c).rank (t :: ts)
Tactic:
rw[rank_combine heq, hrank_of_cons] at *
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (u.rank + 1 != t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (u.rank + 1 != t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
unfold bne at neq
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (!u.rank + 1 == t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : (!u.rank + 1 == t.rank) = true
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
rw[Nat.not_beq_eq_true_eq] at neq
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
Tactic:
have hle : c.rank + 1 ≤ t.rank := by
  apply Nat.succ_le_of_lt lt
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ u.rank + 1 < t.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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts