Theorem: LoVe.Set.empty_union (LoVe/LoVelib.lean)

State before:
α : Type
A : Set α
⊢ ∅ ∪ A = A
Tactic:
simp [Union.union, Set.union]
State after:
no goals