feat: forward-port leanprover-community/mathlib#18356 (#2000)

This is the corresponding forward porting PR to leanprover-community/mathlib#18356 and leanprover-community/mathlib#18491



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Set/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 
 ! This file was ported from Lean 3 source module data.set.basic
-! leanprover-community/mathlib commit b875cbb7f2aa2b4c685aaa2f99705689c95322ad
+! leanprover-community/mathlib commit 75608affb24b4f48699fbcd38f227827f7793771
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1154,6 +1154,10 @@ theorem insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔
   exacts[(ha hx).elim, hxt]
 #align set.insert_subset_insert_iff Set.insert_subset_insert_iff
 
+theorem subset_insert_iff_of_not_mem (ha : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t :=
+  forall₂_congr <| fun _ hb => or_iff_right <| ne_of_mem_of_not_mem hb ha
+#align set.subset_insert_iff_of_not_mem Set.subset_insert_iff_of_not_mem
+
 theorem ssubset_iff_insert {s t : Set α} : s ⊂ t ↔ ∃ (a : α) (_ : a ∉ s), insert a s ⊆ t := by
   simp only [insert_subset, exists_and_right, ssubset_def, not_subset]
   simp only [exists_prop, and_comm]
@@ -2125,6 +2129,12 @@ theorem powerset_univ : 𝒫(univ : Set α) = univ :=
   eq_univ_of_forall subset_univ
 #align set.powerset_univ Set.powerset_univ
 
+/-- The powerset of a singleton contains only `∅` and the singleton itself. -/
+theorem powerset_singleton (x : α) : 𝒫({x} : Set α) = {∅, {x}} := by
+  ext y
+  rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff]
+#align set.powerset_singleton Set.powerset_singleton
+
 /-! ### Sets defined as an if-then-else -/
 
 --Porting note: New theorem to prove `mem_dite` lemmas.

Mathlib/Data/Set/Image.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Ported by: Winston Yin
 
 ! This file was ported from Lean 3 source module data.set.image
-! leanprover-community/mathlib commit 2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e
+! leanprover-community/mathlib commit 4550138052d0a416b700c27056d492e2ef53214e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -610,6 +610,27 @@ theorem image_perm {s : Set α} {σ : Equiv.Perm α} (hs : { a : α | σ a ≠ a
 
 end Image
 
+/-! ### Lemmas about the powerset and image. -/
+
+/-- The powerset of `{a} ∪ s` is `𝒫 s` together with `{a} ∪ t` for each `t ∈ 𝒫 s`. -/
+theorem powerset_insert (s : Set α) (a : α) : 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s := by
+  ext t
+  simp_rw [mem_union, mem_image, mem_powerset_iff]
+  constructor
+  · intro h
+    by_cases hs : a ∈ t
+    · right
+      refine' ⟨t \ {a}, _, _⟩
+      · rw [diff_singleton_subset_iff]
+        assumption
+      · rw [insert_diff_singleton, insert_eq_of_mem hs]
+    · left
+      exact (subset_insert_iff_of_not_mem hs).mp h
+  · rintro (h | ⟨s', h₁, rfl⟩)
+    · exact subset_trans h (subset_insert a s)
+    · exact insert_subset_insert h₁
+#align set.powerset_insert Set.powerset_insert
+
 /-! ### Lemmas about range of a function. -/