feat(algebra/big_operators/basic): edit finset.sum/prod_range_succ (#…

…6676) - Change the RHS of the statement of `sum_range_succ` from `f n + ∑ x in range n, f x` to `∑ x in range n, f x + f n` - Change the RHS of the statement of `prod_range_succ` from `f n * ∑ x in range n, f x` to `∑ x in range n, f x * f n` The old versions of those lemmas are now called `sum_range_succ_comm` and `prod_range_succ_comm`, respectively. See [this conversation](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/break.20off.20last.20term.20of.20summation/near/229634503) on Zulip. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
leanprover-community · Apr 7, 2021 · 08aff2c · 08aff2c
1 parent d76b649
commit 08aff2c
Show file tree

Hide file tree

Showing 22 changed files with 96 additions and 104 deletions.
diff --git a/archive/imo/imo2013_q1.lean b/archive/imo/imo2013_q1.lean
@@ -75,10 +75,9 @@ begin
                                                              ring }
     ... = (1 + 1 / (2 * t + 2^pk.succ)) *
           (1 + (2 ^ pk - 1) / t_succ)                 : by norm_cast
-    ... = (1 + 1 / ↑(m pk)) *
-          ∏ (i : ℕ) in finset.range pk, (1 + 1 / m i) : by rw [hpm, prod_lemma, ←hmpk]
-    ... = ∏ (i : ℕ) in finset.range pk.succ,
-                                        (1 + 1 / m i) : (finset.prod_range_succ _ pk).symm },
+    ... = (∏ i in finset.range pk, (1 + 1 / m i)) *
+          (1 + 1 / (m pk))                            : by rw [prod_lemma, hpm, ←hmpk, mul_comm]
+    ... = ∏ i in finset.range pk.succ, (1 + 1 / m i)  : by rw ← finset.prod_range_succ _ pk },
   { -- odd case
     let t_succ : ℕ+ := ⟨t + 1, t.succ_pos⟩,
     obtain ⟨pm, hpm⟩ := hpk t_succ,
@@ -97,8 +96,7 @@ begin
                                                              ring }
     ... = (1 + 1 / (2 * t + 1)) *
           (1 + (2^pk - 1) / t_succ)                   : by norm_cast
-    ... = (1 + 1 / ↑(m pk)) *
-          ∏ (i : ℕ) in finset.range pk, (1 + 1 / m i) : by rw [hpm, prod_lemma, ←hmpk]
-    ... = ∏ (i : ℕ) in finset.range pk.succ,
-                                        (1 + 1 / m i) : (finset.prod_range_succ _ pk).symm }
+    ... = (∏ i in finset.range pk, (1 + 1 / m i)) *
+          (1 + 1 / ↑(m pk))                           : by rw [prod_lemma, hpm, ←hmpk, mul_comm]
+    ... = ∏ i in finset.range pk.succ, (1 + 1 / m i)  : by rw ← finset.prod_range_succ _ pk }
 end
diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
@@ -702,41 +702,49 @@ begin
   exact prod_congr rfl hfg
 end
 
-lemma sum_range_succ {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) :
-  (∑ x in range (n + 1), f x) = f n + (∑ x in range n, f x) :=
+lemma sum_range_succ_comm {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) :
+  ∑ x in range (n + 1), f x = f n + ∑ x in range n, f x :=
 by rw [range_succ, sum_insert not_mem_range_self]
 
+lemma sum_range_succ {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) :
+  ∑ x in range (n + 1), f x = ∑ x in range n, f x + f n :=
+by simp only [add_comm, sum_range_succ_comm]
+
 @[to_additive]
-lemma prod_range_succ (f : ℕ → β) (n : ℕ) :
-  (∏ x in range (n + 1), f x) = f n * (∏ x in range n, f x) :=
+lemma prod_range_succ_comm (f : ℕ → β) (n : ℕ) :
+  ∏ x in range (n + 1), f x = f n * ∏ x in range n, f x :=
 by rw [range_succ, prod_insert not_mem_range_self]
 
