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

State before:
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeap (singleton a)
Tactic:
constructor
State after:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ 0 < { val := a, rank := 1, children := heap [] }.rank

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []

State before:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ 0 < { val := a, rank := 1, children := heap [] }.rank

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Tactic:
. dsimp
  decide
State after:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []

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

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Tactic:
. constructor
  dsimp
  constructor
State after:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []

State before:
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []
Tactic:
. constructor
State after:
no goals