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

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

State before:
α : Type
a : α
l r : BTree α
⊢ mirror (mirror (BTree.node a l r)) = mirror (BTree.node a (mirror r) (mirror l))
Tactic:
rfl
State after:
no goals

State before:
α : Type
a : α
l r : BTree α
⊢ mirror (BTree.node a (mirror r) (mirror l)) = BTree.node a (mirror (mirror l)) (mirror (mirror r))
Tactic:
rfl
State after:
no goals

State before:
α : Type
a : α
l r : BTree α
⊢ BTree.node a (mirror (mirror l)) (mirror (mirror r)) = BTree.node a l (mirror (mirror r))
Tactic:
rw [mirror_mirror_calc l]
State after:
no goals

State before:
α : Type
a : α
l r : BTree α
⊢ BTree.node a l (mirror (mirror r)) = BTree.node a l r
Tactic:
rw [mirror_mirror_calc r]
State after:
no goals