feat(data/set/pairwise): Simple pairwise_disjoint lemmas (#9764)

src/algebra/support.lean

@@ -283,6 +283,6 @@ end
 
 lemma support_single_disjoint {b' : B} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : A} :
   disjoint (function.support (single i b)) (function.support (single j b')) ↔ i ≠ j :=
-by simpa [support_single, hb, hb'] using ne_comm
+by rw [support_single_of_ne hb, support_single_of_ne hb', disjoint_singleton]
 
 end pi

src/data/finset/basic.lean

@@ -2831,11 +2831,15 @@ disjoint_right.2 (λ x m₁, (disjoint_right.1 d) (h m₁))
 
 @[simp] theorem disjoint_empty_right (s : finset α) : disjoint s ∅ := disjoint_bot_right
 
-@[simp] theorem singleton_disjoint {s : finset α} {a : α} : disjoint (singleton a) s ↔ a ∉ s :=
+@[simp] theorem disjoint_singleton_left {s : finset α} {a : α} : disjoint (singleton a) s ↔ a ∉ s :=
 by simp only [disjoint_left, mem_singleton, forall_eq]
 
-@[simp] theorem disjoint_singleton {s : finset α} {a : α} : disjoint s (singleton a) ↔ a ∉ s :=
-disjoint.comm.trans singleton_disjoint
+@[simp] theorem disjoint_singleton_right {s : finset α} {a : α} :
+  disjoint s (singleton a) ↔ a ∉ s :=
+disjoint.comm.trans disjoint_singleton_left
+
+@[simp] lemma disjoint_singleton {a b : α} : disjoint ({a} : finset α) {b} ↔ a ≠ b :=
+by rw [disjoint_singleton_left, mem_singleton]
 
 @[simp] theorem disjoint_insert_left {a : α} {s t : finset α} :
   disjoint (insert a s) t ↔ a ∉ t ∧ disjoint s t :=

src/data/finsupp/basic.lean

@@ -302,7 +302,7 @@ end
 
 lemma support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
   disjoint (single i b).support (single j b').support ↔ i ≠ j :=
-by simpa [support_single_ne_zero, hb, hb'] using ne_comm
+by rw [support_single_ne_zero hb, support_single_ne_zero hb', disjoint_singleton]
 
 @[simp] lemma single_eq_zero : single a b = 0 ↔ b = 0 :=
 by simp [ext_iff, single_eq_indicator]
@@ -1975,7 +1975,7 @@ begin
     rw [to_multiset_add, multiset.to_finset_add, ih, to_multiset_single, support_add_eq,
       support_single_ne_zero hn, multiset.to_finset_nsmul _ _ hn, multiset.to_finset_singleton],
     refine disjoint.mono_left support_single_subset _,
-    rwa [finset.singleton_disjoint] }
+    rwa [finset.disjoint_singleton_left] }
 end
 
 @[simp] lemma count_to_multiset [decidable_eq α] (f : α →₀ ℕ) (a : α) :

src/data/polynomial/iterated_deriv.lean

@@ -136,8 +136,8 @@ begin
       apply congr_arg2,
       { refl },
       { simp only [prod_singleton], norm_cast },
-      { simp only [succ_pos', disjoint_singleton, and_true, lt_add_iff_pos_right, not_le, mem_Ico],
-        exact lt_add_one (m + 1) } },
+      { rw [disjoint_singleton_right, mem_Ico],
+        exact λ h, (nat.lt_succ_self _).not_le h.1 } },
     { exact congr_arg _ (succ_add m k) } },
 end
 

src/data/set/lattice.lean

@@ -1499,6 +1499,9 @@ by simp [set.disjoint_iff, subset_def]; exact iff.rfl
 @[simp] theorem disjoint_singleton_right {a : α} {s : set α} : disjoint s {a} ↔ a ∉ s :=
 by rw [disjoint.comm]; exact disjoint_singleton_left
 
+@[simp] lemma disjoint_singleton {a b : α} : disjoint ({a} : set α) {b} ↔ a ≠ b :=
+by rw [disjoint_singleton_left, mem_singleton_iff]
+
 theorem disjoint_image_image {f : β → α} {g : γ → α} {s : set β} {t : set γ}
   (h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) : disjoint (f '' s) (g '' t) :=
 by rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩; exact h b hb c hc eq

src/data/set/pairwise.lean

@@ -73,31 +73,60 @@ variables [semilattice_inf_bot α]
 def pairwise_disjoint (s : set α) : Prop :=
 pairwise_on s disjoint
 
-lemma pairwise_disjoint.subset {s t : set α} (ht : pairwise_disjoint t) (h : s ⊆ t) :
-  pairwise_disjoint s :=
+lemma pairwise_disjoint.subset (ht : pairwise_disjoint t) (h : s ⊆ t) : pairwise_disjoint s :=
 pairwise_on.mono h ht
 
-lemma pairwise_disjoint.range {s : set α} (f : s → α) (hf : ∀ (x : s), f x ≤ x.1)
-  (ht : pairwise_disjoint s) : pairwise_disjoint (range f) :=
+lemma pairwise_disjoint_empty : (∅ : set α).pairwise_disjoint :=
+pairwise_on_empty _
+
+lemma pairwise_disjoint_singleton (a : α) : ({a} : set α).pairwise_disjoint :=
+pairwise_on_singleton a _
+
+lemma pairwise_disjoint_insert {a : α} :
+  (insert a s).pairwise_disjoint ↔ s.pairwise_disjoint ∧ ∀ b ∈ s, a ≠ b → disjoint a b :=
+set.pairwise_on_insert_of_symmetric symmetric_disjoint
+
+lemma pairwise_disjoint.insert (hs : s.pairwise_disjoint) {a : α}
+  (hx : ∀ b ∈ s, a ≠ b → disjoint a b) :
+  (insert a s).pairwise_disjoint :=
+set.pairwise_disjoint_insert.2 ⟨hs, hx⟩
+
+lemma pairwise_disjoint.image_of_le (hs : s.pairwise_disjoint) {f : α → α} (hf : ∀ a, f a ≤ a) :
+  (f '' s).pairwise_disjoint :=
+begin
+  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ h,
+  exact (hs a ha b hb $ ne_of_apply_ne _ h).mono (hf a) (hf b),
+end
+
+lemma pairwise_disjoint.range (f : s → α) (hf : ∀ (x : s), f x ≤ x) (ht : pairwise_disjoint s) :
+  pairwise_disjoint (range f) :=
 begin
   rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy,
   exact (ht _ x.2 _ y.2 $ λ h, hxy $ congr_arg f $ subtype.ext h).mono (hf x) (hf y),
 end
 
 -- classical
-lemma pairwise_disjoint.elim {s : set α} (hs : pairwise_disjoint s) {x y : α} (hx : x ∈ s)
+lemma pairwise_disjoint.elim (hs : pairwise_disjoint s) {x y : α} (hx : x ∈ s)
   (hy : y ∈ s) (h : ¬ disjoint x y) :
   x = y :=
 of_not_not $ λ hxy, h $ hs _ hx _ hy hxy
 
 -- classical
-lemma pairwise_disjoint.elim' {s : set α} (hs : pairwise_disjoint s) {x y : α} (hx : x ∈ s)
-  (hy : y ∈ s) (h : x ⊓ y ≠ ⊥) :
+lemma pairwise_disjoint.elim' (hs : pairwise_disjoint s) {x y : α} (hx : x ∈ s) (hy : y ∈ s)
+  (h : x ⊓ y ≠ ⊥) :
   x = y :=
 hs.elim hx hy $ λ hxy, h hxy.eq_bot
 
 end semilattice_inf_bot
 
+/-! ### Pairwise disjoint set of sets -/
+
+lemma pairwise_disjoint_range_singleton : (set.range (singleton : α → set α)).pairwise_disjoint :=
+begin
+  rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h,
+  exact disjoint_singleton.2 (ne_of_apply_ne _ h),
+end
+
 -- classical
 lemma pairwise_disjoint.elim_set {s : set (set α)} (hs : pairwise_disjoint s) {x y : set α}
   (hx : x ∈ s) (hy : y ∈ s) (z : α) (hzx : z ∈ x) (hzy : z ∈ y) : x = y :=

src/geometry/euclidean/circumcenter.lean

@@ -620,7 +620,7 @@ begin
            sum_ite, sum_const, filter_or, filter_eq'],
   rw card_union_eq,
   { simp },
-  { simp [h.symm] }
+  { simpa only [if_true, mem_univ, disjoint_singleton] using h }
 end
 
 include V

src/group_theory/specific_groups/alternating.lean

@@ -112,7 +112,7 @@ begin
     { simp only [←hπ, coe_mk, subgroup.coe_mul, subtype.val_eq_coe],
       have hd : disjoint (swap a b) σ,
       { rw [disjoint_iff_disjoint_support, support_swap ab, finset.disjoint_insert_left,
-          finset.singleton_disjoint],
+          finset.disjoint_singleton_left],
         exact ⟨finset.mem_compl.1 ha, finset.mem_compl.1 hb⟩ },
       rw [mul_assoc π _ σ, hd.commute.eq, coe_inv, coe_mk],
       simp [mul_assoc] } }

src/measure_theory/integral/bochner.lean

@@ -286,7 +286,7 @@ begin
   rw [simple_func.integral_eq_sum_filter, finset.sum_subset hs],
   rintro x - hx, rw [finset.mem_filter, not_and_distrib, ne.def, not_not] at hx,
   rcases hx with hx|rfl; [skip, simp],
-  rw [simple_func.mem_range] at hx, rw [preimage_eq_empty]; simp [disjoint_singleton_left, hx]
+  rw [simple_func.mem_range] at hx, rw [preimage_eq_empty]; simp [set.disjoint_singleton_left, hx]
 end
 
 @[simp] lemma integral_const {m : measurable_space α} (μ : measure α) (y : F) :

src/ring_theory/witt_vector/witt_polynomial.lean

@@ -169,7 +169,7 @@ begin
   { simp only [this, int.nat_cast_eq_coe_nat, bUnion_singleton_eq_self], },
   { simp only [this, int.nat_cast_eq_coe_nat],
     intros a b h,
-    apply singleton_disjoint.mpr,
+    apply disjoint_singleton_left.mpr,
     rwa mem_singleton, },
 end
 
@@ -244,7 +244,7 @@ begin
     intro i,
     rw [mem_union, mem_union],
     apply or.imp id },
-  work_on_goal 1 { rw [vars_X, singleton_disjoint] },
+  work_on_goal 1 { rw [vars_X, disjoint_singleton_left] },
   all_goals {
     intro H,
     replace H := vars_sum_subset _ _ H,

src/topology/algebra/infinite_sum.lean

@@ -1130,7 +1130,7 @@ begin
   rw [filter.mem_map],
   rcases hf.vanishing he with ⟨s, hs⟩,
   refine s.eventually_cofinite_nmem.mono (λ x hx, _),
-  by simpa using hs {x} (singleton_disjoint.2 hx)
+  by simpa using hs {x} (disjoint_singleton_left.2 hx)
 end
 
 lemma summable.tendsto_at_top_zero {f : ℕ → G} (hf : summable f) : tendsto f at_top (𝓝 0) :=

src/topology/separation.lean

@@ -528,8 +528,7 @@ lemma finset_disjoint_finset_opens_of_t2 [t2_space α] :
   ∀ (s t : finset α), disjoint s t → separated (s : set α) t :=
 begin
   refine induction_on_union _ (λ a b hi d, (hi d.symm).symm) (λ a d, empty_right a) (λ a b ab, _) _,
-  { obtain ⟨U, V, oU, oV, aU, bV, UV⟩ := t2_separation
-      (by { rw [ne.def, ← finset.mem_singleton], exact (disjoint_singleton.mp ab.symm) }),
+  { obtain ⟨U, V, oU, oV, aU, bV, UV⟩ := t2_separation (finset.disjoint_singleton.1 ab),
     refine ⟨U, V, oU, oV, _, _, set.disjoint_iff_inter_eq_empty.mpr UV⟩;
     exact singleton_subset_set_iff.mpr ‹_› },
   { intros a b c ac bc d,
@@ -539,7 +538,7 @@ end
 
 lemma point_disjoint_finset_opens_of_t2 [t2_space α] {x : α} {s : finset α} (h : x ∉ s) :
   separated ({x} : set α) s :=
-by exact_mod_cast finset_disjoint_finset_opens_of_t2 {x} s (singleton_disjoint.mpr h)
+by exact_mod_cast finset_disjoint_finset_opens_of_t2 {x} s (finset.disjoint_singleton_left.mpr h)
 
 end separated