internlm/Lean-Github huggingface dataset:
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 y
Tactic:
. cases ht₁ with | cons _ _ hf =>
    cases ht₂ with | cons =>
      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 : u.rank + 1 ≤ t.rank := by
          apply Nat.succ_le_of_lt lt
        constructor
        . 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 (c :: z)
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 u
lt : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ 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
hf : IsHeapForest' u.rank y
⊢ IsHeapForest' (combine le u c).rank y
Tactic:
cases ht₂ with | cons =>
  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 : u.rank + 1 ≤ t.rank := by
      apply Nat.succ_le_of_lt lt
    constructor
    . 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
hf : IsHeapForest' u.rank y
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : IsHeapForest' c.rank z
⊢ IsHeapForest' (combine le u c).rank y
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 : u.rank + 1 ≤ t.rank := by
    apply Nat.succ_le_of_lt lt
  constructor
  . 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 z) = true
a✝⁴ : IsBinTree u
a✝³ : r < u.rank
hf : IsHeapForest' u.rank y
a✝² : IsBinTree c
a✝¹ : r < c.rank
a✝ : 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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.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 : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : 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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. apply lt_of_le_of_ne <;> 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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.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 z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. 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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
this : u.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank z) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
hf : IsHeapForest' u.rank y
a✝⁴ : IsBinTree c
a✝³ : r < c.rank
a✝² : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : u.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ u.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
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)
⊢ IsHeapForest' r z
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 : ℕ
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
⊢ IsHeapForest' r z
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case 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✝¹ : ((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
⊢ IsHeapForest' r z
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 : ℕ
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
⊢ IsHeapForest' ?cons.n z

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 ≤ ?cons.n

case cons.n
α : 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
⊢ ℕ
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
⊢ IsHeapForest' ?cons.n z

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 ≤ ?cons.n

case cons.n
α : 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
⊢ ℕ
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 : ℕ
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