Theorem: project.singleton_IsMinHeap (Project/Main.lean)

State before:
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (singleton a)
Tactic:
constructor
State after:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsSearchTree le { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])

State before:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsSearchTree le { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])
Tactic:
. constructor
  dsimp
  constructor
State after:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])

State before:
case a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
a : α✝
⊢ IsMinHeap le (heap [])
Tactic:
. constructor
State after:
no goals