refactor(algebra/big_operators): introduce notation for finset.prod a…

…nd finset.sum (#2582)

I have not gone through all of mathlib to use this notation everywhere. I think we can maybe transition naturally.

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Reid Barton <rwbarton@gmail.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/algebra/category/Group/biproducts.lean

@@ -14,6 +14,8 @@ import algebra.pi_instances
 open category_theory
 open category_theory.limits
 
+open_locale big_operators
+
 universe u
 
 namespace AddCommGroup
@@ -100,7 +102,7 @@ to any cocone over that family.
 -/
 def desc (s : cocone F) :
   AddCommGroup.of (Π j, F.obj j) ⟶ s.X :=
-{ to_fun := λ f, finset.univ.sum (λ j : J, s.ι.app j (f j)),
+{ to_fun := λ f, ∑ j, s.ι.app j (f j),
   map_zero' :=
   begin
     conv_lhs { apply_congr, skip, simp [@pi.zero_apply _ (λ j, F.obj j) x _], },
@@ -113,7 +115,7 @@ def desc (s : cocone F) :
   end, }
 
 @[simp] lemma desc_apply (s : cocone F) (f : Π j, F.obj j) :
-  (desc F s) f = finset.univ.sum (λ j : J, s.ι.app j (f j)) := rfl
+  (desc F s) f = ∑ j, s.ι.app j (f j) := rfl
 
 variables [decidable_eq J]
 

src/algebra/geom_sum.lean

@@ -13,12 +13,14 @@ variable {α : Type u}
 
 open finset
 
+open_locale big_operators
+
 /-- Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i$. -/
 def geom_series [semiring α] (x : α) (n : ℕ) :=
-(range n).sum (λ i, x ^ i)
+∑ i in range n, x ^ i
 
 theorem geom_series_def [semiring α] (x : α) (n : ℕ) :
-  geom_series x n = (range n).sum (λ i, x ^ i) := rfl
+  geom_series x n = ∑ i in range n, x ^ i := rfl
 
 @[simp] theorem geom_series_zero [semiring α] (x : α) :
   geom_series x 0 = 0 := rfl
@@ -29,10 +31,10 @@ by { rw [geom_series_def, sum_range_one, pow_zero] }
 
 /-- Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i y^{n-1-i}$. -/
 def geom_series₂ [semiring α] (x y : α) (n : ℕ) :=
-(range n).sum (λ i, x ^ i * (y ^ (n - 1 - i)))
+∑ i in range n, x ^ i * (y ^ (n - 1 - i))
 
 theorem geom_series₂_def [semiring α] (x y : α) (n : ℕ) :
-  geom_series₂ x y n = (range n).sum (λ i, x ^ i * y ^ (n - 1 - i)) := rfl
+  geom_series₂ x y n = ∑ i in range n, x ^ i * y ^ (n - 1 - i) := rfl
 
 @[simp] theorem geom_series₂_zero [semiring α] (x y : α) :
   geom_series₂ x y 0 = 0 := rfl
@@ -51,22 +53,22 @@ protected theorem commute.geom_sum₂_mul_add [semiring α] {x y : α} (h : comm
   (geom_series₂ (x + y) y n) * x + y ^ n = (x + y) ^ n :=
 begin
   let f := λ (m i : ℕ), (x + y) ^ i * y ^ (m - 1 - i),
-  change ((range n).sum (f n)) * x + y ^ n = (x + y) ^ n,
+  change (∑ i in range n, (f n) i) * x + y ^ n = (x + y) ^ n,
   induction n with n ih,
   { rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero] },
-  { have f_last : f n.succ n = (x + y) ^ n :=
+  { have f_last : f (n + 1) n = (x + y) ^ n :=
      by { dsimp [f],
           rw [nat.sub_sub, nat.add_comm, nat.sub_self, pow_zero, mul_one] },
-    have f_succ : ∀ i, i ∈ range n → f n.succ i = y * f n i :=
+    have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i :=
       λ i hi, by {
         dsimp [f],
         have : commute y ((x + y) ^ i) :=
          (h.symm.add_right (commute.refl y)).pow_right i,
         rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)],
         congr' 2,
-        rw [nat.succ_eq_add_one, nat.add_sub_cancel, nat.sub_sub, add_comm 1 i],
-        have := nat.add_sub_of_le (mem_range.mp hi),
-        rw [add_comm, nat.succ_eq_add_one] at this,
+        rw [nat.add_sub_cancel, nat.sub_sub, add_comm 1 i],
+        have : i + 1 + (n - (i + 1)) = n := nat.add_sub_of_le (mem_range.mp hi),
+        rw [add_comm (i + 1)] at this,
         rw [← this, nat.add_sub_cancel, add_comm i 1, ← add_assoc,
             nat.add_sub_cancel] },
     rw [pow_succ (x + y), add_mul, sum_range_succ, f_last, add_mul, add_assoc],

src/analysis/specific_limits.lean

@@ -14,6 +14,8 @@ open_locale classical topological_space
 
 open classical function filter finset metric
 
+open_locale big_operators
+
 variables {α : Type*} {β : Type*} {ι : Type*}
 
 lemma tendsto_norm_at_top_at_top : tendsto (norm : ℝ → ℝ) at_top at_top :=
@@ -116,7 +118,7 @@ lemma tendsto_inv_at_top_zero [discrete_linear_ordered_field α] [topological_sp
 tendsto_le_right inf_le_left tendsto_inv_at_top_zero'
 
 lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
-  (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (𝓝 r)) → summable f
+  (∃r, tendsto (λn, (∑ i in range n, abs (f i))) at_top (𝓝 r)) → summable f
 | ⟨r, hr⟩ :=
   begin
     refine summable_of_summable_norm ⟨r, (has_sum_iff_tendsto_nat_of_nonneg _ _).2 _⟩,
@@ -203,7 +205,7 @@ have r + -1 ≠ 0,
   by rw [←sub_eq_add_neg, ne, sub_eq_iff_eq_add]; simp; assumption,
 have tendsto (λn, (r ^ n - 1) * (r - 1)⁻¹) at_top (𝓝 ((0 - 1) * (r - 1)⁻¹)),
   from ((tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds,
-have (λ n, (range n).sum (λ i, r ^ i)) = (λ n, geom_series r n) := rfl,
+have (λ n, (∑ i in range n, r ^ i)) = (λ n, geom_series r n) := rfl,
 (has_sum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr $
   by simp [neg_inv, geom_sum, div_eq_mul_inv, *] at *
 
@@ -264,8 +266,8 @@ begin
     refine λ a ha, (ennreal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp
       (λ n hn, lt_of_lt_of_le hn _),
     have : ∀ k:ℕ, 1 ≤ r^k, by simpa using canonically_ordered_semiring.pow_le_pow_of_le_left hr,
-    calc (n:ennreal) = (range n).sum (λ _, 1) : by rw [sum_const, add_monoid.smul_one, card_range]
-    ... ≤ (range n).sum (pow r) : sum_le_sum (λ k _, this k) }
+    calc (n:ennreal) = (∑ i in range n, 1) : by rw [sum_const, add_monoid.smul_one, card_range]
+    ... ≤ ∑ i in range n, r ^ i : sum_le_sum (λ k _, this k) }
 end
 
 /-- For any positive `ε`, define on an encodable type a positive sequence with sum less than `ε` -/
@@ -435,11 +437,11 @@ section summable_le_geometric
 variables [normed_group α] {r C : ℝ} {f : ℕ → α}
 
 lemma dist_partial_sum_le_of_le_geometric (hf : ∀n, ∥f n∥ ≤ C * r^n) (n : ℕ) :
-  dist ((finset.range n).sum f) ((finset.range (n+1)).sum f) ≤ C * r ^ n :=
+  dist (∑ i in range n, f i) (∑ i in range (n+1), f i) ≤ C * r ^ n :=
 begin
   rw [sum_range_succ, dist_eq_norm, ← norm_neg],
   convert hf n,
-  abel
+  rw [neg_sub, add_sub_cancel]
 end
 
 /-- If `∥f n∥ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` form a

src/data/complex/exponential.lean

@@ -850,7 +850,7 @@ calc x + 1 ≤ lim (⟨(λ n : ℕ, ((exp' x) n).re), is_cau_seq_re (exp' x)⟩
           add_re, add_re, h₁, h₂, add_assoc,
           ← @sum_hom _ _ _ _ _ _ _ complex.re
             (is_add_group_hom.to_is_add_monoid_hom _)],
-        refine le_add_of_nonneg_of_le (sum_nonneg (λ m hm, _)) (le_refl _), dsimp [-nat.fact_succ],
+        refine le_add_of_nonneg_of_le (sum_nonneg (λ m hm, _)) (le_refl _),
         rw [← of_real_pow, ← of_real_nat_cast, ← of_real_div, of_real_re],
         exact div_nonneg (pow_nonneg hx _) (nat.cast_pos.2 (nat.fact_pos _)),
       end⟩)

src/data/mv_polynomial.lean

@@ -340,13 +340,12 @@ begin
     rw [← finset.sum_sdiff (finset.filter_subset _), finset.sum_eq_zero, zero_add], swap,
     { intros x hx,
       rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter), not_and] at hx,
-      rw if_neg,
-      exact hx.2 hx.1 },
+      simp only [if_neg (hx.2 hx.1)] },
     { apply finset.sum_bij, swap 5,
       { intros x hx, exact (x.1, x.2) },
       { intros x hx, rw [finset.mem_filter, finset.mem_sigma] at hx,
         simpa [finset.mem_filter, mem_antidiagonal_support] using hx.symm },
-      { intros x hx, rw finset.mem_filter at hx, rw if_pos hx.2 },
+      { intros x hx, rw finset.mem_filter at hx, simp only [if_pos hx.2], },
       { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl, simpa using and.intro },
       { rintros ⟨i,j⟩ hij, refine ⟨⟨i,j⟩, _, _⟩, { apply_instance },
         { rw [finset.mem_filter, mem_antidiagonal_support] at hij,

src/data/nat/choose.lean

@@ -7,6 +7,8 @@ import algebra.commute
 
 open nat
 
+open_locale big_operators
+
 lemma nat.prime.dvd_choose {p k : ℕ} (hk : 0 < k) (hkp : k < p) (hp : prime p) : p ∣ choose p k :=
 have h₁ : p ∣ fact p, from hp.dvd_fact.2 (le_refl _),
 have h₂ : ¬p ∣ fact k, from mt hp.dvd_fact.1 (not_le_of_gt hkp),
@@ -58,10 +60,10 @@ variables {α : Type*}
 
 /-- A version of the binomial theorem for noncommutative semirings. -/
 theorem commute.add_pow [semiring α] {x y : α} (h : commute x y) (n : ℕ) :
-  (x + y) ^ n = (range (succ n)).sum (λ m, x ^ m * y ^ (n - m) * choose n m) :=
+  (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=
 begin
-  let t : ℕ → ℕ → α := λ n i, x ^ i * (y ^ (n - i)) * (choose n i),
-  change (x + y) ^ n = (range n.succ).sum (t n),
+  let t : ℕ → ℕ → α := λ n m, x ^ m * (y ^ (n - m)) * (choose n m),
+  change (x + y) ^ n = ∑ m in range (n + 1), t n m,
   have h_first : ∀ n, t n 0 = y ^ n :=
     λ n, by { dsimp [t], rw[choose_zero_right, nat.cast_one, mul_one, one_mul] },
   have h_last : ∀ n, t n n.succ = 0 :=
@@ -94,7 +96,7 @@ end
 
 /-- The binomial theorem-/
 theorem add_pow [comm_semiring α] (x y : α) (n : ℕ) :
-  (x + y) ^ n = (range (succ n)).sum (λ m, x ^ m * y ^ (n - m) * choose n m) :=
+  (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=
 (commute.all x y).add_pow n
 
 end binomial

src/group_theory/order_of_element.lean

@@ -472,7 +472,7 @@ lt_irrefl c $
       have hmc : m ∣ c, by simp at hm; tauto,
       (imp_iff_not_or.1 (card_order_of_eq_totient_aux₁ hn hmc)).elim
         (λ h, by simp [nat.le_zero_iff.1 (le_of_not_gt h), nat.zero_le])
-        (by simp [le_refl] {contextual := tt}))
+        (by { intro h, rw h, apply le_refl }))
   ... < φ d + (((range c.succ).filter (∣ c)).erase d).sum φ :
     lt_add_of_pos_left _ (totient_pos (nat.pos_of_ne_zero
       (λ h, nat.pos_iff_ne_zero.1 hc0 (eq_zero_of_zero_dvd $ h ▸ hd))))

src/ring_theory/power_series.lean

@@ -201,7 +201,7 @@ begin
   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, exact ⟨(k, l+j), (l, j)⟩ },
   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H,
     simp only [finset.mem_sigma, mem_antidiagonal_support] at H ⊢, finish },
-  { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, rw mul_assoc },
+  { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, simp only [mul_assoc] },
   { rintros ⟨⟨a,b⟩, ⟨c,d⟩⟩ ⟨⟨i,j⟩, ⟨k,l⟩⟩ H₁ H₂,
     simp only [finset.mem_sigma, mem_antidiagonal_support,
       and_imp, prod.mk.inj_iff, add_comm, heq_iff_eq] at H₁ H₂ ⊢,