rw [Multiset.union_assoc,
    Multiset.union_comm (elems (mirror r)),
    ←Multiset.union_assoc]
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)
no goals