chore(*): to_additive related cleanup (#11559)

A few to_additive related cleanups
* Move measurability before to_additive to avoid having to manually do it later (or forget).
* Ensure anything tagged to_additive, mono has the additive version also mono'd
* Move simp before to_additive

src/algebra/order/lattice_group.lean

@@ -433,7 +433,7 @@ end
 /--
 The unary operation of taking the absolute value is idempotent.
 -/
-@[to_additive abs_abs, simp]
+@[simp, to_additive abs_abs]
 lemma m_abs_abs [covariant_class α α (*) (≤)] (a : α) : | |a| | = |a| :=
 mabs_of_one_le _ (one_le_abs _)
 

src/algebra/pointwise.lean

@@ -813,6 +813,8 @@ by simp [finset.mul_def]
 @[to_additive, mono] lemma mul_subset_mul  (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁ * t₁ ⊆ s₂ * t₂ :=
 image_subset_image (product_subset_product hs ht)
 
+attribute [mono] add_subset_add
+
 @[simp, to_additive]
 lemma mul_singleton (a : α) : s * {a} = s.image (* a) :=
 by { rw [mul_def, product_singleton, map_eq_image, image_image], refl }

src/measure_theory/group/arithmetic.lean

@@ -88,43 +88,43 @@ variables {M α : Type*} [measurable_space M] [has_mul M] {m : measurable_space
 
 include m
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.const_mul [has_measurable_mul M] (hf : measurable f) (c : M) :
   measurable (λ x, c * f x) :=
 (measurable_const_mul c).comp hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.const_mul [has_measurable_mul M] (hf : ae_measurable f μ) (c : M) :
   ae_measurable (λ x, c * f x) μ :=
 (has_measurable_mul.measurable_const_mul c).comp_ae_measurable hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.mul_const [has_measurable_mul M] (hf : measurable f) (c : M) :
   measurable (λ x, f x * c) :=
 (measurable_mul_const c).comp hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.mul_const [has_measurable_mul M] (hf : ae_measurable f μ) (c : M) :
   ae_measurable (λ x, f x * c) μ :=
 (measurable_mul_const c).comp_ae_measurable hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.mul' [has_measurable_mul₂ M] (hf : measurable f) (hg : measurable g) :
   measurable (f * g) :=
 measurable_mul.comp (hf.prod_mk hg)
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.mul [has_measurable_mul₂ M] (hf : measurable f) (hg : measurable g) :
   measurable (λ a, f a * g a) :=
 measurable_mul.comp (hf.prod_mk hg)
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.mul' [has_measurable_mul₂ M] (hf : ae_measurable f μ)
   (hg : ae_measurable g μ) :
   ae_measurable (f * g) μ :=
 measurable_mul.comp_ae_measurable (hf.prod_mk hg)
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.mul [has_measurable_mul₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
   ae_measurable (λ a, f a * g a) μ :=
 measurable_mul.comp_ae_measurable (hf.prod_mk hg)
@@ -233,43 +233,43 @@ variables {G α : Type*} [measurable_space G] [has_div G] {m : measurable_space
 
 include m
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.const_div [has_measurable_div G] (hf : measurable f) (c : G) :
   measurable (λ x, c / f x) :=
 (has_measurable_div.measurable_const_div c).comp hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.const_div [has_measurable_div G] (hf : ae_measurable f μ) (c : G) :
   ae_measurable (λ x, c / f x) μ :=
 (has_measurable_div.measurable_const_div c).comp_ae_measurable hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.div_const [has_measurable_div G] (hf : measurable f) (c : G) :
   measurable (λ x, f x / c) :=
 (has_measurable_div.measurable_div_const c).comp hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.div_const [has_measurable_div G] (hf : ae_measurable f μ) (c : G) :
   ae_measurable (λ x, f x / c) μ :=
 (has_measurable_div.measurable_div_const c).comp_ae_measurable hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.div' [has_measurable_div₂ G] (hf : measurable f) (hg : measurable g) :
   measurable (f / g) :=
 measurable_div.comp (hf.prod_mk hg)
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.div [has_measurable_div₂ G] (hf : measurable f) (hg : measurable g) :
   measurable (λ a, f a / g a) :=
 measurable_div.comp (hf.prod_mk hg)
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.div' [has_measurable_div₂ G] (hf : ae_measurable f μ)
   (hg : ae_measurable g μ) :
   ae_measurable (f / g) μ :=
 measurable_div.comp_ae_measurable (hf.prod_mk hg)
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.div [has_measurable_div₂ G] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
   ae_measurable (λ a, f a / g a) μ :=
 measurable_div.comp_ae_measurable (hf.prod_mk hg)
@@ -336,10 +336,10 @@ variables {G α : Type*} [has_inv G] [measurable_space G] [has_measurable_inv G]
 
 include m
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma measurable.inv (hf : measurable f) : measurable (λ x, (f x)⁻¹) := measurable_inv.comp hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma ae_measurable.inv (hf : ae_measurable f μ) : ae_measurable (λ x, (f x)⁻¹) μ :=
 measurable_inv.comp_ae_measurable hf
 
@@ -613,7 +613,7 @@ variables {M α : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂
 
 include m
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma list.measurable_prod' (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) :
   measurable l.prod :=
 begin
@@ -623,7 +623,7 @@ begin
   exact hl.1.mul (ihl hl.2)
 end
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma list.ae_measurable_prod' (l : list (α → M))
   (hl : ∀ f ∈ l, ae_measurable f μ) : ae_measurable l.prod μ :=
 begin
@@ -633,12 +633,12 @@ begin
   exact hl.1.mul (ihl hl.2)
 end
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma list.measurable_prod (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) :
   measurable (λ x, (l.map (λ f : α → M, f x)).prod) :=
 by simpa only [← pi.list_prod_apply] using l.measurable_prod' hl
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma list.ae_measurable_prod (l : list (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) :
   ae_measurable (λ x, (l.map (λ f : α → M, f x)).prod) μ :=
 by simpa only [← pi.list_prod_apply] using l.ae_measurable_prod' hl
@@ -653,52 +653,47 @@ variables {M ι α : Type*} [comm_monoid M] [measurable_space M] [has_measurable
 
 include m
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma multiset.measurable_prod' (l : multiset (α → M)) (hl : ∀ f ∈ l, measurable f) :
   measurable l.prod :=
 by { rcases l with ⟨l⟩, simpa using l.measurable_prod' (by simpa using hl) }
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma multiset.ae_measurable_prod' (l : multiset (α → M))
   (hl : ∀ f ∈ l, ae_measurable f μ) : ae_measurable l.prod μ :=
 by { rcases l with ⟨l⟩, simpa using l.ae_measurable_prod' (by simpa using hl) }
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma multiset.measurable_prod (s : multiset (α → M)) (hs : ∀ f ∈ s, measurable f) :
   measurable (λ x, (s.map (λ f : α → M, f x)).prod) :=
 by simpa only [← pi.multiset_prod_apply] using s.measurable_prod' hs
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma multiset.ae_measurable_prod (s : multiset (α → M))
   (hs : ∀ f ∈ s, ae_measurable f μ) : ae_measurable (λ x, (s.map (λ f : α → M, f x)).prod) μ :=
 by simpa only [← pi.multiset_prod_apply] using s.ae_measurable_prod' hs
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma finset.measurable_prod' (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) :
   measurable (∏ i in s, f i) :=
 finset.prod_induction _ _ (λ _ _, measurable.mul) (@measurable_one M _ _ _ _) hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma finset.measurable_prod (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) :
   measurable (λ a, ∏ i in s, f i a) :=
 by simpa only [← finset.prod_apply] using s.measurable_prod' hf
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma finset.ae_measurable_prod' (s : finset ι) (hf : ∀i ∈ s, ae_measurable (f i) μ) :
   ae_measurable (∏ i in s, f i) μ :=
 multiset.ae_measurable_prod' _ $
   λ g hg, let ⟨i, hi, hg⟩ := multiset.mem_map.1 hg in (hg ▸ hf _ hi)
 
-@[to_additive, measurability]
+@[measurability, to_additive]
 lemma finset.ae_measurable_prod (s : finset ι) (hf : ∀i ∈ s, ae_measurable (f i) μ) :
   ae_measurable (λ a, ∏ i in s, f i a) μ :=
 by simpa only [← finset.prod_apply] using s.ae_measurable_prod' hf
 
 omit m
 
 end comm_monoid
-
-attribute [measurability] list.measurable_sum' list.ae_measurable_sum' list.measurable_sum
-  list.ae_measurable_sum multiset.measurable_sum' multiset.ae_measurable_sum'
-  multiset.measurable_sum multiset.ae_measurable_sum finset.measurable_sum'
-  finset.ae_measurable_sum' finset.measurable_sum finset.ae_measurable_sum

src/measure_theory/measurable_space.lean

@@ -248,13 +248,11 @@ lemma measurable.indicator [has_zero β] (hf : measurable f) (hs : measurable_se
   measurable (s.indicator f) :=
 hf.piecewise hs measurable_const
 
-@[to_additive, measurability] lemma measurable_set_mul_support [has_one β]
+@[measurability, to_additive] lemma measurable_set_mul_support [has_one β]
   [measurable_singleton_class β] (hf : measurable f) :
   measurable_set (mul_support f) :=
 hf (measurable_set_singleton 1).compl
 
-attribute [measurability] measurable_set_support
-
 /-- If a function coincides with a measurable function outside of a countable set, it is
 measurable. -/
 lemma measurable.measurable_of_countable_ne [measurable_singleton_class α]