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

State before:
α : Type
a : α
A B : Set α
⊢ a ∈ A ∪ B ↔ a ∈ A ∨ a ∈ B
Tactic:
rfl
State after:
no goals