theorem Std.HashSet.mem_union_iff {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {a : α} (m₁ m₂ : HashSet α) : a ∈ m₁.union m₂ ↔ a ∈ m₁ ∨ a ∈ m₂