From ca895e49010670027e2ffb667339671623e5f428 Mon Sep 17 00:00:00 2001
From: Haitao Zhang <zhtprog@gmail.com>
Date: Thu, 16 Jul 2015 14:13:06 -0700
Subject: [PATCH] fix(library/data/finset/partition): improve lemmas on binary
 partition

---
 library/data/finset/partition.lean        | 24 ++++++++++++++++++-----
 library/theories/group_theory/action.lean |  5 +++--
 2 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/library/data/finset/partition.lean b/library/data/finset/partition.lean
index 4059e2875..cf74cc562 100644
--- a/library/data/finset/partition.lean
+++ b/library/data/finset/partition.lean
@@ -114,13 +114,27 @@ begin rewrite [binary_union P at {1}], apply Union_union, exact binary_inter_emp
 end
 
 open nat
+section
+open algebra
+
+variables {B : Type} [acmB : add_comm_monoid B]
+include acmB
+
+lemma Sum_binary_union (f : A → B) (P : A → Prop) [decP : decidable_pred P] {S : finset A} :
+  Sum S f = Sum {s ∈ S | P s} f + Sum {s ∈ S | ¬P s} f :=
+calc
+  Sum S f = Sum ({s ∈ S | P s} ∪ {s ∈ S | ¬(P s)}) f : binary_union
+      ... = Sum {s ∈ S | P s} f + Sum {s ∈ S | ¬P s} f : Sum_union f binary_inter_empty
+
+end
+
 lemma card_binary_Union_disjoint_sets (P : finset A → Prop) [decP : decidable_pred P] {S : finset (finset A)} :
-  disjoint_sets S → Sum S card = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card :=
+  disjoint_sets S → card (Union S id) = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card :=
 assume Pds, calc
-  Sum S card = card (Union S id) : card_Union_of_disjoint S id Pds
-         ... = card (Union {s ∈ S | P s} id ∪ Union {s ∈ S | ¬P s} id) : binary_Union
-         ... = card (Union {s ∈ S | P s} id) + card (Union {s ∈ S | ¬P s} id) : card_union_of_disjoint (binary_inter_empty_Union_disjoint_sets Pds)
-         ... = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card : by rewrite [*(card_Union_of_disjoint _ id (disjoint_sets_filter_of_disjoint_sets Pds))]
+        card (Union S id)
+      = card (Union {s ∈ S | P s} id ∪ Union {s ∈ S | ¬P s} id) : binary_Union
+  ... = card (Union {s ∈ S | P s} id) + card (Union {s ∈ S | ¬P s} id) : card_union_of_disjoint (binary_inter_empty_Union_disjoint_sets Pds)
+  ... = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card : by rewrite [*(card_Union_of_disjoint _ id (disjoint_sets_filter_of_disjoint_sets Pds))]
 
 end partition
 end finset
diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean
index 6e2069cef..0dd68d60a 100644
--- a/library/theories/group_theory/action.lean
+++ b/library/theories/group_theory/action.lean
@@ -371,10 +371,11 @@ calc Sum _ _ = Sum (fixed_point_orbits hom H) (λ x, 1) : Sum_ext (take c Pin, o
          ... = card (fixed_point_orbits hom H) * 1 : Sum_const_eq_card_mul
          ... = card (fixed_point_orbits hom H) : mul_one (card (fixed_point_orbits hom H))
 
+local attribute nat.comm_semiring [instance]
 lemma orbit_class_equation' : card S = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card :=
 calc card S = Sum (orbits hom H) finset.card : orbit_class_equation
-        ... = Sum (fixed_point_orbits hom H) finset.card + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_binary_Union_disjoint_sets _ (equiv_class_disjoint _)
-        ... = card (fixed_point_orbits hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_fixed_point_orbits
+        ... = Sum (fixed_point_orbits hom H) finset.card + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : Sum_binary_union
+        ... = card (fixed_point_orbits hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : {card_fixed_point_orbits}
         ... = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_fixed_point_orbits_eq
 
 end orbit_partition