internlm/Lean-Github huggingface dataset:
Theorem: project.IsHeapForest'_of_IsRankedTree
Proof state before:
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsHeapForest' (r - 1) (t :: ts)
Tactic:
constructor
Proof state after:
case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ r - 1 < t.rank

case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsBinTree t

case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsHeapForest' t.rank ts
Theorem: project.IsHeapForest'_of_IsRankedTree
Proof state before:
case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ r - 1 < t.rank

case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsBinTree t

case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsHeapForest' t.rank ts
Tactic:
. rw[←eq]
  apply Nat.pred_lt
  simp
  rw[eq]
  assumption
Proof state after:
case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsBinTree t

case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsHeapForest' t.rank ts
Theorem: project.IsHeapForest'_of_IsRankedTree
Proof state before:
case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsBinTree t

case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsHeapForest' t.rank ts
Tactic:
. assumption
Proof state after:
case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsHeapForest' t.rank ts
Theorem: project.IsHeapForest'_of_IsRankedTree
Proof state before:
case a
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ IsHeapForest' t.rank ts
Tactic:
. have : t.rank = (r + 1) - 1 := by
    simp_all
  rw[this]
  apply IsHeapForest'_of_IsRankedTree
  . simp
  . assumption
Proof state after:
no goals
Theorem: project.IsHeapForest'_of_IsRankedTree
Proof state before:
α : Sort ?u.894
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r s✝ : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
s : ℕ
ts : List (BinTree α✝)
t : BinTree α✝
eq : t.rank = r
rt : IsRankedTree (r + 1) s ts
a✝ : IsBinTree t
⊢ t.rank = r + 1 - 1
Tactic:
simp_all
Proof state after:
no goals
Theorem: project.children_IsHeap
Proof state before:
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
h : HeapNodeAux α✝ (Heap α✝)
⊢ IsHeap (Heap.heap [h]) → IsHeap h.children
Tactic:
intro h₁
Proof state after:
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
h : HeapNodeAux α✝ (Heap α✝)
h₁ : IsHeap (Heap.heap [h])
⊢ IsHeap h.children
Theorem: project.children_IsHeap
Proof state before:
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
h : HeapNodeAux α✝ (Heap α✝)
h₁ : IsHeap (Heap.heap [h])
⊢ IsHeap h.children
Tactic:
cases h with | mk val rank children =>
dsimp at *
cases h₁ with | cons lt bt h₁ =>
dsimp at *
cases children with | heap nodes =>
dsimp at *
cases bt with | mk rt =>
dsimp at rt
apply IsHeapForest'_of_IsRankedTree (r := 1)
. simp
. assumption
Proof state after:
no goals
Theorem: project.children_IsHeap
Proof state before:
case mk
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
children : Heap α✝
h₁ : IsHeap (Heap.heap [{ val := val, rank := rank, children := children }])
⊢ IsHeap { val := val, rank := rank, children := children }.children
Tactic:
dsimp at *
Proof state after:
case mk
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
children : Heap α✝
h₁ : IsHeap (Heap.heap [{ val := val, rank := rank, children := children }])
⊢ IsHeap children
Theorem: project.children_IsHeap
Proof state before:
case mk
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
children : Heap α✝
h₁ : IsHeap (Heap.heap [{ val := val, rank := rank, children := children }])
⊢ IsHeap children
Tactic:
cases h₁ with | cons lt bt h₁ =>
dsimp at *
cases children with | heap nodes =>
dsimp at *
cases bt with | mk rt =>
dsimp at rt
apply IsHeapForest'_of_IsRankedTree (r := 1)
. simp
. assumption
Proof state after:
no goals
Theorem: project.children_IsHeap
Proof state before:
case mk.cons
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
children : Heap α✝
bt : IsBinTree { val := val, rank := rank, children := children }
lt : 0 < { val := val, rank := rank, children := children }.rank
h₁ : IsHeapForest' { val := val, rank := rank, children := children }.rank []
⊢ IsHeap children
Tactic:
dsimp at *
Proof state after:
case mk.cons
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
children : Heap α✝
bt : IsBinTree { val := val, rank := rank, children := children }
lt : 0 < rank
h₁ : IsHeapForest' rank []
⊢ IsHeap children
Theorem: project.children_IsHeap
Proof state before:
case mk.cons
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
children : Heap α✝
bt : IsBinTree { val := val, rank := rank, children := children }
lt : 0 < rank
h₁ : IsHeapForest' rank []
⊢ IsHeap children
Tactic:
cases children with | heap nodes =>
dsimp at *
cases bt with | mk rt =>
dsimp at rt
apply IsHeapForest'_of_IsRankedTree (r := 1)
. simp
. assumption
Proof state after:
no goals
Theorem: project.children_IsHeap
Proof state before:
case mk.cons.heap
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
bt : IsBinTree { val := val, rank := rank, children := Heap.heap nodes }
⊢ IsHeap (Heap.heap nodes)
Tactic:
cases bt with | mk rt =>
dsimp at rt
apply IsHeapForest'_of_IsRankedTree (r := 1)
. simp
. assumption
Proof state after:
no goals
Theorem: project.children_IsHeap
Proof state before:
case mk.cons.heap.mk
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt :
  IsRankedTree 1 { val := val, rank := rank, children := Heap.heap nodes }.rank
    (Heap.nodes { val := val, rank := rank, children := Heap.heap nodes }.children)
