Theorem: LoVe.mirror_IsFull (LoVe/Labs/Lab5Solution.lean)

State before:
α : Type
⊢ ∀ (t : BTree α), IsFull (mirror t) → IsFull t
Tactic:
intro t fmt
State after:
α : Type
t : BTree α
fmt : IsFull (mirror t)
⊢ IsFull t

State before:
α : Type
t : BTree α
fmt : IsFull (mirror t)
⊢ IsFull t
Tactic:
have fmmt : IsFull (mirror (mirror t)) :=
  IsFull_mirror _ fmt
State after:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull (mirror (mirror t))
⊢ IsFull t

State before:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull (mirror (mirror t))
⊢ IsFull t
Tactic:
rw [mirror_mirror] at fmmt
State after:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull t
⊢ IsFull t

State before:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull t
⊢ IsFull t
Tactic:
assumption
State after:
no goals