+@[to_additive]
+lemma prod_range_succ (f : ℕ → β) (n : ℕ) :
+  ∏ x in range (n + 1), f x = (∏ x in range n, f x) * f n :=
+by simp only [mul_comm, prod_range_succ_comm]
+
 lemma prod_range_succ' (f : ℕ → β) :
   ∀ n : ℕ, (∏ k in range (n + 1), f k) = (∏ k in range n, f (k+1)) * f 0
-| 0       := (prod_range_succ _ _).trans $ mul_comm _ _
-| (n + 1) := by rw [prod_range_succ (λ m, f (nat.succ m)), mul_assoc, ← prod_range_succ'];
-                 exact prod_range_succ _ _
+| 0       := prod_range_succ _ _
+| (n + 1) := by rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ', prod_range_succ]
 
-lemma prod_range_add (f : ℕ → β) (n : ℕ) (m : ℕ) :
-  (∏ x in range (n + m), f x) =
+lemma prod_range_add (f : ℕ → β) (n m : ℕ) :
+  ∏ x in range (n + m), f x =
   (∏ x in range n, f x) * (∏ x in range m, f (n + x)) :=
 begin
   induction m with m hm,
   { simp },
-  { rw [nat.add_succ, finset.prod_range_succ, hm, finset.prod_range_succ, mul_left_comm _ _ _] },
+  { rw [nat.add_succ, prod_range_succ, hm, prod_range_succ, mul_assoc], },
 end
 
 @[to_additive]
 lemma prod_range_zero (f : ℕ → β) :
- (∏ k in range 0, f k) = 1 :=
+  ∏ k in range 0, f k = 1 :=
 by rw [range_zero, prod_empty]
 
 lemma prod_range_one (f : ℕ → β) :
-  (∏ k in range 1, f k) = f 0 :=
+  ∏ k in range 1, f k = f 0 :=
 by { rw [range_one], apply @prod_singleton ℕ β 0 f }
 
 lemma sum_range_one {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) :
-  (∑ k in range 1, f k) = f 0 :=
+  ∑ k in range 1, f k = f 0 :=
 @prod_range_one (multiplicative δ) _ f
 
 attribute [to_additive finset.sum_range_one] prod_range_one
@@ -870,17 +878,17 @@ lemma pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ k in range n, b
 | (n+1) := by simp
 
 lemma prod_pow (s : finset α) (n : ℕ) (f : α → β) :
-  (∏ x in s, f x ^ n) = (∏ x in s, f x) ^ n :=
+  ∏ x in s, f x ^ n = (∏ x in s, f x) ^ n :=
 by haveI := classical.dec_eq α; exact
 finset.induction_on s (by simp) (by simp [mul_pow] {contextual := tt})
 
 -- `to_additive` fails on this lemma, so we prove it manually below
 lemma prod_flip {n : ℕ} (f : ℕ → β) :
-  (∏ r in range (n + 1), f (n - r)) = (∏ k in range (n + 1), f k) :=
+  ∏ r in range (n + 1), f (n - r) = ∏ k in range (n + 1), f k :=
 begin
   induction n with n ih,
   { rw [prod_range_one, prod_range_one] },
-  { rw [prod_range_succ', prod_range_succ _ (nat.succ n), mul_comm],
+  { rw [prod_range_succ', prod_range_succ _ (nat.succ n)],
     simp [← ih] }
 end
 

diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean
@@ -120,7 +120,7 @@ theorem add_pow_char_of_commute [semiring R] {p : ℕ} [fact p.prime]
   [char_p R p] (x y : R) (h : commute x y) :
   (x + y)^p = x^p + y^p :=
 begin
-  rw [commute.add_pow h, finset.sum_range_succ, nat.sub_self, pow_zero, nat.choose_self],
+  rw [commute.add_pow h, finset.sum_range_succ_comm, nat.sub_self, pow_zero, nat.choose_self],
   rw [nat.cast_one, mul_one, mul_one], congr' 1,
   convert finset.sum_eq_single 0 _ _,
   { simp only [mul_one, one_mul, nat.choose_zero_right, nat.sub_zero, nat.cast_one, pow_zero] },

diff --git a/src/algebra/geom_sum.lean b/src/algebra/geom_sum.lean
@@ -111,11 +111,10 @@ begin
         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],
-    rw [(((commute.refl x).add_right h).pow_right n).eq],
+    rw [pow_succ (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc],
+    rw (((commute.refl x).add_right h).pow_right n).eq,
     congr' 1,
-    rw[sum_congr rfl f_succ, ← mul_sum, pow_succ y],
-    rw[mul_assoc, ← mul_add y, ih] }
+    rw [sum_congr rfl f_succ, ← mul_sum, pow_succ y, mul_assoc, ← mul_add y, ih] }
 end
 
 theorem geom_sum₂_self {α : Type*} [comm_ring α] (x : α) (n : ℕ) :
@@ -233,13 +232,10 @@ protected theorem commute.geom_sum₂_succ_eq {α : Type u} [ring α] {x y : α}
   (h : commute x y) {n : ℕ} :
   geom_sum₂ x y (n + 1) = x ^ n + y * (geom_sum₂ x y n) :=
 begin
-  dunfold geom_sum₂,
-  rw [mul_sum, sum_range_succ _ n, nat.add_succ_sub_one, add_zero, nat.sub_self, pow_zero, mul_one],
-  apply congr_arg (has_add.add (x ^ n)),
-  apply finset.sum_congr rfl,
-  intros i hi,
-  rw [←mul_assoc, (h.symm.pow_right i).eq, mul_assoc, ←pow_succ],
-  suffices : n - 1 - i + 1 = n - i , { rw this },
+  simp_rw [geom_sum₂, mul_sum, sum_range_succ_comm, nat.add_succ_sub_one, add_zero, nat.sub_self,
+    pow_zero, mul_one, add_right_inj, ←mul_assoc, (h.symm.pow_right _).eq, mul_assoc, ←pow_succ],
+  refine sum_congr rfl (λ i hi, _),
+  suffices : n - 1 - i + 1 = n - i, { rw this },
   cases n,
   { exact absurd (list.mem_range.mp hi) i.not_lt_zero },
   { rw [nat.sub_add_eq_add_sub (nat.le_pred_of_lt (list.mem_range.mp hi)),

diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
@@ -446,7 +446,7 @@ begin
     have hA : has_sum (λ n, A (n + 2)) (f y.1 - f y.2 - (p 1 (λ _, y.1 - y.2))),
     { convert (has_sum_nat_add_iff' 2).2 ((hf.has_sum_sub hy.1).sub (hf.has_sum_sub hy.2)),
       rw [finset.sum_range_succ, finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self,
-        add_zero, ← subsingleton.pi_single_eq (0 : fin 1) (y.1 - x), pi.single,
+        zero_add, ← subsingleton.pi_single_eq (0 : fin 1) (y.1 - x), pi.single,
         ← subsingleton.pi_single_eq (0 : fin 1) (y.2 - x), pi.single, ← (p 1).map_sub, ← pi.single,
         subsingleton.pi_single_eq, sub_sub_sub_cancel_right] },
     rw [emetric.mem_ball, edist_eq_coe_nnnorm_sub, ennreal.coe_lt_coe] at hy',

diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean
@@ -1726,8 +1726,7 @@ begin
       nat.cast_one] },
   { simp only [function.iterate_succ_apply', ihk, finset.prod_range_succ],
     ext x,
-    rw [((has_deriv_at_pow (n - k) x).const_mul _).deriv, nat.cast_mul, mul_left_comm, mul_assoc,
-      nat.succ_eq_add_one, nat.sub_sub] }
+    rw [((has_deriv_at_pow (n - k) x).const_mul _).deriv, nat.cast_mul, mul_assoc, nat.sub_sub] }
 end
 
 lemma iter_deriv_pow {k : ℕ} :
@@ -1828,7 +1827,7 @@ begin
   induction k with k ihk generalizing x hx,
   { simp only [one_mul, finset.prod_range_zero, function.iterate_zero_apply, int.coe_nat_zero,
       sub_zero, int.cast_one] },
-  { rw [function.iterate_succ', finset.prod_range_succ, int.cast_mul, mul_assoc, mul_left_comm,
+  { rw [function.iterate_succ', finset.prod_range_succ, int.cast_mul, mul_assoc,
       int.coe_nat_succ, ← sub_sub, ← ((has_deriv_at_fpow _ hx).const_mul _).deriv],
     exact filter.eventually_eq.deriv_eq (eventually.mono (mem_nhds_sets is_open_ne hx) @ihk) }
 end

diff --git a/src/analysis/normed_space/banach.lean b/src/analysis/normed_space/banach.lean
@@ -193,15 +193,14 @@ begin
     ... = 2 * C * ∥y∥ : by rw [tsum_geometric_two, mul_assoc]
     ... ≤ 2 * C * ∥y∥ + ∥y∥ : le_add_of_nonneg_right (norm_nonneg y)
     ... = (2 * C + 1) * ∥y∥ : by ring,
-  have fsumeq : ∀n:ℕ, f (∑ i in finset.range n, u i) = y - (h^[n]) y,
+  have fsumeq : ∀n:ℕ, f (∑ i in range n, u i) = y - (h^[n]) y,
   { assume n,
     induction n with n IH,
     { simp [f.map_zero] },
-    { rw [sum_range_succ, f.map_add, IH, iterate_succ'],
-      simp [u, h, sub_eq_add_neg, add_comm, add_left_comm] } },
+    { rw [sum_range_succ, f.map_add, IH, iterate_succ', sub_add] } },
   have : tendsto (λn, ∑ i in range n, u i) at_top (𝓝 x) :=
     su.has_sum.tendsto_sum_nat,
-  have L₁ : tendsto (λn, f(∑ i in range n, u i)) at_top (𝓝 (f x)) :=
+  have L₁ : tendsto (λn, f (∑ i in range n, u i)) at_top (𝓝 (f x)) :=
     (f.continuous.tendsto _).comp this,
   simp only [fsumeq] at L₁,
   have L₂ : tendsto (λn, y - (h^[n]) y) at_top (𝓝 (y - 0)),

diff --git a/src/analysis/p_series.lean b/src/analysis/p_series.lean
@@ -46,7 +46,7 @@ lemma le_sum_condensed' (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m)
 begin
   induction n with n ihn, { simp },
   suffices : (∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k) ≤ (2 ^ n) •ℕ f (2 ^ n),
-  { rw [sum_range_succ, add_comm, ← sum_Ico_consecutive],
+  { rw [sum_range_succ, ← sum_Ico_consecutive],
     exact add_le_add ihn this,
     exacts [n.one_le_two_pow, nat.pow_le_pow_of_le_right zero_lt_two n.le_succ] },
   have : ∀ k ∈ Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ f (2 ^ n) :=
@@ -59,15 +59,15 @@ lemma le_sum_condensed (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (
   (∑ k in range (2 ^ n), f k) ≤ f 0 + ∑ k in range n, (2 ^ k) •ℕ f (2 ^ k) :=
 begin
   convert add_le_add_left (le_sum_condensed' hf n) (f 0),
-  rw [← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ, sum_range_zero, add_zero]
+  rw [← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ, sum_range_zero, zero_add]
 end
 
 lemma sum_condensed_le' (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) :
   (∑ k in range n, (2 ^ k) •ℕ f (2 ^ (k + 1))) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k :=
 begin
   induction n with n ihn, { simp },
   suffices : (2 ^ n) •ℕ f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k,
-  { rw [sum_range_succ, add_comm, ← sum_Ico_consecutive],
+  { rw [sum_range_succ, ← sum_Ico_consecutive],
     exact add_le_add ihn this,
     exacts [add_le_add_right n.one_le_two_pow _,
       add_le_add_right (nat.pow_le_pow_of_le_right zero_lt_two n.le_succ) _] },

diff --git a/src/analysis/special_functions/integrals.lean b/src/analysis/special_functions/integrals.lean
@@ -196,21 +196,17 @@ theorem integral_sin_pow_odd (n : ℕ) :
 begin
   induction n with k ih,
   { norm_num },
-  rw [finset.prod_range_succ, ← mul_assoc, mul_comm (2:ℝ) ((2 * k + 2) / (2 * k + 3)),
-    mul_assoc, ← ih],
-  have h₁ : 2 * k.succ + 1 = 2 * k + 1 + 2, { ring },
-  have h₂ : (2:ℝ) * k + 1 + 1 = 2 * k + 2, { norm_cast },
-  have h₃ : (2:ℝ) * k + 1 + 2 = 2 * k + 3, { norm_cast },
-  simp [h₁, h₂, h₃, integral_sin_pow_succ_succ (2 * k + 1)],
+  rw [finset.prod_range_succ_comm, mul_left_comm, ← ih, nat.mul_succ, integral_sin_pow_succ_succ],
+  norm_cast,
 end
 
 theorem integral_sin_pow_even (n : ℕ) :
   ∫ x in 0..π, sin x ^ (2 * n) = π * ∏ i in finset.range n, (2 * i + 1) / (2 * i + 2) :=
 begin
   induction n with k ih,
   { norm_num },
-  rw [finset.prod_range_succ, ← mul_assoc, mul_comm π ((2 * k + 1) / (2 * k + 2)), mul_assoc, ← ih],
-  simp [nat.succ_eq_add_one, mul_add, mul_one, integral_sin_pow_succ_succ _],
+  rw [finset.prod_range_succ_comm, mul_left_comm, ← ih, nat.mul_succ, integral_sin_pow_succ_succ],
+  norm_cast,
 end
 
 lemma integral_sin_pow_pos (n : ℕ) : 0 < ∫ x in 0..π, sin x ^ n :=

diff --git a/src/analysis/special_functions/polynomials.lean b/src/analysis/special_functions/polynomials.lean
@@ -43,7 +43,7 @@ begin
   { simp [h] },
   { conv_lhs
     { funext,
-      rw [polynomial.eval_eq_finset_sum, sum_range_succ, add_comm] },
+      rw [polynomial.eval_eq_finset_sum, sum_range_succ] },
     exact is_equivalent.refl.add_is_o (is_o.sum $ λ i hi, is_o.const_mul_left
       (is_o.const_mul_right (λ hz, h $ leading_coeff_eq_zero.mp hz) $
         is_o_pow_pow_at_top_of_lt (mem_range.mp hi)) _) }

diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean
@@ -612,9 +612,8 @@ variables [normed_group α] {r C : ℝ} {f : ℕ → α}
 lemma dist_partial_sum_le_of_le_geometric (hf : ∀n, ∥f n∥ ≤ C * r^n) (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,
-  rw [neg_sub, add_sub_cancel]
+  rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel'],
+  exact hf n,
 end
 
 /-- If `∥f n∥ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` form a

diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
@@ -108,8 +108,7 @@ begin
   clear hk ji j,
   induction k with k' hi,
   { simp [abv_zero abv] },
-  { dsimp at *,
-    simp only [nat.succ_add, sum_range_succ, sub_eq_add_neg, add_assoc],
+  { simp only [nat.succ_add, sum_range_succ_comm, sub_eq_add_neg, add_assoc],
     refine le_trans (abv_add _ _ _) _,
     simp only [sub_eq_add_neg] at hi,
     exact add_le_add (hm _ (le_add_of_nonneg_of_le (nat.zero_le _) (le_max_left _ _))) hi },
@@ -1285,7 +1284,7 @@ calc abs (exp x - 1) = abs (exp x - ∑ m in range 1, x ^ m / m!) :
 lemma abs_exp_sub_one_sub_id_le {x : ℂ} (hx : abs x ≤ 1) :
   abs (exp x - 1 - x) ≤ (abs x)^2 :=
 calc abs (exp x - 1 - x) = abs (exp x - ∑ m in range 2, x ^ m / m!) :
-  by simp [sub_eq_add_neg, sum_range_succ, add_assoc]
+  by simp [sub_eq_add_neg, sum_range_succ_comm, add_assoc]
 ... ≤ (abs x)^2 * (nat.succ 2 * (2! * (2 : ℕ))⁻¹) :
   exp_bound hx dec_trivial
 ... ≤ (abs x)^2 * 1 :

diff --git a/src/data/nat/choose/sum.lean b/src/data/nat/choose/sum.lean
@@ -30,33 +30,33 @@ begin
   let t : ℕ → ℕ → R := λ 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] },
+    λ n, by { dsimp [t], rw [choose_zero_right, nat.cast_one, mul_one, one_mul] },
   have h_last : ∀ n, t n n.succ = 0 :=
     λ n, by { dsimp [t], rw [choose_succ_self, nat.cast_zero, mul_zero] },
-  have h_middle : ∀ (n i : ℕ), (i ∈ finset.range n.succ) →
+  have h_middle : ∀ (n i : ℕ), (i ∈ range n.succ) →
    ((t n.succ) ∘ nat.succ) i = x * (t n i) + y * (t n i.succ) :=
   begin
     intros n i h_mem,
-    have h_le : i ≤ n := nat.le_of_lt_succ (finset.mem_range.mp h_mem),
+    have h_le : i ≤ n := nat.le_of_lt_succ (mem_range.mp h_mem),
     dsimp [t],
     rw [choose_succ_succ, nat.cast_add, mul_add],
     congr' 1,
-    { rw[pow_succ x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc] },
-    { rw[← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq],
+    { rw [pow_succ x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc] },
+    { rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq],
       by_cases h_eq : i = n,
       { rw [h_eq, choose_succ_self, nat.cast_zero, mul_zero, mul_zero] },
-      { rw[succ_sub (lt_of_le_of_ne h_le h_eq)],
-        rw[pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc] } }
+      { rw [succ_sub (lt_of_le_of_ne h_le h_eq)],
+        rw [pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc] } }
   end,
   induction n with n ih,
-  { rw [pow_zero, sum_range_succ, range_zero, sum_empty, add_zero],
+  { rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add],
     dsimp [t], rw [choose_self, nat.cast_one, mul_one, mul_one] },
-  { rw[sum_range_succ', h_first],
-    rw[finset.sum_congr rfl (h_middle n), finset.sum_add_distrib, add_assoc],
-    rw[pow_succ (x + y), ih, add_mul, finset.mul_sum, finset.mul_sum],
+  { rw [sum_range_succ', h_first],
+    rw [sum_congr rfl (h_middle n), sum_add_distrib, add_assoc],
+    rw [pow_succ (x + y), ih, add_mul, mul_sum, mul_sum],
     congr' 1,
-    rw[finset.sum_range_succ', finset.sum_range_succ, h_first, h_last,
-       mul_zero, zero_add, pow_succ] }
+    rw [sum_range_succ', sum_range_succ, h_first, h_last,
+       mul_zero, add_zero, pow_succ] }
 end
 
 /-- The binomial theorem -/

diff --git a/src/data/padics/padic_norm.lean b/src/data/padics/padic_norm.lean
@@ -329,10 +329,10 @@ begin
   { exact false.elim (hn0 rfl) },
   { rw finset.sum_range_succ at hn0 ⊢,
     by_cases h : ∑ (x : ℕ) in finset.range d, F x = 0,
-    { rw [h, add_zero],
+    { rw [h, zero_add],
       exact hF d (lt_add_one _) },
-    { refine lt_of_lt_of_le _ (min_le_padic_val_rat_add p (λ h1, _) h hn0),
-      { refine lt_min (hF d (lt_add_one _)) (hd (λ i hi, _) h),
+    { refine lt_of_lt_of_le _ (min_le_padic_val_rat_add p h (λ h1, _) hn0),
+      { refine lt_min (hd (λ i hi, _) h) (hF d (lt_add_one _)),
         exact hF _ (lt_trans hi (lt_add_one _)) },
       { have h2 := hF d (lt_add_one _),
         rw h1 at h2,

diff --git a/src/data/polynomial/iterated_deriv.lean b/src/data/polynomial/iterated_deriv.lean
@@ -144,19 +144,18 @@ begin
 end
 
 lemma coeff_iterated_deriv_as_prod_range :
-  ∀ m : ℕ, (iterated_deriv f k).coeff m = f.coeff (m + k) * (∏ i in finset.range k, ↑(m + k - i)) :=
+  ∀ m : ℕ, (iterated_deriv f k).coeff m = f.coeff (m + k) * (∏ i in range k, ↑(m + k - i)) :=
 begin
   induction k with k ih,
   { simp },
-
   intro m,
   calc (f.iterated_deriv k.succ).coeff m
-      = f.coeff (m + k.succ) * (∏ i in finset.range k, ↑(m + k.succ - i)) * (m + 1) :
+      = f.coeff (m + k.succ) * (∏ i in range k, ↑(m + k.succ - i)) * (m + 1) :
     by rw [iterated_deriv_succ, coeff_derivative, ih m.succ, succ_add, add_succ]
-  ... = f.coeff (m + k.succ) * (↑(m + 1) * (∏ (i : ℕ) in range k, ↑(m + k.succ - i))) :
-    by { push_cast, ring }
-  ... = f.coeff (m + k.succ) * (∏ (i : ℕ) in range k.succ, ↑(m + k.succ - i)) :
-    by { rw [prod_range_succ, nat.add_sub_assoc (le_succ k), nat.succ_sub le_rfl, nat.sub_self] }
+  ... = f.coeff (m + k.succ) * (∏ i in range k, ↑(m + k.succ - i)) * ↑(m + 1) :
+    by push_cast
+  ... = f.coeff (m + k.succ) * (∏ i in range k.succ, ↑(m + k.succ - i)) :
+    by rw [prod_range_succ, nat.add_sub_assoc k.le_succ, succ_sub le_rfl, nat.sub_self, mul_assoc]
 end
 
 lemma iterated_deriv_eq_zero_of_nat_degree_lt (h : f.nat_degree < n) : iterated_deriv f n = 0 :=
@@ -205,7 +204,7 @@ begin
 
   congr,
   refine (sum_range_succ' _ _).trans (congr_arg2 (+) _ _),
-  { rw [sum_range_succ, nat.choose_succ_self, cast_zero, C.map_zero, zero_mul, zero_mul, zero_add],
+  { rw [sum_range_succ, nat.choose_succ_self, cast_zero, C.map_zero, zero_mul, zero_mul, add_zero],
     refine sum_congr rfl (λ k hk, _),
     rw mem_range at hk,
     congr,

diff --git a/src/data/polynomial/monic.lean b/src/data/polynomial/monic.lean
@@ -27,9 +27,9 @@ section semiring
 variables [semiring R] {p q r : polynomial R}
 
 lemma monic.as_sum {p : polynomial R} (hp : p.monic) :
-  p = X^(p.nat_degree) + (∑ i in finset.range p.nat_degree, C (p.coeff i) * X^i) :=
+  p = X^(p.nat_degree) + (∑ i in range p.nat_degree, C (p.coeff i) * X^i) :=
 begin
-  conv_lhs { rw [p.as_sum_range_C_mul_X_pow, finset.sum_range_succ] },
+  conv_lhs { rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm] },
   suffices : C (p.coeff p.nat_degree) = 1,
   { rw [this, one_mul] },
   exact congr_arg C hp