internlm/Lean-Github huggingface dataset:
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' h₁.rank (mergeNodes le t₁ (h₂ :: t₂))
Tactic:
rename_i hlt₂
Proof state after:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' h₁.rank (mergeNodes le t₁ (h₂ :: t₂))
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' h₁.rank (mergeNodes le t₁ (h₂ :: t₂))
Tactic:
have : h₁.rank = min h₁.rank (h₂.rank - 1) := by
  have hle : h₁.rank ≤ (h₂.rank - 1) := by
    apply Nat.le_pred_of_lt hlt₂
  have : min h₁.rank (h₂.rank - 1) = h₁.rank := by
    apply min_eq_left hle
  rw[this]
Proof state after:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
this : h₁.rank = min h₁.rank (h₂.rank - 1)
⊢ IsHeapForest' h₁.rank (mergeNodes le t₁ (h₂ :: t₂))
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
this : h₁.rank = min h₁.rank (h₂.rank - 1)
⊢ IsHeapForest' h₁.rank (mergeNodes le t₁ (h₂ :: t₂))
Tactic:
rw [this]
Proof state after:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
this : h₁.rank = min h₁.rank (h₂.rank - 1)
⊢ IsHeapForest' (min h₁.rank (h₂.rank - 1)) (mergeNodes le t₁ (h₂ :: t₂))
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
this : h₁.rank = min h₁.rank (h₂.rank - 1)
⊢ IsHeapForest' (min h₁.rank (h₂.rank - 1)) (mergeNodes le t₁ (h₂ :: t₂))
Tactic:
clear this
Proof state after:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (min h₁.rank (h₂.rank - 1)) (mergeNodes le t₁ (h₂ :: t₂))
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (min h₁.rank (h₂.rank - 1)) (mergeNodes le t₁ (h₂ :: t₂))
Tactic:
apply IsHeap_merge
Proof state after:
case inl.a.cons.hxs
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' h₁.rank t₁

case inl.a.cons.hys
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₂.rank - 1) (h₂ :: t₂)
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons.hxs
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' h₁.rank t₁

case inl.a.cons.hys
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₂.rank - 1) (h₂ :: t₂)
Tactic:
. assumption
Proof state after:
case inl.a.cons.hys
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₂.rank - 1) (h₂ :: t₂)
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons.hys
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₂.rank - 1) (h₂ :: t₂)
Tactic:
. apply IsHeapForest'_strengthen_pred
  . assumption
  . cases bt with | mk =>
      have hge : h₁.rank ≥ 0 := by
        cases h₁.rank
        . simp 
        . simp
      have hle : 0 ≤ h₁.rank := by
        apply hge
      have : 0 < h₂.rank := by
        apply lt_of_le_of_lt hle hlt₂
      assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ h₁.rank = min h₁.rank (h₂.rank - 1)
Tactic:
have hle : h₁.rank ≤ (h₂.rank - 1) := by
  apply Nat.le_pred_of_lt hlt₂
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
hle : h₁.rank ≤ h₂.rank - 1
⊢ h₁.rank = min h₁.rank (h₂.rank - 1)
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
hle : h₁.rank ≤ h₂.rank - 1
⊢ h₁.rank = min h₁.rank (h₂.rank - 1)
Tactic:
have : min h₁.rank (h₂.rank - 1) = h₁.rank := by
  apply min_eq_left hle
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
hle : h₁.rank ≤ h₂.rank - 1
this : min h₁.rank (h₂.rank - 1) = h₁.rank
⊢ h₁.rank = min h₁.rank (h₂.rank - 1)
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
hle : h₁.rank ≤ h₂.rank - 1
this : min h₁.rank (h₂.rank - 1) = h₁.rank
⊢ h₁.rank = min h₁.rank (h₂.rank - 1)
Tactic:
rw[this]
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ h₁.rank ≤ h₂.rank - 1
Tactic:
apply Nat.le_pred_of_lt hlt₂
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
hle : h₁.rank ≤ h₂.rank - 1
⊢ min h₁.rank (h₂.rank - 1) = h₁.rank
Tactic:
apply min_eq_left hle
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons.hys.hpos.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
⊢ h₂.rank > 0
Tactic:
have hge : h₁.rank ≥ 0 := by
  cases h₁.rank
  . simp 
  . simp
