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

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