Theorem: project.children_IsHeap (Project/DeleteMin.lean)

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₁
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

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
State after:
no goals

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 *
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

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
State after:
no goals

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 *
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

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
State after:
no goals

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
State after:
no goals

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
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)

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)
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
⊢ ℕ

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
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
⊢ ℕ

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
State after:
no goals