Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-12 19:33 4a4a3a90

View on Github →

chore(data/finset/basic): Golf and compress (#11987)

  • Move the lattice instance earlier so that it can be used to prove lemmas
  • Golf proofs
  • Compress statements within the style guidelines

Estimated changes

modified theorem equiv.finset_congr_refl
modified theorem equiv.finset_congr_symm
modified theorem finset.bUnion_congr
modified theorem finset.bUnion_mono
modified theorem finset.coe_eq_empty
modified theorem finset.coe_to_list
modified def finset.cons
modified theorem finset.cons_subset_cons
modified theorem finset.cons_val
modified theorem finset.disj_union_eq_union
modified theorem finset.disjoint_bUnion_left
modified theorem finset.disjoint_filter
modified theorem finset.disjoint_iff_ne
modified theorem finset.disjoint_insert_left
modified theorem finset.disjoint_left
modified theorem finset.disjoint_right
modified theorem finset.disjoint_sdiff
modified theorem finset.disjoint_singleton
modified theorem finset.disjoint_union_left
modified theorem finset.disjoint_union_right
modified theorem finset.disjoint_val
modified theorem finset.empty_inter
modified theorem finset.empty_sdiff
modified theorem finset.eq_of_mem_singleton
modified theorem finset.erase_inj
modified theorem finset.erase_inj_on
modified theorem finset.exists_mem_insert
modified theorem finset.filter_eq
modified theorem finset.filter_ne'
modified theorem finset.filter_ne
modified theorem finset.forall_mem_insert
modified theorem finset.forall_mem_union
modified theorem finset.image_id
modified theorem finset.image_inter
modified theorem finset.image_subset_iff
modified theorem finset.inf_eq_inter
modified theorem finset.insert_eq_of_mem
modified theorem finset.insert_sdiff_of_mem
modified theorem finset.insert_subset
modified theorem finset.insert_union_distrib
modified theorem finset.inter_empty
modified theorem finset.inter_sdiff
modified theorem finset.inter_self
modified theorem finset.inter_val
modified theorem finset.map_insert
modified theorem finset.map_subtype_subset
modified theorem finset.mem_bUnion
modified theorem finset.mem_cons
modified theorem finset.mem_cons_self
modified theorem finset.mem_image_const
modified theorem finset.mem_image_const_self
modified theorem finset.mem_insert
modified theorem finset.mem_insert_of_mem
modified theorem finset.mem_map'
modified theorem finset.mem_map_equiv
modified theorem finset.mem_map_of_mem
modified theorem finset.mem_of_mem_erase
modified theorem finset.mem_range_le
modified theorem finset.mem_union
modified theorem finset.mem_union_left
modified theorem finset.mem_union_right
modified theorem finset.mk_cons
modified theorem finset.monotone_filter_left
modified theorem finset.ne_insert_of_not_mem
modified theorem finset.ne_of_mem_erase
modified theorem finset.nonempty.bUnion
deleted theorem finset.nonempty.image
modified theorem finset.nonempty.image_iff
modified theorem finset.nonempty_cons
modified theorem finset.not_disjoint_iff
modified theorem finset.not_mem_union
modified def finset.piecewise
modified theorem finset.piecewise_coe
modified theorem finset.piecewise_empty
modified theorem finset.piecewise_eq_of_mem
modified theorem finset.piecewise_insert
modified theorem finset.range_add_one
modified theorem finset.sdiff_disjoint
modified theorem finset.sdiff_empty
modified theorem finset.sdiff_eq_self
modified theorem finset.sdiff_erase
modified theorem finset.sdiff_idem
modified theorem finset.sdiff_inter_self
modified theorem finset.sdiff_self
modified theorem finset.sdiff_ssubset
modified theorem finset.sdiff_subset
modified theorem finset.sdiff_subset_sdiff
modified theorem finset.sdiff_union_distrib
modified theorem finset.sdiff_union_inter
modified theorem finset.singleton_subset_iff
modified theorem finset.ssubset_iff
modified theorem finset.ssubset_insert
modified theorem finset.subset_bUnion_of_mem
modified theorem finset.subset_image_iff
modified theorem finset.subset_insert
modified theorem finset.subset_inter
modified theorem finset.subset_inter_iff
modified theorem finset.sup_eq_union
modified theorem finset.to_list_empty
modified theorem finset.union_assoc
modified theorem finset.union_comm
modified theorem finset.union_idempotent
modified theorem finset.union_left_comm
modified theorem finset.union_right_comm
modified theorem finset.union_sdiff_distrib
modified theorem finset.union_sdiff_self
modified theorem finset.union_subset
modified theorem finset.union_subset_iff
modified theorem finset.union_subset_left
modified theorem finset.union_subset_right
modified theorem finset.union_subset_union
modified theorem finset.union_val
modified theorem finset.union_val_nd
modified theorem list.mem_to_finset
modified theorem list.to_finset.ext
modified theorem list.to_finset_append
modified theorem list.to_finset_cons
modified theorem list.to_finset_eq
modified theorem list.to_finset_eq_empty_iff
modified theorem list.to_finset_eq_of_perm
modified theorem list.to_finset_nil
modified theorem list.to_finset_reverse
modified theorem multiset.mem_to_finset
modified theorem multiset.to_finset_add
modified theorem multiset.to_finset_inter
modified theorem multiset.to_finset_subset
modified theorem multiset.to_finset_union
modified theorem multiset.to_finset_zero