From 4550138052d0a416b700c27056d492e2ef53214e Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 22 Feb 2023 15:42:26 +0000
Subject: [PATCH] feat(data/set): add lemmas about `powerset` of `insert` and
 `singleton` (#18356)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add lemmas about `𝒫 {x}` and `𝒫 (insert x A)`.

Mathlib4 pair : leanprover-community/mathlib4/pull/2000



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/data/set/basic.lean | 20 ++++++++++++++++++++
 src/data/set/image.lean | 23 +++++++++++++++++++++++
 2 files changed, 43 insertions(+)

diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 661e500e3b9cf..729ea6cb1e1db 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -698,6 +698,22 @@ begin
   exacts [(ha hx).elim, hxt]
 end
 
+theorem subset_insert_iff_of_not_mem {s t : set α} {a : α} (h : a ∉ s) :
+  s ⊆ insert a t ↔ s ⊆ t :=
+begin
+  constructor,
+  { intros g y hy,
+    specialize g hy,
+    rw [mem_insert_iff] at g,
+    rcases g with g | g,
+    { rw [g] at hy,
+      contradiction },
+    { assumption }},
+  { intros g y hy,
+    specialize g hy,
+    exact mem_insert_of_mem _ g }
+end
+
 theorem ssubset_iff_insert {s t : set α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t :=
 begin
   simp only [insert_subset, exists_and_distrib_right, ssubset_def, not_subset],
@@ -1301,6 +1317,10 @@ ext $ λ s, subset_empty_iff
 @[simp] theorem powerset_univ : 𝒫 (univ : set α) = univ :=
 eq_univ_of_forall subset_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] }
+
 /-! ### Sets defined as an if-then-else -/
 
 lemma mem_dite_univ_right (p : Prop) [decidable p] (t : p → set α) (x : α) :
diff --git a/src/data/set/image.lean b/src/data/set/image.lean
index b5d416816794a..fba4f00b8d959 100644
--- a/src/data/set/image.lean
+++ b/src/data/set/image.lean
@@ -471,6 +471,29 @@ end
 
 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) :=
+begin
+  ext t,
+  simp_rw [mem_union, mem_image, mem_powerset_iff],
+  split,
+  { 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}},
+  { rintros (h | ⟨s', h₁, rfl⟩),
+    { exact subset_trans h (subset_insert a s) },
+    { exact insert_subset_insert h₁ }}
+end
+
 /-! ### Lemmas about range of a function. -/
 section range
 variables {f : ι → α} {s t : set α}