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