Commit 2019-09-18 15:46 08390f54

refactor(algebra/big_operators,data/finset): use finset.disjoint in definitions (#1456)

• Use finset.disjoint in algebra/big_operators
• New lemma disjoint_filter It should be a painless step from using filter_inter_filter_neg_eq to using this lemma
• Update other dependencies of finset.prod_union and finset.prod_bind
• Reformat some lines to make them fit within 100 characters
• We can actually do away with two non-terminal simps now