mathlib3

45501380 - feat(data/set): add lemmas about `powerset` of `insert` and `singleton` (#18356)

feat(data/set): add lemmas about `powerset` of `insert` and `singleton` (#18356) Add lemmas about `𝒫 {x}` and `𝒫 (insert x A)`. Mathlib4 pair : leanprover-community/mathlib4/pull/2000 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>