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

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

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

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

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

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

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

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

State before:
case mk.cons.heap.nil.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 : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt :
  IsMinTree le { val := val, rank := rank, children := Heap.heap nodes }.val
    (Heap.nodes { val := val, rank := rank, children := Heap.heap nodes }.children)
⊢ IsMinHeap le (Heap.heap nodes)
Tactic:
dsimp at mt
State after:
case mk.cons.heap.nil.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 : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinHeap le (Heap.heap nodes)

State before:
case mk.cons.heap.nil.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 : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinHeap le (Heap.heap nodes)
Tactic:
apply IsMinHeap_of_IsMinTree
State after:
case mk.cons.heap.nil.mk.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 : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinTree le ?mk.cons.heap.nil.mk.val nodes

case mk.cons.heap.nil.mk.val
α : 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 α))
mt : IsMinTree le val nodes
⊢ α

State before:
case mk.cons.heap.nil.mk.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 : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinTree le ?mk.cons.heap.nil.mk.val nodes

case mk.cons.heap.nil.mk.val
α : 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 α))
mt : IsMinTree le val nodes
⊢ α
Tactic:
repeat assumption
State after:
no goals

State before:
case mk.cons.heap.nil.mk.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 : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinTree le ?mk.cons.heap.nil.mk.val nodes

case mk.cons.heap.nil.mk.val
α : 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 α))
mt : IsMinTree le val nodes
⊢ α
Tactic:
assumption
State after:
no goals