Proof state after:
case inl.a.cons.hys.hpos.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
⊢ h₂.rank > 0
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons.hys.hpos.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
⊢ h₂.rank > 0
Tactic:
have hle : 0 ≤ h₁.rank := by
  apply hge
Proof state after:
case inl.a.cons.hys.hpos.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
hle : 0 ≤ h₁.rank
⊢ h₂.rank > 0
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons.hys.hpos.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
hle : 0 ≤ h₁.rank
⊢ h₂.rank > 0
Tactic:
have : 0 < h₂.rank := by
  apply lt_of_le_of_lt hle hlt₂
Proof state after:
case inl.a.cons.hys.hpos.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
hle : 0 ≤ h₁.rank
this : 0 < h₂.rank
⊢ h₂.rank > 0
Theorem: project.IsHeap_merge
Proof state before:
case inl.a.cons.hys.hpos.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
hle : 0 ≤ h₁.rank
this : 0 < h₂.rank
⊢ h₂.rank > 0
Tactic:
assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
⊢ h₁.rank ≥ 0
Tactic:
cases h₁.rank
Proof state after:
case zero
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
⊢ Nat.zero ≥ 0

case succ
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
n✝ : ℕ
⊢ Nat.succ n✝ ≥ 0
Theorem: project.IsHeap_merge
Proof state before:
case zero
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
⊢ Nat.zero ≥ 0

case succ
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
n✝ : ℕ
⊢ Nat.succ n✝ ≥ 0
Tactic:
. simp
Proof state after:
case succ
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
n✝ : ℕ
⊢ Nat.succ n✝ ≥ 0
Theorem: project.IsHeap_merge
Proof state before:
case succ
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
n✝ : ℕ
⊢ Nat.succ n✝ ≥ 0
Tactic:
. simp
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
⊢ 0 ≤ h₁.rank
Tactic:
apply hge
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝ : IsRankedTree 1 h₁.rank (Heap.nodes h₁.children)
hge : h₁.rank ≥ 0
hle : 0 ≤ h₁.rank
⊢ 0 < h₂.rank
Tactic:
apply lt_of_le_of_lt hle hlt₂
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ min h₂.rank (h₁.rank - 1) = h₂.rank
Tactic:
have : h₂.rank ≤ (h₁.rank - 1) := by
  apply Nat.le_pred_of_lt
  assumption
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
this : h₂.rank ≤ h₁.rank - 1
⊢ min h₂.rank (h₁.rank - 1) = h₂.rank
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
this : h₂.rank ≤ h₁.rank - 1
⊢ min h₂.rank (h₁.rank - 1) = h₂.rank
Tactic:
apply min_eq_left
Proof state after:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
this : h₂.rank ≤ h₁.rank - 1
⊢ h₂.rank ≤ h₁.rank - 1
Theorem: project.IsHeap_merge
Proof state before:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
this : h₂.rank ≤ h₁.rank - 1
⊢ h₂.rank ≤ h₁.rank - 1
Tactic:
assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ h₂.rank ≤ h₁.rank - 1
Tactic:
apply Nat.le_pred_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
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ h₂.rank < h₁.rank
Theorem: project.IsHeap_merge
Proof state before:
case h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ h₂.rank < h₁.rank
Tactic:
assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inl.a.hys.a.cons.a.succ.h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
heq : min h₂.rank (h₁.rank - 1) = h₂.rank
a✝² : IsBinTree h₁
a✝¹ : IsHeapForest' h₁.rank t₁
n✝ : ℕ
a✝ : Nat.succ n✝ < h₁.rank
⊢ ?inr.inl.a.hys.a.cons.a.succ.b < h₁.rank

case inr.inl.a.hys.a.cons.a.succ.b
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
heq : min h₂.rank (h₁.rank - 1) = h₂.rank
a✝² : IsBinTree h₁
a✝¹ : IsHeapForest' h₁.rank t₁
n✝ : ℕ
a✝ : Nat.succ n✝ < h₁.rank
⊢ ℕ
Tactic:
assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
hneq : ((combine le h₁ h₂).rank != hRank t₁) = true
hneq₂ : ((combine le h₁ h₂).rank != hRank t₂) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝¹ : h₂.rank ≤ h₁.rank
h✝ : h₁.rank ≤ h₂.rank
⊢ h₁.rank = h₂.rank
Tactic:
apply Nat.le_antisymm <;> assumption
Proof state after:
no goals