From 6f4ee5ed2e7954914322eebf8589ecd55878528c Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Fri, 5 Jun 2020 05:31:15 +0000
Subject: [PATCH] feat(data/setoid/partition): some lemmas about partitions
 (#2937)

---
 src/data/setoid/partition.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/data/setoid/partition.lean b/src/data/setoid/partition.lean
index ec02348416e0b..6c0d4b0ad9458 100644
--- a/src/data/setoid/partition.lean
+++ b/src/data/setoid/partition.lean
@@ -128,6 +128,18 @@ lemma nonempty_of_mem_partition {c : set (set α)} (hc : is_partition c) {s} (h
   s.nonempty :=
 set.ne_empty_iff_nonempty.1 $ λ hs0, hc.1 $ hs0 ▸ h
 
+lemma is_partition_classes (r : setoid α) : is_partition r.classes :=
+⟨empty_not_mem_classes, classes_eqv_classes⟩
+
+lemma is_partition.pairwise_disjoint {c : set (set α)} (hc : is_partition c) : 
+  c.pairwise_disjoint :=
+eqv_classes_disjoint hc.2
+
+lemma is_partition.sUnion_eq_univ {c : set (set α)} (hc : is_partition c) : 
+  ⋃₀ c = set.univ :=
+set.eq_univ_of_forall $ λ x, set.mem_sUnion.2 $
+  let ⟨t, ht⟩ := hc.2 x in ⟨t, by clear_aux_decl; finish⟩
+
 /-- All elements of a partition of α are the equivalence class of some y ∈ α. -/
 lemma exists_of_mem_partition {c : set (set α)} (hc : is_partition c) {s} (hs : s ∈ c) :
   ∃ y, s = {x | (mk_classes c hc.2).rel x y} :=