Theorem: LoVe.IsFull_singleton (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
α : Type
a : α
⊢ IsFull (BTree.node a BTree.empty BTree.empty)
Tactic:
apply IsFull.node
State after:
case hl
α : Type
a : α
⊢ IsFull BTree.empty

case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty

State before:
case hl
α : Type
a : α
⊢ IsFull BTree.empty

case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
{ exact IsFull.empty }
State after:
case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty

State before:
case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
{ exact IsFull.empty }
State after:
case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty

State before:
case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
{ rfl }
State after:
no goals

State before:
case hl
α : Type
a : α
⊢ IsFull BTree.empty
Tactic:
exact IsFull.empty
State after:
no goals

State before:
case hr
α : Type
a : α
⊢ IsFull BTree.empty
Tactic:
exact IsFull.empty
State after:
no goals

State before:
case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
rfl
State after:
no goals