fix(tactic/transport): make to_additive copy protectedstatus (#2212)

* fix(tactic/transport): make `to_additive` copy `protected`status

Fixes #2210, also slightly cleanup `algebra/group/units`

* Fix compile (protected `finset.sum`)

* Fix usage of `finset.sum`

* Update src/tactic/transport.lean

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

* fix build

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/group/to_additive.lean

@@ -112,10 +112,13 @@ do let n := src.mk_string "_to_additive",
 @[derive has_reflect, derive inhabited]
 structure value_type := (tgt : name) (doc : option string)
 
+/-- Dictionary of words used by `to_additive.guess_name` to autogenerate
+names. -/
 meta def tokens_dict : native.rb_map string string :=
 native.rb_map.of_list $
 [("mul", "add"), ("one", "zero"), ("inv", "neg"), ("prod", "sum")]
 
+/-- Autogenerate target name for `to_additive`. -/
 meta def guess_name : string → string :=
 string.map_tokens '_' $ list.map $
 string.map_tokens ''' $ list.map $

src/algebra/group/units.lean

@@ -48,59 +48,19 @@ variables [monoid α]
   a = b ↔ (a : α) = b :=
 ext.eq_iff.symm
 
-instance [decidable_eq α] : decidable_eq (units α)
-| a b := decidable_of_iff' _ ext_iff
-
-/-- The unit group inherits the multiplication of the monoid. -/
-protected def mul (u₁ u₂ : units α) : units α :=
-⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
-  have u₁.val * (u₂.val * u₂.inv) * u₁.inv = 1,
-    by rw [u₂.val_inv]; rw [mul_one, u₁.val_inv],
-  by simpa only [mul_assoc],
-  have u₂.inv * (u₁.inv * u₁.val) * u₂.val = 1,
-    by rw [u₁.inv_val]; rw [mul_one, u₂.inv_val],
-  by simpa only [mul_assoc]⟩
-
-/-- The inverse of a unit. -/
-protected def inv' (u : units α) : units α :=
-⟨u.inv, u.val, u.inv_val, u.val_inv⟩
+@[to_additive] instance [decidable_eq α] : decidable_eq (units α) := λ a b, decidable_of_iff' _ ext_iff
 
-end units
-namespace add_units
-
-variables [add_monoid α]
-
-instance [decidable_eq α] : decidable_eq (add_units α)
-| a b := decidable_of_iff' _ ext_iff
-
-attribute [to_additive add_units.decidable_eq] units.decidable_eq
-
-/-- The add_unit group inherits the addition of the add_monoid. -/
-protected def add (u₁ u₂ : add_units α) : add_units α :=
-⟨u₁.val + u₂.val, u₂.neg + u₁.neg,
-  have u₁.val + (u₂.val + u₂.neg) + u₁.neg = 0,
-    by rw [u₂.val_neg]; rw [add_zero, u₁.val_neg],
-  by simpa only [add_assoc],
-  have u₂.neg + (u₁.neg + u₁.val) + u₂.val = 0,
-    by rw [u₁.neg_val]; rw [add_zero, u₂.neg_val],
-  by simpa only [add_assoc]⟩
-
-attribute [to_additive add_units.add] units.mul
-
-/-- The additive inverse of an add_unit. -/
-protected def neg' (u : add_units α) : add_units α :=
-⟨u.neg, u.val, u.neg_val, u.val_neg⟩
-
-attribute [to_additive add_units.neg'] units.inv'
-
-end add_units
-namespace units
-
-variables [monoid α]
-
-@[to_additive] instance : has_mul (units α) := ⟨units.mul⟩
-@[to_additive] instance : has_one (units α) := ⟨⟨1, 1, mul_one 1, one_mul 1⟩⟩
-@[to_additive] instance : has_inv (units α) := ⟨units.inv'⟩
+/-- Units of a monoid form a group. -/
+@[to_additive] instance : group (units α) :=
+{ mul := λ u₁ u₂, ⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
+    by rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv],
+    by rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]⟩,
+  one := ⟨1, 1, one_mul 1, one_mul 1⟩,
+  mul_one := λ u, ext $ mul_one u,
+  one_mul := λ u, ext $ one_mul u,
+  mul_assoc := λ u₁ u₂ u₃, ext $ mul_assoc u₁ u₂ u₃,
+  inv := λ u, ⟨u.2, u.1, u.4, u.3⟩,
+  mul_left_inv := λ u, ext u.inv_val }
 
 variables (a b : units α) {c : units α}
 @[simp, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
@@ -122,11 +82,6 @@ by rw [mul_assoc, mul_inv, mul_one]
 @[simp, to_additive] lemma inv_mul_cancel_right (a : α) (b : units α) : a * ↑b⁻¹ * b = a :=
 by rw [mul_assoc, inv_mul, mul_one]
 
-@[to_additive] instance : group (units α) :=
-by refine {mul := (*), one := 1, inv := has_inv.inv, ..};
-  { intros, apply ext, simp only [coe_mul, coe_one,
-      mul_assoc, one_mul, mul_one, inv_mul] }
-
 @[to_additive] instance : inhabited (units α) := ⟨1⟩
 
 @[to_additive] instance {α} [comm_monoid α] : comm_group (units α) :=
@@ -157,7 +112,7 @@ end units
 theorem nat.units_eq_one (u : units ℕ) : u = 1 :=
 units.ext $ nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩
 
-theorem nat.add_units_eq_one (u : add_units ℕ) : u = 0 :=
+theorem nat.add_units_eq_zero (u : add_units ℕ) : u = 0 :=
 add_units.ext $ (nat.eq_zero_of_add_eq_zero u.val_neg).1
 
 /-- For `a, b` in a `comm_monoid` such that `a * b = 1`, makes a unit out of `a`. -/

src/data/complex/exponential.lean

@@ -163,7 +163,7 @@ have h₁ : ((range n).sigma (range ∘ nat.succ)).sum
     (range n).sum (λ m, (range (m + 1)).sum
     (λ k, f k (m - k))) := sum_sigma,
 have h₂ : ((range n).sigma (λ m, range (n - m))).sum (λ a : Σ (m : ℕ), ℕ, f (a.1) (a.2)) =
-    (range n).sum (λ m, sum (range (n - m)) (f m)) := sum_sigma,
+    (range n).sum (λ m, (range (n - m)).sum (f m)) := sum_sigma,
 h₁ ▸ h₂ ▸ sum_bij
 (λ a _, ⟨a.2, a.1 - a.2⟩)
 (λ a ha, have h₁ : a.1 < n := mem_range.1 (mem_sigma.1 ha).1,
@@ -223,8 +223,8 @@ have hQε0 : 0 < ε / (4 * Q),
   from div_pos ε0 (mul_pos (show (0 : α) < 4, by norm_num) (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0))),
 let ⟨M, hM⟩ := cau_seq.cauchy₂ ⟨_, ha⟩ hQε0 in
 ⟨2 * (max N M + 1), λ K hK,
-have h₁ : sum (range K) (λ m, (range (m + 1)).sum (λ k, a k * b (m - k))) =
-    sum (range K) (λ m, sum (range (K - m)) (λ n, a m * b n)),
+have h₁ : (range K).sum (λ m, (range (m + 1)).sum (λ k, a k * b (m - k))) =
+    (range K).sum (λ m, (range (K - m)).sum (λ n, a m * b n)),
   by simpa using sum_range_diag_flip K (λ m n, a m * b n),
 have h₂ : (λ i, (range (K - i)).sum (λ k, a i * b k)) = (λ i, a i * (range (K - i)).sum b),
   by simp [finset.mul_sum],
@@ -253,9 +253,9 @@ have hsumlesum : (range (max N M + 1)).sum (λ i, abv (a i) *
         (by rw two_mul; exact add_le_add (le_of_lt (mem_range.1 hmJ))
           (le_trans (le_max_left _ _) (le_of_lt (lt_add_one _)))) hK))
       (le_of_lt hKN))) (abv_nonneg abv _)),
-have hsumltP : sum (range (max N M + 1)) (λ n, abv (a n)) < P :=
-  calc sum (range (max N M + 1)) (λ n, abv (a n))
-      = abs (sum (range (max N M + 1)) (λ n, abv (a n))) :
+have hsumltP : (range (max N M + 1)).sum (λ n, abv (a n)) < P :=
+  calc (range (max N M + 1)).sum (λ n, abv (a n))
+      = abs ((range (max N M + 1)).sum (λ n, abv (a n))) :
   eq.symm (abs_of_nonneg (sum_nonneg (λ x h, abv_nonneg abv (a x))))
   ... < P : hP (max N M + 1),
 begin
@@ -268,9 +268,9 @@ begin
   refine add_lt_add (lt_of_le_of_lt hsumlesum
     (by rw [← sum_mul, mul_comm]; exact (mul_lt_mul_left hPε0).mpr hsumltP)) _,
   rw sum_range_sub_sum_range (le_of_lt hNMK),
-  exact calc sum ((range K).filter (λ k, max N M + 1 ≤ k))
-      (λ i, abv (a i) * abv (sum (range (K - i)) b - sum (range K) b))
-      ≤ sum ((range K).filter (λ k, max N M + 1 ≤ k)) (λ i, abv (a i) * (2 * Q)) :
+  exact calc ((range K).filter (λ k, max N M + 1 ≤ k)).sum
+      (λ i, abv (a i) * abv ((range (K - i)).sum b - (range K).sum b))
+      ≤ ((range K).filter (λ k, max N M + 1 ≤ k)).sum (λ i, abv (a i) * (2 * Q)) :
     sum_le_sum (λ n hn, begin
       refine mul_le_mul_of_nonneg_left _ (abv_nonneg _ _),
       rw sub_eq_add_neg,
@@ -892,7 +892,7 @@ end real
 namespace complex
 
 lemma sum_div_fact_le {α : Type*} [discrete_linear_ordered_field α] (n j : ℕ) (hn : 0 < n) :
-  (sum (filter (λ k, n ≤ k) (range j)) (λ m : ℕ, (1 / m.fact : α))) ≤ n.succ * (n.fact * n)⁻¹ :=
+  (filter (λ k, n ≤ k) (range j)).sum (λ m : ℕ, (1 / m.fact : α)) ≤ n.succ * (n.fact * n)⁻¹ :=
 calc (filter (λ k, n ≤ k) (range j)).sum (λ m : ℕ, (1 / m.fact : α))
     = (range (j - n)).sum (λ m, 1 / (m + n).fact) :
   sum_bij (λ m _, m - n)
@@ -945,8 +945,8 @@ begin
   exact calc abs (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (x ^ m / m.fact : ℂ)))
       = abs (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (x ^ n * (x ^ (m - n) / m.fact) : ℂ))) :
     congr_arg abs (sum_congr rfl (λ m hm, by rw [← mul_div_assoc, ← pow_add, nat.add_sub_cancel']; simp at hm; tauto))
-  ... ≤ sum (filter (λ k, n ≤ k) (range j)) (λ m, abs (x ^ n * (_ / m.fact))) : abv_sum_le_sum_abv _ _
-  ... ≤ sum (filter (λ k, n ≤ k) (range j)) (λ m, abs x ^ n * (1 / m.fact)) :
+  ... ≤ (filter (λ k, n ≤ k) (range j)).sum (λ m, abs (x ^ n * (_ / m.fact))) : abv_sum_le_sum_abv _ _
+  ... ≤ (filter (λ k, n ≤ k) (range j)).sum (λ m, abs x ^ n * (1 / m.fact)) :
     begin
       refine sum_le_sum (λ m hm, _),
       rw [abs_mul, abv_pow abs, abs_div, abs_cast_nat],

src/data/polynomial.lean

@@ -189,7 +189,7 @@ lemma coeff_mul (p q : polynomial α) (n : ℕ) :
 have hite : ∀ a : ℕ × ℕ, ite (a.1 + a.2 = n) (coeff p (a.fst) * coeff q (a.snd)) 0 ≠ 0
     → a.1 + a.2 = n, from λ a ha, by_contradiction
   (λ h, absurd (eq.refl (0 : α)) (by rwa if_neg h at ha)),
-calc coeff (p * q) n = sum (p.support) (λ a, sum (q.support)
+calc coeff (p * q) n = p.support.sum (λ a, q.support.sum
     (λ b, ite (a + b = n) (coeff p a * coeff q b) 0)) :
   by simp only [mul_def, coeff_sum, coeff_single]; refl
 ... = (p.support.product q.support).sum
@@ -718,7 +718,7 @@ lemma degree_sum_le (s : finset β) (f : β → polynomial α) :
   degree (s.sum f) ≤ s.sup (λ b, degree (f b)) :=
 finset.induction_on s (by simp only [sum_empty, sup_empty, degree_zero, le_refl]) $
   assume a s has ih,
-  calc degree (sum (insert a s) f) ≤ max (degree (f a)) (degree (s.sum f)) :
+  calc degree ((insert a s).sum f) ≤ max (degree (f a)) (degree (s.sum f)) :
     by rw sum_insert has; exact degree_add_le _ _
   ... ≤ _ : by rw [sup_insert, with_bot.sup_eq_max]; exact max_le_max (le_refl _) ih
 

src/linear_algebra/nonsingular_inverse.lean

@@ -187,7 +187,7 @@ end
 
 /-- Use linearity of `cramer` to take it out of a summation. -/
 lemma sum_cramer {β} (s : finset β) (f : β → n → α) :
-  s.sum (λ x, cramer α A (f x)) = cramer α A (sum s f) :=
+  s.sum (λ x, cramer α A (f x)) = cramer α A (s.sum f) :=
 (linear_map.map_sum (cramer α A)).symm
 
 /-- Use linearity of `cramer` and vector evaluation to take `cramer A _ i` out of a summation. -/
@@ -265,10 +265,10 @@ begin
   ext i j,
   rw [mul_val, smul_val, one_val, mul_ite],
   calc
-    sum univ (λ (k : n), A i k * adjugate A k j)
-        = sum univ (λ (k : n), cramer α A (λ j, if k = j then A i k else 0) j)
+    univ.sum (λ (k : n), A i k * adjugate A k j)
+        = univ.sum (λ (k : n), cramer α A (λ j, if k = j then A i k else 0) j)
       : by {congr, ext k, apply mul_adjugate_val A i j k}
-    ... = cramer α A (λ j, sum univ (λ (k : n), if k = j then A i k else 0)) j
+    ... = cramer α A (λ j, univ.sum (λ (k : n), if k = j then A i k else 0)) j
       : sum_cramer_apply A univ (λ (j k : n), if k = j then A i k else 0) j
     ... = cramer α A (A i) j : by { rw [cramer_apply], congr, ext,
       rw [sum_ite_eq' univ x (A i), if_pos (mem_univ _)] }

src/measure_theory/bochner_integration.lean

@@ -325,20 +325,20 @@ by rw [bintegral_eq_integral' hf h_pos, ← lintegral_eq_integral]
 
 lemma bintegral_add {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) :
   bintegral (f + g) = bintegral f + bintegral g :=
-calc bintegral (f + g) = sum (pair f g).range
+calc bintegral (f + g) = (pair f g).range.sum
        (λx, ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • (x.fst + x.snd)) :
 begin
   rw [add_eq_map₂, map_bintegral (pair f g)],
   { exact integrable_pair hf hg },
   { simp only [add_zero, prod.fst_zero, prod.snd_zero] }
 end
-... = sum (pair f g).range
+... = (pair f g).range.sum
         (λx, ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.fst +
              ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.snd) :
   finset.sum_congr rfl $ assume a ha, smul_add _ _ _
-... = sum (simple_func.range (pair f g))
+... = (simple_func.range (pair f g)).sum
         (λ (x : β × β), ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.fst) +
-      sum (simple_func.range (pair f g))
+      (simple_func.range (pair f g)).sum
         (λ (x : β × β), ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.snd) :
   by rw finset.sum_add_distrib
 ... = ((pair f g).map prod.fst).bintegral + ((pair f g).map prod.snd).bintegral :
@@ -368,9 +368,9 @@ end
 
 lemma bintegral_smul (r : ℝ) {f : α →ₛ β} (hf : integrable f) :
   bintegral (r • f) = r • bintegral f :=
-calc bintegral (r • f) = sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • r • x) :
+calc bintegral (r • f) = f.range.sum (λx, ennreal.to_real (volume (f ⁻¹' {x})) • r • x) :
   by rw [smul_eq_map r f, map_bintegral f _ hf (smul_zero _)]
-... = (f.range).sum (λ (x : β), ((ennreal.to_real (volume (f ⁻¹' {x}))) * r) • x) :
+... = f.range.sum (λ (x : β), ((ennreal.to_real (volume (f ⁻¹' {x}))) * r) • x) :
   finset.sum_congr rfl $ λb hb, by apply smul_smul
 ... = r • bintegral f :
 begin
@@ -384,10 +384,10 @@ lemma norm_bintegral_le_bintegral_norm (f : α →ₛ β) (hf : integrable f) :
 begin
   rw map_bintegral f norm hf norm_zero,
   rw bintegral,
-  calc ∥sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • x)∥ ≤
-       sum f.range (λx, ∥ennreal.to_real (volume (f ⁻¹' {x})) • x∥) :
+  calc ∥f.range.sum (λx, ennreal.to_real (volume (f ⁻¹' {x})) • x)∥ ≤
+       f.range.sum (λx, ∥ennreal.to_real (volume (f ⁻¹' {x})) • x∥) :
     norm_sum_le _ _
-    ... = sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • ∥x∥) :
+    ... = f.range.sum (λx, ennreal.to_real (volume (f ⁻¹' {x})) • ∥x∥) :
     begin
       refine finset.sum_congr rfl (λb hb, _),
       rw [norm_smul, smul_eq_mul, real.norm_eq_abs, abs_of_nonneg to_real_nonneg]

src/measure_theory/measure_space.lean

@@ -371,7 +371,7 @@ begin
     ennreal.tsum_eq_supr_nat],
   refine supr_le (λ n, _),
   cases n, {apply zero_le _},
-  suffices : sum (finset.range n.succ) (λ i, μ (disjointed s i)) = μ (s n),
+  suffices : (finset.range n.succ).sum (λ i, μ (disjointed s i)) = μ (s n),
   { rw this, exact le_supr _ n },
   rw [← Union_disjointed_of_mono hs, measure_Union, tsum_eq_sum],
   { apply sum_congr rfl, intros i hi,

src/tactic/transport.lean

@@ -13,7 +13,9 @@ do
     decl ← get_decl src,
     (decl.type.list_names_with_prefix pre).mfold () (λ n _, transport_with_prefix_fun_aux n),
     (decl.value.list_names_with_prefix pre).mfold () (λ n _, transport_with_prefix_fun_aux n),
-    add_decl (decl.update_with_fun (name.map_prefix f) tgt),
+    is_protected ← is_protected_decl src,
+    let decl := decl.update_with_fun (name.map_prefix f) tgt,
+    if is_protected then add_protected_decl decl else add_decl decl,
     attrs.mmap' (λ n, copy_attribute n src tgt)
 
 meta def transport_with_prefix_fun (f : name → option name) (src tgt : name) (attrs : list name) :

src/topology/algebra/infinite_sum.lean

@@ -648,7 +648,7 @@ lemma cauchy_seq_of_edist_le_of_summable [emetric_space α] {f : ℕ → α} (d
 begin
   refine emetric.cauchy_seq_iff_nnreal.2 (λ ε εpos, _),
   -- Actually we need partial sums of `d` to be a Cauchy sequence
-  replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
+  replace hd : cauchy_seq (λ (n : ℕ), (range n).sum d) :=
     let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ H.tendsto_sum_nat,
   -- Now we take the same `N` as in one of the definitions of a Cauchy sequence
   refine (metric.cauchy_seq_iff'.1 hd ε (nnreal.coe_pos.2 εpos)).imp (λ N hN n hn, _),
@@ -670,7 +670,7 @@ lemma cauchy_seq_of_dist_le_of_summable [metric_space α] {f : ℕ → α} (d :
   (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
 begin
   refine metric.cauchy_seq_iff'.2 (λε εpos, _),
-  replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
+  replace hd : cauchy_seq (λ (n : ℕ), (range n).sum d) :=
     let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ H.tendsto_sum_nat,
   refine (metric.cauchy_seq_iff'.1 hd ε εpos).imp (λ N hN n hn, _),
   have hsum := hN n hn,