mathlib

289df3a7 - feat(data/set/lattice): add lemmas set.Union_subtype and set.Union_of_singleton_coe (#5691)

feat(data/set/lattice): add lemmas set.Union_subtype and set.Union_of_singleton_coe (#5691) Add one simp lemma, following a suggestion on the Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/image_bUnion