feat: port Data.Finset.Option (#1596)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Mathlib.lean

@@ -226,6 +226,7 @@ import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Card
 import Mathlib.Data.Finset.Fold
 import Mathlib.Data.Finset.Image
+import Mathlib.Data.Finset.Option
 import Mathlib.Data.Finset.Order
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.FunLike.Basic

Mathlib/Data/Finset/Option.lean

@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Mario Carneiro, Sean Leather
+
+! This file was ported from Lean 3 source module data.finset.option
+! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Finset.Card
+import Mathlib.Order.Hom.Basic
+
+/-!
+# Finite sets in `option α`
+
+In this file we define
+
+* `Option.toFinset`: construct an empty or singleton `Finset α` from an `Option α`;
+* `Finset.insertNone`: given `s : Finset α`, lift it to a finset on `Option α` using `Option.some`
+  and then insert `Option.none`;
+* `Finset.eraseNone`: given `s : Finset (option α)`, returns `t : Finset α` such that
+  `x ∈ t ↔ some x ∈ s`.
+
+Then we prove some basic lemmas about these definitions.
+
+## Tags
+
+finset, option
+-/
+
+
+variable {α β : Type _}
+
+open Function
+
+namespace Option
+
+/-- Construct an empty or singleton finset from an `Option` -/
+def toFinset (o : Option α) : Finset α :=
+  o.elim ∅ singleton
+#align option.to_finset Option.toFinset
+
+@[simp]
+theorem toFinset_none : none.toFinset = (∅ : Finset α) :=
+  rfl
+#align option.to_finset_none Option.toFinset_none
+
+@[simp]
+theorem toFinset_some {a : α} : (some a).toFinset = {a} :=
+  rfl
+#align option.to_finset_some Option.toFinset_some
+
+@[simp]
+theorem mem_toFinset {a : α} {o : Option α} : a ∈ o.toFinset ↔ a ∈ o := by
+  cases o <;> simp [eq_comm]
+#align option.mem_to_finset Option.mem_toFinset
+
+theorem card_toFinset (o : Option α) : o.toFinset.card = o.elim 0 1 := by cases o <;> rfl
+#align option.card_to_finset Option.card_toFinset
+
+end Option
+
+namespace Finset
+
+/-- Given a finset on `α`, lift it to being a finset on `Option α`
+using `Option.some` and then insert `Option.none`. -/
+def insertNone : Finset α ↪o Finset (Option α) :=
+  (OrderEmbedding.ofMapLeIff fun s => cons none (s.map Embedding.some) <| by simp) fun s t => by
+    rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
+#align finset.insert_none Finset.insertNone
+
+@[simp]
+theorem mem_insertNone {s : Finset α} : ∀ {o : Option α}, o ∈ insertNone s ↔ ∀ a ∈ o, a ∈ s
+  | none => iff_of_true (Multiset.mem_cons_self _ _) fun a h => by cases h
+  | some a => Multiset.mem_cons.trans <| by simp
+#align finset.mem_insert_none Finset.mem_insertNone
+
+theorem some_mem_insertNone {s : Finset α} {a : α} : some a ∈ insertNone s ↔ a ∈ s := by simp
+#align finset.some_mem_insert_none Finset.some_mem_insertNone
+
+@[simp]
+theorem card_insertNone (s : Finset α) : s.insertNone.card = s.card + 1 := by simp [insertNone]
+#align finset.card_insert_none Finset.card_insertNone
+
+/-- Given `s : Finset (Option α)`, `eraseNone s : Finset α` is the set of `x : α` such that
+`some x ∈ s`. -/
+def eraseNone : Finset (Option α) →o Finset α :=
+  (Finset.mapEmbedding (Equiv.optionIsSomeEquiv α).toEmbedding).toOrderHom.comp
+    ⟨Finset.subtype _, subtype_mono⟩
+#align finset.erase_none Finset.eraseNone
+
+@[simp]
+theorem mem_eraseNone {s : Finset (Option α)} {x : α} : x ∈ eraseNone s ↔ some x ∈ s := by
+  simp [eraseNone]
+#align finset.mem_erase_none Finset.mem_eraseNone
+
+theorem eraseNone_eq_bUnion [DecidableEq α] (s : Finset (Option α)) :
+    eraseNone s = s.bunionᵢ Option.toFinset := by
+  ext
+  simp
+#align finset.erase_none_eq_bUnion Finset.eraseNone_eq_bUnion
+
+@[simp]
+theorem eraseNone_map_some (s : Finset α) : eraseNone (s.map Embedding.some) = s := by
+  ext
+  simp
+#align finset.erase_none_map_some Finset.eraseNone_map_some
+
+@[simp]
+theorem eraseNone_image_some [DecidableEq (Option α)] (s : Finset α) :
+    eraseNone (s.image some) = s := by simpa only [map_eq_image] using eraseNone_map_some s
+#align finset.erase_none_image_some Finset.eraseNone_image_some
+
+@[simp]
+theorem coe_eraseNone (s : Finset (Option α)) : (eraseNone s : Set α) = some ⁻¹' s :=
+  Set.ext fun _ => mem_eraseNone
+#align finset.coe_erase_none Finset.coe_eraseNone
+
+@[simp]
+theorem eraseNone_union [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
+    eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t := by
+  ext
+  simp
+#align finset.erase_none_union Finset.eraseNone_union
+
+@[simp]
+theorem eraseNone_inter [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
+    eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t := by
+  ext
+  simp
+#align finset.erase_none_inter Finset.eraseNone_inter
+
+@[simp]
+theorem eraseNone_empty : eraseNone (∅ : Finset (Option α)) = ∅ := by
+  ext
+  simp
+#align finset.erase_none_empty Finset.eraseNone_empty
+
+@[simp]
+theorem eraseNone_none : eraseNone ({none} : Finset (Option α)) = ∅ := by
+  ext
+  simp
+#align finset.erase_none_none Finset.eraseNone_none
+
+@[simp]
+theorem image_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
+    (eraseNone s).image some = s.erase none := by ext (_ | x) <;> simp
+#align finset.image_some_erase_none Finset.image_some_eraseNone
+
+@[simp]
+theorem map_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
+    (eraseNone s).map Embedding.some = s.erase none := by
+  rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]
+#align finset.map_some_erase_none Finset.map_some_eraseNone
+
+@[simp]
+theorem insert_none_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
+    insertNone (eraseNone s) = insert none s := by ext (_ | x) <;> simp
+#align finset.insert_none_erase_none Finset.insert_none_eraseNone
+
+@[simp]
+theorem eraseNone_insert_none (s : Finset α) : eraseNone (insertNone s) = s := by
+  ext
+  simp
+#align finset.erase_none_insert_none Finset.eraseNone_insert_none
+
+end Finset