internlm/Lean-Github huggingface dataset:
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inr.hxs.a.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
lt : rx < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ rx < h₁.rank + 1
Tactic:
have : h₁.rank < h₁.rank + 1 := by
  apply Nat.lt_succ_self
Proof state after:
case inr.inr.inl.inr.hxs.a.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
lt : rx < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
this : h₁.rank < h₁.rank + 1
⊢ rx < h₁.rank + 1
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inr.hxs.a.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
lt : rx < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
this : h₁.rank < h₁.rank + 1
⊢ rx < h₁.rank + 1
Tactic:
apply lt_trans lt this
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 α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
lt : rx < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ h₁.rank < h₁.rank + 1
Tactic:
apply Nat.lt_succ_self
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₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
Tactic:
have : (combine le h₁ h₂).rank = h₁.rank + 1 := by
  apply rank_combine heq
Proof state after:
α : 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₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
this : (combine le h₁ h₂).rank = h₁.rank + 1
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
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₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
this : (combine le h₁ h₂).rank = h₁.rank + 1
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
Tactic:
simp only [this] at *
Proof state after:
α : 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₂)
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
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₁) = true
h✝ : (h₁.rank + 1 != hRank t₂) = false
this : True
⊢ IsHeapForest' (h₁.rank + 1) t₁
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₂)
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
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₁) = true
h✝ : (h₁.rank + 1 != hRank t₂) = false
this : True
⊢ IsHeapForest' (h₁.rank + 1) t₁
Tactic:
clear this
Proof state after:
α : 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₂)
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
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₁) = true
h✝ : (h₁.rank + 1 != hRank t₂) = false
⊢ IsHeapForest' (h₁.rank + 1) t₁
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₂)
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
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₁) = true
h✝ : (h₁.rank + 1 != hRank t₂) = false
⊢ IsHeapForest' (h₁.rank + 1) t₁
Tactic:
match hf with
| .nil =>
  constructor
| .cons (t := t) (ts := ts) lt _ _ =>
  constructor
  . have : h₁.rank + 1 ≤ t.rank := by
      apply Nat.succ_le_of_lt lt
    apply lt_of_le_of_ne this
    rw[hrank_of_cons] at *
    unfold bne at *
    rw[Nat.not_beq_eq_true_eq] at *
    assumption
  . assumption
  . 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₂)
h✝³ : ((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✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
⊢ (combine le h₁ h₂).rank = h₁.rank + 1
Tactic:
apply rank_combine heq
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 α)
hys : IsHeapForest' ry (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
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
hxs : IsHeapForest' rx [h₁]
h✝ : (h₁.rank + 1 != hRank []) = true
⊢ IsHeapForest' (h₁.rank + 1) []
Tactic:
constructor
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 α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' (h₁.rank + 1) (t :: ts)
Tactic:
constructor
Proof state after:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ h₁.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
Theorem: project.IsHeap_merge
Proof state before:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
Tactic:
. assumption
Proof state after:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
Theorem: project.IsHeap_merge
Proof state before:
case a
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ IsHeapForest' t.rank ts
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 α)
hys : IsHeapForest' ry (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
a✝³ : rx < h₁.rank
a✝² : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₂) = false
t : BinTree α
ts : List (BinTree α)
lt : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
hxs : IsHeapForest' rx (h₁ :: t :: ts)
h✝ : (h₁.rank + 1 != hRank (t :: ts)) = true
⊢ h₁.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inr.hys.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 α)
hxs : IsHeapForest' rx (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
a✝ : IsBinTree h₂
lt : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' ry t₂
Tactic:
have : ry ≤ h₂.rank := by
    apply le_of_lt lt
Proof state after:
case inr.inr.inl.inr.hys.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 α)
hxs : IsHeapForest' rx (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
a✝ : IsBinTree h₂
lt : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
this : ry ≤ h₂.rank
⊢ IsHeapForest' ry t₂
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inr.hys.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 α)
hxs : IsHeapForest' rx (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
a✝ : IsBinTree h₂
lt : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
this : ry ≤ h₂.rank
⊢ IsHeapForest' ry t₂
Tactic:
apply IsHeapForest'_weaken hf 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 α)
hxs : IsHeapForest' rx (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
a✝ : IsBinTree h₂
lt : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
⊢ ry ≤ h₂.rank
Tactic:
apply le_of_lt lt
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inl.hxs.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
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝ : IsBinTree h₁
lt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' rx t₁
Tactic:
have : rx ≤ h₁.rank := by
    apply le_of_lt lt
Proof state after:
case inr.inr.inr.inl.hxs.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
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝ : IsBinTree h₁
lt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
this : rx ≤ h₁.rank
⊢ IsHeapForest' rx t₁
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inl.hxs.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
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝ : IsBinTree h₁
lt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
this : rx ≤ h₁.rank
⊢ IsHeapForest' rx t₁
Tactic:
apply IsHeapForest'_weaken hf 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₂)
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
a✝ : IsBinTree h₁
lt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ rx ≤ h₁.rank
Tactic:
apply le_of_lt lt
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₂)
h✝³ : ((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✝ : ((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.IsHeap_merge
Proof state before:
case inr.inr.inr.inl.hys.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
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝² : IsBinTree h₁
a✝¹ : rx < h₁.rank
a✝ : IsHeapForest' h₁.rank t₁
⊢ IsBinTree (combine le h₁ h₂)
Tactic:
cases hys with | cons =>
  simp at *
  have : h₁.rank = h₂.rank := by
    apply Nat.le_antisymm <;> assumption
  apply combine_IsBinTree <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inl.hys.a.cons.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 α)
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
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsBinTree (combine le h₁ h₂)
Tactic:
simp at *
Proof state after:
case inr.inr.inr.inl.hys.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank 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
⊢ IsBinTree (combine le h₁ h₂)
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inl.hys.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank 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
⊢ IsBinTree (combine le h₁ h₂)
Tactic:
have : h₁.rank = h₂.rank := by
  apply Nat.le_antisymm <;> assumption
Proof state after:
case inr.inr.inr.inl.hys.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank 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
this : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inl.hys.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank 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
this : h₁.rank = h₂.rank
⊢ IsBinTree (combine le h₁ h₂)
Tactic:
apply combine_IsBinTree <;> assumption
Proof state after:
no goals