rw [Multiset.elems]
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = elems (BTree.node a l r)
case node
a : ℕ
l r : BTree ℕ
ih_l : elems (mirror l) = elems l
ih_r : elems (mirror r) = elems r
⊢ elems (mirror (BTree.node a l r)) = {a} ∪ elems l ∪ elems r