From d4f69d96f3532729da8ebb763f4bc26fcf640f06 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sun, 18 Dec 2022 18:49:52 +0000
Subject: [PATCH] feat(algebra/big_operators/basic): Sum of `ite` (#16825)

A sum of if then else that don't happen simultaneously can be written as a single if then else.
---
 src/algebra/big_operators/basic.lean | 15 +++++++++++++++
 src/data/set/pairwise.lean           | 27 +++++++++++++++++++++++++++
 2 files changed, 42 insertions(+)

diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
index 98797855b4e12..b8641c0685d44 100644
--- a/src/algebra/big_operators/basic.lean
+++ b/src/algebra/big_operators/basic.lean
@@ -1328,6 +1328,21 @@ begin
   rwa eq_of_mem_of_not_mem_erase hx hnx
 end
 
+/-- See also `finset.prod_boole`. -/
+@[to_additive "See also `finset.sum_boole`."]
+lemma prod_ite_one {f : α → Prop} [decidable_pred f] (hf : (s : set α).pairwise_disjoint f)
+  (a : β) :
+  ∏ i in s, ite (f i) a 1 = ite (∃ i ∈ s, f i) a 1 :=
+begin
+  split_ifs,
+  { obtain ⟨i, hi, hfi⟩ := h,
+    rw [prod_eq_single_of_mem _ hi, if_pos hfi],
+    exact λ j hj h, if_neg (λ hfj, (hf hj hi h).le_bot ⟨hfj, hfi⟩) },
+  { push_neg at h,
+    rw prod_eq_one,
+    exact λ i hi, if_neg (h i hi) }
+end
+
 lemma sum_erase_lt_of_pos {γ : Type*} [decidable_eq α] [ordered_add_comm_monoid γ]
   [covariant_class γ γ (+) (<)] {s : finset α} {d : α} (hd : d ∈ s) {f : α → γ} (hdf : 0 < f d) :
   ∑ (m : α) in s.erase d, f m < ∑ (m : α) in s, f m :=
diff --git a/src/data/set/pairwise.lean b/src/data/set/pairwise.lean
index 251ba470614af..ba87b6e47e941 100644
--- a/src/data/set/pairwise.lean
+++ b/src/data/set/pairwise.lean
@@ -136,19 +136,37 @@ lemma pairwise_insert :
 by simp only [insert_eq, pairwise_union, pairwise_singleton, true_and,
   mem_singleton_iff, forall_eq]
 
+lemma pairwise_insert_of_not_mem (ha : a ∉ s) :
+  (insert a s).pairwise r ↔ s.pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a :=
+pairwise_insert.trans $ and_congr_right' $ forall₂_congr $ λ b hb,
+  by simp [(ne_of_mem_of_not_mem hb ha).symm]
+
 lemma pairwise.insert (hs : s.pairwise r) (h : ∀ b ∈ s, a ≠ b → r a b ∧ r b a) :
   (insert a s).pairwise r :=
 pairwise_insert.2 ⟨hs, h⟩
 
+lemma pairwise.insert_of_not_mem (ha : a ∉ s) (hs : s.pairwise r) (h : ∀ b ∈ s, r a b ∧ r b a) :
+  (insert a s).pairwise r :=
+(pairwise_insert_of_not_mem ha).2 ⟨hs, h⟩
+
 lemma pairwise_insert_of_symmetric (hr : symmetric r) :
   (insert a s).pairwise r ↔ s.pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b :=
 by simp only [pairwise_insert, hr.iff a, and_self]
 
+lemma pairwise_insert_of_symmetric_of_not_mem (hr : symmetric r) (ha : a ∉ s) :
+  (insert a s).pairwise r ↔ s.pairwise r ∧ ∀ b ∈ s, r a b :=
+by simp only [pairwise_insert_of_not_mem ha, hr.iff a, and_self]
+
 lemma pairwise.insert_of_symmetric (hs : s.pairwise r) (hr : symmetric r)
   (h : ∀ b ∈ s, a ≠ b → r a b) :
   (insert a s).pairwise r :=
 (pairwise_insert_of_symmetric hr).2 ⟨hs, h⟩
 
+lemma pairwise.insert_of_symmetric_of_not_mem (hs : s.pairwise r) (hr : symmetric r) (ha : a ∉ s)
+  (h : ∀ b ∈ s, r a b) :
+  (insert a s).pairwise r :=
+(pairwise_insert_of_symmetric_of_not_mem hr ha).2 ⟨hs, h⟩
+
 lemma pairwise_pair : set.pairwise {a, b} r ↔ (a ≠ b → r a b ∧ r b a) :=
 by simp [pairwise_insert]
 
@@ -226,11 +244,20 @@ lemma pairwise_disjoint_insert {i : ι} :
     ↔ s.pairwise_disjoint f ∧ ∀ j ∈ s, i ≠ j → disjoint (f i) (f j) :=
 set.pairwise_insert_of_symmetric $ symmetric_disjoint.comap f
 
+lemma pairwise_disjoint_insert_of_not_mem {i : ι} (hi : i ∉ s) :
+  (insert i s).pairwise_disjoint f ↔ s.pairwise_disjoint f ∧ ∀ j ∈ s, disjoint (f i) (f j) :=
+pairwise_insert_of_symmetric_of_not_mem (symmetric_disjoint.comap f) hi
+
 lemma pairwise_disjoint.insert (hs : s.pairwise_disjoint f) {i : ι}
   (h : ∀ j ∈ s, i ≠ j → disjoint (f i) (f j)) :
   (insert i s).pairwise_disjoint f :=
 set.pairwise_disjoint_insert.2 ⟨hs, h⟩
 
+lemma pairwise_disjoint.insert_of_not_mem (hs : s.pairwise_disjoint f) {i : ι} (hi : i ∉ s)
+  (h : ∀ j ∈ s, disjoint (f i) (f j)) :
+  (insert i s).pairwise_disjoint f :=
+(set.pairwise_disjoint_insert_of_not_mem hi).2 ⟨hs, h⟩
+
 lemma pairwise_disjoint.image_of_le (hs : s.pairwise_disjoint f) {g : ι → ι} (hg : f ∘ g ≤ f) :
   (g '' s).pairwise_disjoint f :=
 begin