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

State before:
α : Type
t : BTree α
ht : IsFull t
⊢ IsFull (mirror t)
Tactic:
induction ht with
| empty                           => exact IsFull.empty
| node a l r hl hr hiff ih_l ih_r =>
  { rw [mirror]
    apply IsFull.node
    { exact ih_r }
    { exact ih_l }
    { simp [mirror_Eq_empty_Iff, *] } }
State after:
no goals

State before:
case empty
α : Type
t : BTree α
⊢ IsFull (mirror BTree.empty)
Tactic:
exact IsFull.empty
State after:
no goals

State before:
case node
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror (BTree.node a l r))
Tactic:
rw [mirror]
State after:
case node
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (BTree.node a (mirror r) (mirror l))

State before:
case node
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (BTree.node a (mirror r) (mirror l))
Tactic:
apply IsFull.node
State after:
case node.hl
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror r)

case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty

State before:
case node.hl
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror r)

case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ exact ih_r }
State after:
case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty

State before:
case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)

case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ exact ih_l }
State after:
case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty

State before:
case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
{ simp [mirror_Eq_empty_Iff, *] }
State after:
no goals

State before:
case node.hl
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror r)
Tactic:
exact ih_r
State after:
no goals

State before:
case node.hr
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror l)
Tactic:
exact ih_l
State after:
no goals

State before:
case node.hiff
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
Tactic:
simp [mirror_Eq_empty_Iff, *]
State after:
no goals