Theorem: LoVe.mirror_mirror (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
α : Type
t : BTree α
⊢ mirror (mirror t) = t
Tactic:
induction t with
| empty                => rfl
| node a l r ih_l ih_r => simp [mirror, ih_l, ih_r]
State after:
no goals

State before:
case empty
α : Type
⊢ mirror (mirror BTree.empty) = BTree.empty
Tactic:
rfl
State after:
no goals

State before:
case node
α : Type
a : α
l r : BTree α
ih_l : mirror (mirror l) = l
ih_r : mirror (mirror r) = r
⊢ mirror (mirror (BTree.node a l r)) = BTree.node a l r
Tactic:
simp [mirror, ih_l, ih_r]
State after:
no goals