Theorem: LoVe.Multiset.elems_mirror (LoVe/Labs/Lab7Solution.lean)

State before:
t : BTree ℕ
⊢ elems (mirror t) = elems t
Tactic:
induction t with
| empty =>
  rfl
| node a l r ih_l ih_r =>
  rw [Multiset.elems]
  rw [mirror]
  rw [←ih_l]
  rw [←ih_r]
  rw [Multiset.elems]
  rw [Multiset.union_assoc,
      Multiset.union_comm (elems (mirror r)),
      ←Multiset.union_assoc]
State after:
no goals

State before:
case empty

⊢ elems (mirror BTree.empty) = elems BTree.empty
Tactic:
rfl
State after:
no goals

State before:
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)
Tactic:
rw [Multiset.elems]
State after:
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

State before:
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
Tactic:
rw [mirror]
State after:
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 l ∪ elems r

State before:
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 l ∪ elems r
Tactic:
rw [←ih_l]
State after:
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 r

State before:
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 r
Tactic:
rw [←ih_r]
State after:
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)

State before:
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)
Tactic:
rw [Multiset.elems]
State after:
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)

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