⊢ IsHeap (Heap.heap nodes)
Tactic:
dsimp at rt
Proof state after:
case mk.cons.heap.mk
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ IsHeap (Heap.heap nodes)
Theorem: project.children_IsHeap
Proof state before:
case mk.cons.heap.mk
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ IsHeap (Heap.heap nodes)
Tactic:
apply IsHeapForest'_of_IsRankedTree (r := 1)
Proof state after:
case mk.cons.heap.mk.h₁
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ 1 ≠ 0

case mk.cons.heap.mk.a
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ IsRankedTree 1 ?m.30690 (Heap.nodes (Heap.heap nodes))

α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ ℕ
Theorem: project.children_IsHeap
Proof state before:
case mk.cons.heap.mk.h₁
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ 1 ≠ 0

case mk.cons.heap.mk.a
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ IsRankedTree 1 ?m.30690 (Heap.nodes (Heap.heap nodes))

α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ ℕ
Tactic:
. simp
Proof state after:
case mk.cons.heap.mk.a
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ IsRankedTree 1 ?m.30690 (Heap.nodes (Heap.heap nodes))

α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ ℕ
Theorem: project.children_IsHeap
Proof state before:
case mk.cons.heap.mk.a
α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ IsRankedTree 1 ?m.30690 (Heap.nodes (Heap.heap nodes))

