chore(ring_theory/power_series): review, golf (#5431)

src/algebra/big_operators/basic.lean

@@ -258,15 +258,18 @@ begin
   apply h, cc
 end
 
-/-- An uncurried version of `prod_product`. -/
-@[to_additive]
+/-- An uncurried version of `finset.prod_product`. -/
+@[to_additive "An uncurried version of `finset.sum_product`"]
 lemma prod_product' {s : finset γ} {t : finset α} {f : γ → α → β} :
   (∏ x in s.product t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
 prod_product
 
-@[to_additive]
+/-- Product over a sigma type equals the product of fiberwise products. For rewriting
+in the reverse direction, use `finset.prod_sigma'`.  -/
+@[to_additive "Sum over a sigma type equals the sum of fiberwise sums. For rewriting
+in the reverse direction, use `finset.sum_sigma'`"]
 lemma prod_sigma {σ : α → Type*}
-  {s : finset α} {t : Πa, finset (σ a)} {f : sigma σ → β} :
+  (s : finset α) (t : Πa, finset (σ a)) (f : sigma σ → β) :
   (∏ x in s.sigma t, f x) = ∏ a in s, ∏ s in (t a), f ⟨a, s⟩ :=
 by classical;
 calc (∏ x in s.sigma t, f x) =
@@ -278,6 +281,12 @@ calc (∏ x in s.sigma t, f x) =
   ... = ∏ a in s, ∏ s in t a, f ⟨a, s⟩ :
     prod_congr rfl $ λ _ _, prod_map _ _ _
 
+@[to_additive]
+lemma prod_sigma' {σ : α → Type*}
+  (s : finset α) (t : Πa, finset (σ a)) (f : Πa, σ a → β) :
+  (∏ a in s, ∏ s in (t a), f a s) = ∏ x in s.sigma t, f x.1 x.2 :=
+eq.symm $ prod_sigma s t (λ x, f x.1 x.2)
+
 @[to_additive]
 lemma prod_fiberwise_of_maps_to [decidable_eq γ] {s : finset α} {t : finset γ} {g : α → γ}
   (h : ∀ x ∈ s, g x ∈ t) (f : α → β) :
@@ -503,6 +512,11 @@ prod_dite_eq s a (λ x _, b x)
   (∏ x in s, (ite (x = a) (b x) 1)) = ite (a ∈ s) (b a) 1 :=
 prod_dite_eq' s a (λ x _, b x)
 
+@[to_additive]
+lemma prod_ite_index (p : Prop) [decidable p] (s t : finset α) (f : α → β) :
+  (∏ x in if p then s else t, f x) = if p then ∏ x in s, f x else ∏ x in t, f x :=
+apply_ite (λ s, ∏ x in s, f x) _ _ _
+
 /--
   Reorder a product.
 
@@ -781,7 +795,7 @@ lemma prod_comp [decidable_eq γ] {s : finset α} (f : γ → β) (g : α → γ
 calc ∏ a in s, f (g a)
     = ∏ x in (s.image g).sigma (λ b : γ, s.filter (λ a, g a = b)), f (g x.2) :
   prod_bij (λ a ha, ⟨g a, a⟩) (by simp; tauto) (λ _ _, rfl) (by simp) (by finish)
-... = ∏ b in s.image g, ∏ a in s.filter (λ a, g a = b), f (g a) : prod_sigma
+... = ∏ b in s.image g, ∏ a in s.filter (λ a, g a = b), f (g a) : prod_sigma _ _ _
 ... = ∏ b in s.image g, ∏ a in s.filter (λ a, g a = b), f b :
   prod_congr rfl (λ b hb, prod_congr rfl (by simp {contextual := tt}))
 ... = ∏ b in s.image g, f b ^ (s.filter (λ a, g a = b)).card :

src/analysis/analytic/composition.lean

@@ -594,12 +594,7 @@ begin
     by simpa only [formal_multilinear_series.partial_sum,
                    continuous_multilinear_map.map_sum_finset] using H,
   -- rewrite the first sum as a big sum over a sigma type
-  rw ← @finset.sum_sigma _ _ _ _
-    (finset.range N) (λ (n : ℕ), (fintype.pi_finset (λ (i : fin n), finset.Ico 1 N)) : _)
-    (λ i, q i.1 (λ (j : fin i.1), p (i.2 j) (λ (k : fin (i.2 j)), z))),
-  show ∑ i in comp_partial_sum_source N,
-    q i.1 (λ (j : fin i.1), p (i.2 j) (λ (k : fin (i.2 j)), z)) =
-    ∑ i in comp_partial_sum_target N, q.comp_along_composition_multilinear p i.2 (λ j, z),
+  rw [finset.sum_sigma'],
   -- show that the two sums correspond to each other by reindexing the variables.
   apply finset.sum_bij (comp_change_of_variables N),
   -- To conclude, we should show that the correspondance we have set up is indeed a bijection
@@ -1057,19 +1052,14 @@ begin
   /- First, rewrite the two compositions appearing in the theorem as two sums over complicated
   sigma types, as in the description of the proof above. -/
   let f : (Σ (a : composition n), composition a.length) → H :=
-    λ ⟨a, b⟩, r b.length (apply_composition q b (apply_composition p a v)),
+    λ c, r c.2.length (apply_composition q c.2 (apply_composition p c.1 v)),
   let g : (Σ (c : composition n), Π (i : fin c.length), composition (c.blocks_fun i)) → H :=
-    λ ⟨c, d⟩, r c.length
-      (λ (i : fin c.length), q (d i).length (apply_composition p (d i) (v ∘ c.embedding i))),
-  suffices A : ∑ c, f c = ∑ c, g c,
-  { dsimp [formal_multilinear_series.comp],
-    simp only [continuous_multilinear_map.sum_apply, comp_along_composition_apply],
-    rw ← @finset.sum_sigma _ _ _ _ (finset.univ : finset (composition n)) _ f,
-    dsimp [apply_composition],
-    simp only [continuous_multilinear_map.sum_apply, comp_along_composition_apply,
-      continuous_multilinear_map.map_sum],
-    rw ← @finset.sum_sigma _ _ _ _ (finset.univ : finset (composition n)) _ g,
-    exact A },
+    λ c, r c.1.length (λ (i : fin c.1.length),
+      q (c.2 i).length (apply_composition p (c.2 i) (v ∘ c.1.embedding i))),
+  suffices : ∑ c, f c = ∑ c, g c,
+    by simpa only [formal_multilinear_series.comp, continuous_multilinear_map.sum_apply,
+      comp_along_composition_apply, continuous_multilinear_map.map_sum, finset.sum_sigma',
+      apply_composition],
   /- Now, we use `composition.sigma_equiv_sigma_pi n` to change
   variables in the second sum, and check that we get exactly the same sums. -/
   rw ← (sigma_equiv_sigma_pi n).sum_comp,

src/data/complex/exponential.lean

@@ -184,11 +184,7 @@ end
 lemma sum_range_diag_flip {α : Type*} [add_comm_monoid α] (n : ℕ) (f : ℕ → ℕ → α) :
   ∑ m in range n, ∑ k in range (m + 1), f k (m - k) =
   ∑ m in range n, ∑ k in range (n - m), f m k :=
-have h₁ : ∑ a in (range n).sigma (range ∘ nat.succ), f (a.2) (a.1 - a.2) =
-    ∑ m in range n, ∑ k in range (m + 1), f k (m - k) := sum_sigma,
-have h₂ : ∑ a in (range n).sigma (λ m, range (n - m)), f (a.1) (a.2) =
-    ∑ m in range n, ∑ k in range (n - m), f m k := sum_sigma,
-h₁ ▸ h₂ ▸ sum_bij
+by rw [sum_sigma', sum_sigma']; exact sum_bij
 (λ a _, ⟨a.2, a.1 - a.2⟩)
 (λ a ha, have h₁ : a.1 < n := mem_range.1 (mem_sigma.1 ha).1,
   have h₂ : a.2 < nat.succ a.1 := mem_range.1 (mem_sigma.1 ha).2,

src/data/nat/enat.lean

@@ -150,7 +150,7 @@ instance order_top : order_top enat :=
 
 lemma top_eq_none : (⊤ : enat) = none := rfl
 
-lemma coe_lt_top (x : ℕ) : (x : enat) < ⊤ :=
+@[simp] lemma coe_lt_top (x : ℕ) : (x : enat) < ⊤ :=
 lt_of_le_of_ne le_top (λ h, absurd (congr_arg dom h) true_ne_false)
 
 @[simp] lemma coe_ne_top (x : ℕ) : (x : enat) ≠ ⊤ := ne_of_lt (coe_lt_top x)

src/number_theory/arithmetic_function.lean

@@ -189,11 +189,7 @@ lemma mul_smul' (f g : arithmetic_function R) (h : arithmetic_function M) :
   (f * g) • h = f • g • h :=
 begin
   ext n,
-  simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum],
-  apply eq.trans (@finset.sum_sigma (ℕ × ℕ) M _ _ (divisors_antidiagonal n)
-    (λ p, (divisors_antidiagonal p.1)) (λ x, f x.2.1 • g x.2.2 • h x.1.2)).symm,
-  apply eq.trans _ (@finset.sum_sigma (ℕ × ℕ) M _ _ (divisors_antidiagonal n)
-    (λ p, (divisors_antidiagonal p.2)) (λ x, f x.1.1 • (g x.2.1 • h x.2.2))),
+  simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum, finset.sum_sigma'],
   apply finset.sum_bij,
   swap 5,
   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, exact ⟨(k, l*j), (l, j)⟩ },