Theorem: LoVe.BTree.map_mirror (LoVe/Labs/Lab5Solution.lean)

State before:
α β : Type
f : α → β
⊢ ∀ (t : BTree α), IsFull t → IsFull (map f t)
Tactic:
intro t hfull
State after:
α β : Type
f : α → β
t : BTree α
hfull : IsFull t
⊢ IsFull (map f t)

State before:
α β : Type
f : α → β
t : BTree α
hfull : IsFull t
⊢ IsFull (map f t)
Tactic:
induction hfull with
| empty =>
  simp [BTree.map]
  exact IsFull.empty
| node a l r hl hr hiff ihl ihr =>
  simp [BTree.map]
  apply IsFull.node
  { exact ihl }
  { exact ihr }
  { simp [BTree.map_eq_empty_iff]
    assumption }
State after:
no goals

State before:
case empty
α β : Type
f : α → β
t : BTree α
⊢ IsFull (map f empty)
Tactic:
simp [BTree.map]
State after:
case empty
α β : Type
f : α → β
t : BTree α
⊢ IsFull empty

State before:
case empty
α β : Type
f : α → β
t : BTree α
⊢ IsFull empty
Tactic:
exact IsFull.empty
State after:
no goals

State before:
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f (node a l r))
Tactic:
simp [BTree.map]
State after:
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (node (f a) (map f l) (map f r))

State before:
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (node (f a) (map f l) (map f r))
Tactic:
apply IsFull.node
State after:
case node.hl
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f l)

case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty

State before:
case node.hl
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f l)

case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
{ exact ihl }
State after:
case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty

State before:
case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
{ exact ihr }
State after:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty

State before:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
{ simp [BTree.map_eq_empty_iff]
  assumption }
State after:
no goals

State before:
case node.hl
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f l)
Tactic:
exact ihl
State after:
no goals

State before:
case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)
Tactic:
exact ihr
State after:
no goals

State before:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
simp [BTree.map_eq_empty_iff]
State after:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ l = empty ↔ r = empty

State before:
case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ l = empty ↔ r = empty
Tactic:
assumption
State after:
no goals