α : Sort ?u.30046
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
val : α✝
rank : ℕ
lt : 0 < rank
h₁ : IsHeapForest' rank []
nodes : List (HeapNodeAux α✝ (Heap α✝))
rt : IsRankedTree 1 rank nodes
⊢ ℕ
Tactic:
. assumption
Proof state after:
no goals
Theorem: project.IsMinHeap_of_IsMinTree
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes : List (BinTree α)
⊢ IsMinHeap le (Heap.heap [])
Tactic:
constructor
Proof state after:
no goals
Theorem: project.IsMinHeap_of_IsMinTree
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes ts✝ : List (BinTree α)
t✝ : BinTree α
a✝² : le val t✝.val = true
a✝¹ : IsMinTree le val ts✝
a✝ : IsSearchTree le t✝
⊢ IsMinHeap le (Heap.heap (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
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes ts✝ : List (BinTree α)
t✝ : BinTree α
a✝² : le val t✝.val = true
a✝¹ : IsMinTree le val ts✝
a✝ : IsSearchTree le t✝
⊢ IsSearchTree le t✝

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes ts✝ : List (BinTree α)
t✝ : BinTree α
a✝² : le val t✝.val = true
a✝¹ : IsMinTree le val ts✝
a✝ : IsSearchTree le t✝
⊢ IsMinHeap le (Heap.heap ts✝)
Theorem: project.IsMinHeap_of_IsMinTree
Proof state before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes ts✝ : List (BinTree α)
t✝ : BinTree α
a✝² : le val t✝.val = true
a✝¹ : IsMinTree le val ts✝
a✝ : IsSearchTree le t✝
⊢ IsSearchTree le t✝

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes ts✝ : List (BinTree α)
t✝ : BinTree α
a✝² : le val t✝.val = true
a✝¹ : IsMinTree le val ts✝
a✝ : IsSearchTree le t✝
⊢ IsMinHeap le (Heap.heap 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
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes ts✝ : List (BinTree α)
t✝ : BinTree α
a✝² : le val t✝.val = true
a✝¹ : IsMinTree le val ts✝
a✝ : IsSearchTree le t✝
⊢ IsMinHeap le (Heap.heap ts✝)
Theorem: project.IsMinHeap_of_IsMinTree
Proof state before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
nodes ts✝ : List (BinTree α)
t✝ : BinTree α
a✝² : le val t✝.val = true
a✝¹ : IsMinTree le val ts✝
a✝ : IsSearchTree le t✝
⊢ IsMinHeap le (Heap.heap ts✝)
Tactic:
. apply IsMinHeap_of_IsMinTree
  . assumption
Proof state after:
no goals
Theorem: project.children_IsMinHeap
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
⊢ IsMinHeap le (Heap.heap [h]) → IsMinHeap le h.children
Tactic:
intro imh
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
imh : IsMinHeap le (Heap.heap [h])
⊢ IsMinHeap le h.children
Theorem: project.children_IsMinHeap
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
h : HeapNodeAux α (Heap α)
imh : IsMinHeap le (Heap.heap [h])
⊢ IsMinHeap le h.children
Tactic:
cases h with | mk val rank children =>
dsimp at *
cases imh with | cons st imh =>
cases children with | heap nodes =>
cases imh with | nil =>
cases st with | mk mt =>
dsimp at mt
apply IsMinHeap_of_IsMinTree
repeat assumption
Proof state after:
no goals
Theorem: project.children_IsMinHeap
Proof state before:
case mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
children : Heap α
imh : IsMinHeap le (Heap.heap [{ val := val, rank := rank, children := children }])
⊢ IsMinHeap le { val := val, rank := rank, children := children }.children
Tactic:
dsimp at *
Proof state after:
case mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
children : Heap α
imh : IsMinHeap le (Heap.heap [{ val := val, rank := rank, children := children }])
⊢ IsMinHeap le children
Theorem: project.children_IsMinHeap
Proof state before:
case mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
children : Heap α
imh : IsMinHeap le (Heap.heap [{ val := val, rank := rank, children := children }])
⊢ IsMinHeap le children
Tactic:
cases imh with | cons st imh =>
cases children with | heap nodes =>
cases imh with | nil =>
cases st with | mk mt =>
dsimp at mt
apply IsMinHeap_of_IsMinTree
repeat assumption
Proof state after:
no goals
Theorem: project.children_IsMinHeap
Proof state before:
case mk.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
children : Heap α
st : IsSearchTree le { val := val, rank := rank, children := children }
imh : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le children
Tactic:
cases children with | heap nodes =>
cases imh with | nil =>
cases st with | mk mt =>
dsimp at mt
apply IsMinHeap_of_IsMinTree
repeat assumption
Proof state after:
no goals
Theorem: project.children_IsMinHeap
Proof state before:
case mk.cons.heap
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
imh : IsMinHeap le (Heap.heap [])
nodes : List (HeapNodeAux α (Heap α))
st : IsSearchTree le { val := val, rank := rank, children := Heap.heap nodes }
⊢ IsMinHeap le (Heap.heap nodes)
Tactic:
cases imh with | nil =>
cases st with | mk mt =>
dsimp at mt
apply IsMinHeap_of_IsMinTree
repeat assumption
Proof state after:
no goals
Theorem: project.children_IsMinHeap
Proof state before:
case mk.cons.heap.nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
st : IsSearchTree le { val := val, rank := rank, children := Heap.heap nodes }
⊢ IsMinHeap le (Heap.heap nodes)
Tactic:
cases st with | mk mt =>
dsimp at mt
apply IsMinHeap_of_IsMinTree
repeat assumption
Proof state after:
no goals