[Merged by Bors] - feat(Finset): extra toLeft/toRight API

Mathlib/Data/Finset/Sum.lean

@@ -35,11 +35,9 @@ def disjSum : Finset (α ⊕ β) :=
 theorem val_disjSum : (s.disjSum t).1 = s.1.disjSum t.1 :=
   rfl
 
-@[simp]
 theorem empty_disjSum : (∅ : Finset α).disjSum t = t.map Embedding.inr :=
   val_inj.1 <| Multiset.zero_disjSum _
 
-@[simp]
 theorem disjSum_empty : s.disjSum (∅ : Finset β) = s.map Embedding.inl :=
   val_inj.1 <| Multiset.disjSum_zero _
 
@@ -110,25 +108,22 @@ forms a quasi-inverse to `disjSum`, in that it recovers its left input.
 
 See also `List.partitionMap`.
 -/
-def toLeft (s : Finset (α ⊕ β)) : Finset α :=
-  s.filterMap (Sum.elim some fun _ => none) (by clear x; aesop)
+def toLeft (u : Finset (α ⊕ β)) : Finset α :=
+  u.filterMap (Sum.elim some fun _ => none) (by clear x; aesop)
 
 /--
 Given a finset of elements `α ⊕ β`, extract all the elements of the form `β`. This
 forms a quasi-inverse to `disjSum`, in that it recovers its right input.
 
 See also `List.partitionMap`.
 -/
-def toRight (s : Finset (α ⊕ β)) : Finset β :=
-  s.filterMap (Sum.elim (fun _ => none) some) (by clear x; aesop)
+def toRight (u : Finset (α ⊕ β)) : Finset β :=
+  u.filterMap (Sum.elim (fun _ => none) some) (by clear x; aesop)
 
-variable {u v : Finset (α ⊕ β)}
+variable {u v : Finset (α ⊕ β)} {a : α} {b : β}
 
-@[simp] lemma mem_toLeft {x : α} : x ∈ u.toLeft ↔ inl x ∈ u := by
-  simp [toLeft]
-
-@[simp] lemma mem_toRight {x : β} : x ∈ u.toRight ↔ inr x ∈ u := by
-  simp [toRight]
+@[simp] lemma mem_toLeft : a ∈ u.toLeft ↔ .inl a ∈ u := by simp [toLeft]
+@[simp] lemma mem_toRight : b ∈ u.toRight ↔ .inr b ∈ u := by simp [toRight]
 
 @[gcongr]
 lemma toLeft_subset_toLeft : u ⊆ v → u.toLeft ⊆ v.toLeft :=
@@ -144,13 +139,13 @@ lemma toRight_monotone : Monotone (@toRight α β) := fun _ _ => toRight_subset_
 lemma toLeft_disjSum_toRight : u.toLeft.disjSum u.toRight = u := by
   ext (x | x) <;> simp
 
-lemma card_toLeft_add_card_toRight : u.toLeft.card + u.toRight.card = u.card := by
+lemma card_toLeft_add_card_toRight : #u.toLeft + #u.toRight = #u := by
   rw [← card_disjSum, toLeft_disjSum_toRight]
 
-lemma card_toLeft_le : u.toLeft.card ≤ u.card :=
+lemma card_toLeft_le : #u.toLeft ≤ #u :=
   (Nat.le_add_right _ _).trans_eq card_toLeft_add_card_toRight
 
-lemma card_toRight_le : u.toRight.card ≤ u.card :=
+lemma card_toRight_le : #u.toRight ≤ #u :=
   (Nat.le_add_left _ _).trans_eq card_toLeft_add_card_toRight
 
 @[simp] lemma toLeft_disjSum : (s.disjSum t).toLeft = s := by ext x; simp
@@ -163,6 +158,9 @@ lemma disjSum_eq_iff : s.disjSum t = u ↔ s = u.toLeft ∧ t = u.toRight :=
 lemma eq_disjSum_iff : u = s.disjSum t ↔ u.toLeft = s ∧ u.toRight = t :=
   ⟨fun h => by simp [h], fun h => by simp [← h, toLeft_disjSum_toRight]⟩
 
+lemma disjSum_subset : s.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight := by simp [subset_iff]
+lemma subset_disjSum : u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t := by simp [subset_iff]
+
 @[simp] lemma toLeft_map_sumComm : (u.map (Equiv.sumComm _ _).toEmbedding).toLeft = u.toRight := by
   ext x; simp
 

Mathlib/Data/Fintype/Sum.lean

@@ -24,10 +24,32 @@ instance (α : Type u) (β : Type v) [Fintype α] [Fintype β] : Fintype (α ⊕
   elems := univ.disjSum univ
   complete := by rintro (_ | _) <;> simp
 
-@[simp]
-theorem Finset.univ_disjSum_univ {α β : Type*} [Fintype α] [Fintype β] :
-    univ.disjSum univ = (univ : Finset (α ⊕ β)) :=
-  rfl
+namespace Finset
+variable {α β : Type*} {u : Finset (α ⊕ β)} {s : Finset α} {t : Finset β}
+
+section left
+variable [Fintype α] {u : Finset (α ⊕ β)}
+
+lemma toLeft_eq_univ : u.toLeft = univ ↔ univ.disjSum ∅ ⊆ u := by simp [disjSum_subset]
+lemma toRight_eq_empty : u.toRight = ∅ ↔ u ⊆ univ.disjSum ∅ := by simp [subset_disjSum]
+
+end left
+
+section right
+variable [Fintype β] {u : Finset (α ⊕ β)}
+
+lemma toRight_eq_univ : u.toRight = univ ↔ disjSum ∅ univ ⊆ u := by simp [disjSum_subset]
+lemma toLeft_eq_empty : u.toLeft = ∅ ↔ u ⊆ disjSum ∅ univ := by simp [subset_disjSum]
+
+end right
+
+variable [Fintype α] [Fintype β]
+
+@[simp] lemma univ_disjSum_univ : univ.disjSum univ = (univ : Finset (α ⊕ β)) := rfl
+@[simp] lemma toLeft_univ : (univ : Finset (α ⊕ β)).toLeft = univ := by ext; simp
+@[simp] lemma toRight_univ : (univ : Finset (α ⊕ β)).toRight = univ := by ext; simp
+
+end Finset
 
 @[simp]
 theorem Fintype.card_sum [Fintype α] [Fintype β] :