refactor(topology/algebra/infinite_sum): review (#3371)

## Rename

- `has_sum_unique` → `has_sum.unique`;
- `summable.summable_comp_of_injective` → `summable.comp_injective`;
- `has_sum_iff_tendsto_nat_of_summable` → `summable.has_sum_iff_tendsto_nat`;
- `tsum_eq_has_sum` → `has_sum.tsum_eq`;
- `support_comp` → `support_comp_subset`, delete `support_comp'`;

## Change arguments

- `tsum_eq_tsum_of_ne_zero_bij`, `has_sum_iff_has_sum_of_ne_zero_bij`: use functions from `support` instead of `Π x, f x ≠ 0 → β`;


## Add

- `indicator_compl_add_self_apply`, `indicator_compl_add_self`;
- `indicator_self_add_compl_apply`, `indicator_self_add_compl`;
- `support_subset_iff`, `support_subset_iff'`;
- `support_subset_comp`;
- `support_prod_mk`;
- `embedding.coe_subtype`;

src/analysis/analytic/basic.lean

@@ -304,7 +304,7 @@ begin
     have : 0 < i := bot_lt_iff_ne_bot.mpr hi,
     apply continuous_multilinear_map.map_coord_zero _ (⟨0, this⟩ : fin i),
     refl },
-  have A := has_sum_unique (hf.has_sum zero_mem) (has_sum_single _ this),
+  have A := (hf.has_sum zero_mem).unique (has_sum_single _ this),
   simpa [v_eq] using A.symm,
 end
 
@@ -441,7 +441,7 @@ lemma has_fpower_series_on_ball.sum [complete_space F] (h : has_fpower_series_on
 begin
   have A := h.has_sum hy,
   have B := (p.has_fpower_series_on_ball h.radius_pos).has_sum (lt_of_lt_of_le hy h.r_le),
-  simpa using has_sum_unique A B
+  simpa using A.unique B
 end
 
 /-- The sum of a converging power series is continuous in its disk of convergence. -/
@@ -589,7 +589,7 @@ begin
     ennreal.lt_iff_exists_add_pos_lt.mp h,
   have S : @summable ℝ _ _ _ ((λ ⟨n, s, hs⟩, ∥(p n).restr s hs x∥ * (r : ℝ) ^ k) :
     (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ),
-  { convert summable.summable_comp_of_injective (p.change_origin_summable_aux2 hr)
+  { convert (p.change_origin_summable_aux2 hr).comp_injective
       (change_origin_summable_aux_j_injective k),
     -- again, cleanup that could be done by `tidy`:
     ext ⟨_, ⟨_, _⟩⟩, refl },

src/analysis/normed_space/basic.lean

@@ -1099,12 +1099,11 @@ real function `g` which is summable, then `f` is summable. -/
 lemma summable_of_norm_bounded_eventually {f : ι → α} (g : ι → ℝ) (hg : summable g)
   (h : ∀ᶠ i in cofinite, ∥f i∥ ≤ g i) : summable f :=
 begin
-  let s : finset ι := (mem_cofinite.mp h).to_finset,
-  refine (summable_subtype_iff s).mp _,
-  refine summable_of_norm_bounded _ ((summable_subtype_iff s).mpr hg) _,
-  refine subtype.forall.mpr _,
-  intros a h',
-  simpa [s] using h',
+  replace h := mem_cofinite.1 h,
+  refine h.summable_compl_iff.mp _,
+  refine summable_of_norm_bounded _ (h.summable_compl_iff.mpr hg) _,
+  rintros ⟨a, h'⟩,
+  simpa using h'
 end
 
 lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → nnreal) (hg : summable g)

src/analysis/special_functions/exp_log.lean

@@ -513,7 +513,7 @@ end
 theorem has_sum_pow_div_log_of_abs_lt_1 {x : ℝ} (h : abs x < 1) :
   has_sum (λ (n : ℕ), x ^ (n + 1) / (n + 1)) (-log (1 - x)) :=
 begin
-  rw has_sum_iff_tendsto_nat_of_summable,
+  rw summable.has_sum_iff_tendsto_nat,
   show tendsto (λ (n : ℕ), ∑ (i : ℕ) in range n, x ^ (i + 1) / (i + 1)) at_top (𝓝 (-log (1 - x))),
   { rw [tendsto_iff_norm_tendsto_zero],
     simp only [norm_eq_abs, sub_neg_eq_add],

src/analysis/specific_limits.lean

@@ -261,7 +261,7 @@ lemma summable_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : sum
 ⟨_, has_sum_geometric_of_lt_1 h₁ h₂⟩
 
 lemma tsum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
-tsum_eq_has_sum (has_sum_geometric_of_lt_1 h₁ h₂)
+(has_sum_geometric_of_lt_1 h₁ h₂).tsum_eq
 
 lemma has_sum_geometric_two : has_sum (λn:ℕ, ((1:ℝ)/2) ^ n) 2 :=
 by convert has_sum_geometric_of_lt_1 _ _; norm_num
@@ -270,7 +270,7 @@ lemma summable_geometric_two : summable (λn:ℕ, ((1:ℝ)/2) ^ n) :=
 ⟨_, has_sum_geometric_two⟩
 
 lemma tsum_geometric_two : (∑'n:ℕ, ((1:ℝ)/2) ^ n) = 2 :=
-tsum_eq_has_sum has_sum_geometric_two
+has_sum_geometric_two.tsum_eq
 
 lemma sum_geometric_two_le (n : ℕ) : ∑ (i : ℕ) in range n, (1 / (2 : ℝ)) ^ i ≤ 2 :=
 begin
@@ -292,7 +292,7 @@ lemma summable_geometric_two' (a : ℝ) : summable (λ n:ℕ, (a / 2) / 2 ^ n) :
 ⟨a, has_sum_geometric_two' a⟩
 
 lemma tsum_geometric_two' (a : ℝ) : (∑' n:ℕ, (a / 2) / 2^n) = a :=
-tsum_eq_has_sum $ has_sum_geometric_two' a
+(has_sum_geometric_two' a).tsum_eq
 
 lemma nnreal.has_sum_geometric {r : nnreal} (hr : r < 1) :
   has_sum (λ n : ℕ, r ^ n) (1 - r)⁻¹ :=
@@ -307,7 +307,7 @@ lemma nnreal.summable_geometric {r : nnreal} (hr : r < 1) : summable (λn:ℕ, r
 ⟨_, nnreal.has_sum_geometric hr⟩
 
 lemma tsum_geometric_nnreal {r : nnreal} (hr : r < 1) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
-tsum_eq_has_sum (nnreal.has_sum_geometric hr)
+(nnreal.has_sum_geometric hr).tsum_eq
 
 /-- The series `pow r` converges to `(1-r)⁻¹`. For `r < 1` the RHS is a finite number,
 and for `1 ≤ r` the RHS equals `∞`. -/
@@ -343,7 +343,7 @@ lemma summable_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : summable (λn:ℕ, ξ
 ⟨_, has_sum_geometric_of_norm_lt_1 h⟩
 
 lemma tsum_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : (∑'n:ℕ, ξ ^ n) = (1 - ξ)⁻¹ :=
-tsum_eq_has_sum (has_sum_geometric_of_norm_lt_1 h)
+(has_sum_geometric_of_norm_lt_1 h).tsum_eq
 
 lemma has_sum_geometric_of_abs_lt_1 {r : ℝ} (h : abs r < 1) : has_sum (λn:ℕ, r ^ n) (1 - r)⁻¹ :=
 has_sum_geometric_of_norm_lt_1 h
@@ -467,7 +467,7 @@ cauchy_seq_of_dist_le_of_summable _ hu ⟨_, aux_has_sum_of_le_geometric hr hu
 `f n` to the limit of `f` is bounded above by `C * r^n / (1 - r)`. -/
 lemma dist_le_of_le_geometric_of_tendsto₀ {a : α} (ha : tendsto f at_top (𝓝 a)) :
   dist (f 0) a ≤ C / (1 - r) :=
-(tsum_eq_has_sum $ aux_has_sum_of_le_geometric hr hu) ▸
+(aux_has_sum_of_le_geometric hr hu).tsum_eq ▸
   dist_le_tsum_of_dist_le_of_tendsto₀ _ hu ⟨_, aux_has_sum_of_le_geometric hr hu⟩ ha
 
 /-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then the distance from
@@ -479,7 +479,7 @@ begin
   convert dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n,
   simp only [pow_add, mul_left_comm C, mul_div_right_comm],
   rw [mul_comm],
-  exact (eq.symm $ tsum_eq_has_sum $ this.mul_left _)
+  exact (this.mul_left _).tsum_eq.symm
 end
 
 omit hr hu
@@ -506,7 +506,7 @@ begin
   convert dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n,
   simp only [add_comm n, pow_add, (div_div_eq_div_mul _ _ _).symm],
   symmetry,
-  exact tsum_eq_has_sum (has_sum.mul_right _ $ has_sum_geometric_two' C)
+  exact ((has_sum_geometric_two' C).mul_right _).tsum_eq
 end
 
 end le_geometric
@@ -604,8 +604,7 @@ begin
   have hf : has_sum f ε := has_sum_geometric_two' _,
   have f0 : ∀ n, 0 < f n := λ n, div_pos (half_pos hε) (pow_pos two_pos _),
   refine ⟨f ∘ encodable.encode, λ i, f0 _, _⟩,
-  rcases hf.summable.summable_comp_of_injective (@encodable.encode_injective ι _)
-    with ⟨c, hg⟩,
+  rcases hf.summable.comp_injective (@encodable.encode_injective ι _) with ⟨c, hg⟩,
   refine ⟨c, hg, has_sum_le_inj _ (@encodable.encode_injective ι _) _ _ hg hf⟩,
   { assume i _, exact le_of_lt (f0 _) },
   { assume n, exact le_refl _ }

src/data/indicator_function.lean

@@ -115,6 +115,22 @@ lemma indicator_add (s : set α) (f g : α → β) :
   indicator s (λa, f a + g a) = λa, indicator s f a + indicator s g a :=
 by { funext, simp only [indicator], split_ifs, { refl }, rw add_zero }
 
+@[simp] lemma indicator_compl_add_self_apply (s : set α) (f : α → β) (a : α) :
+  indicator sᶜ f a + indicator s f a = f a :=
+classical.by_cases (λ ha : a ∈ s, by simp [ha]) (λ ha, by simp [ha])
+
+@[simp] lemma indicator_compl_add_self (s : set α) (f : α → β) :
+  indicator sᶜ f + indicator s f = f :=
+funext $ indicator_compl_add_self_apply s f
+
+@[simp] lemma indicator_self_add_compl_apply (s : set α) (f : α → β) (a : α) :
+  indicator s f a + indicator sᶜ f a = f a :=
+classical.by_cases (λ ha : a ∈ s, by simp [ha]) (λ ha, by simp [ha])
+
+@[simp] lemma indicator_self_add_compl (s : set α) (f : α → β) :
+  indicator s f + indicator sᶜ f = f :=
+funext $ indicator_self_add_compl_apply s f
+
 variables (β)
 instance is_add_monoid_hom.indicator (s : set α) : is_add_monoid_hom (λf:α → β, indicator s f) :=
 { map_add := λ _ _, indicator_add _ _ _,
@@ -143,15 +159,8 @@ lemma indicator_sub (s : set α) (f g : α → β) :
   indicator s (λa, f a - g a) = λa, indicator s f a - indicator s g a :=
 show indicator s (f - g) = indicator s f - indicator s g, from is_add_group_hom.map_sub _ _ _
 
-lemma indicator_compl (s : set α) (f : α → β) : indicator sᶜ f = λ a, f a - indicator s f a :=
-begin
-  funext,
-  simp only [indicator],
-  split_ifs with h₁ h₂,
-  { rw sub_zero },
-  { rw sub_self },
-  { rw ← mem_compl_iff at h₂, contradiction }
-end
+lemma indicator_compl (s : set α) (f : α → β) : indicator sᶜ f = f - indicator s f :=
+eq_sub_of_add_eq $ s.indicator_compl_add_self f
 
 lemma indicator_finset_sum {β} [add_comm_monoid β] {ι : Type*} (I : finset ι) (s : set α) (f : ι → α → β) :
   indicator s (∑ i in I, f i) = ∑ i in I, indicator s (f i) :=

src/data/set/basic.lean

@@ -317,6 +317,9 @@ by simp [subset.antisymm_iff]
 theorem eq_empty_of_subset_empty {s : set α} : s ⊆ ∅ → s = ∅ :=
 subset_empty_iff.1
 
+theorem eq_empty_of_not_nonempty (h : ¬nonempty α) (s : set α) : s = ∅ :=
+eq_empty_of_subset_empty $ λ x hx, h ⟨x⟩
+
 lemma not_nonempty_iff_eq_empty {s : set α} : ¬s.nonempty ↔ s = ∅ :=
 by simp only [set.nonempty, eq_empty_iff_forall_not_mem, not_exists]
 
@@ -959,6 +962,10 @@ begin
   { simp [h, h'] }
 end
 
+lemma insert_diff_self_of_not_mem {a : α} {s : set α} (h : a ∉ s) :
+  insert a s \ {a} = s :=
+ext $ λ x, by simp [and_iff_left_of_imp (λ hx : x ∈ s, show x ≠ a, from λ hxa, h $ hxa ▸ hx)]
+
 theorem union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t :=
 by finish [ext_iff, iff_def]
 

src/data/support.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import order.conditionally_complete_lattice
 import algebra.big_operators
+import algebra.group.prod
 
 /-!
 # Support of a function
@@ -31,6 +32,14 @@ lemma mem_support [has_zero A] {f : α → A} {x : α} :
   x ∈ support f ↔ f x ≠ 0 :=
 iff.rfl
 
+lemma support_subset_iff [has_zero A] {f : α → A} {s : set α} :
+  support f ⊆ s ↔ ∀ x, f x ≠ 0 → x ∈ s :=
+iff.rfl
+
+lemma support_subset_iff' [has_zero A] {f : α → A} {s : set α} :
+  support f ⊆ s ↔ ∀ x ∉ s, f x = 0 :=
+forall_congr $ λ x, by classical; exact not_imp_comm
+
 lemma support_binop_subset [has_zero A] (op : A → A → A) (op0 : op 0 0 = 0) (f g : α → A) :
   support (λ x, op (f x) (g x)) ⊆ support f ∪ support g :=
 λ x hx, classical.by_cases
@@ -112,22 +121,23 @@ lemma support_prod [comm_monoid_with_zero A] [no_zero_divisors A] [nontrivial A]
 set.ext $ λ x, by
   simp only [support, ne.def, finset.prod_eq_zero_iff, mem_set_of_eq, set.mem_Inter, not_exists]
 
-lemma support_comp [has_zero A] [has_zero B] (g : A → B) (hg : g 0 = 0) (f : α → A) :
+lemma support_comp_subset [has_zero A] [has_zero B] {g : A → B} (hg : g 0 = 0) (f : α → A) :
   support (g ∘ f) ⊆ support f :=
 λ x, mt $ λ h, by simp [(∘), *]
 
-lemma support_comp' [has_zero A] [has_zero B] (g : A → B) (hg : g 0 = 0) (f : α → A) :
-  support (λ x, g (f x)) ⊆ support f :=
-support_comp g hg f
+lemma support_subset_comp [has_zero A] [has_zero B] {g : A → B} (hg : ∀ {x}, g x = 0 → x = 0)
+  (f : α → A) :
+  support f ⊆ support (g ∘ f) :=
+λ x, mt hg
 
 lemma support_comp_eq [has_zero A] [has_zero B] (g : A → B) (hg : ∀ {x}, g x = 0 ↔ x = 0)
   (f : α → A) :
   support (g ∘ f) = support f :=
 set.ext $ λ x, not_congr hg
 
-lemma support_comp_eq' [has_zero A] [has_zero B] (g : A → B) (hg : ∀ {x}, g x = 0 ↔ x = 0)
-  (f : α → A) :
-  support (λ x, g (f x)) = support f :=
-support_comp_eq g @hg f
+lemma support_prod_mk [has_zero A] [has_zero B] (f : α → A) (g : α → B) :
+  support (λ x, (f x, g x)) = support f ∪ support g :=
+set.ext $ λ x, by simp only [support, classical.not_and_distrib, mem_union_eq, mem_set_of_eq,
+  prod.mk_eq_zero, ne.def]
 
 end function

src/logic/embedding.lean

@@ -107,7 +107,9 @@ protected def some {α} : α ↪ option α :=
 
 /-- Embedding of a `subtype`. -/
 def subtype {α} (p : α → Prop) : subtype p ↪ α :=
-⟨subtype.val, λ _ _, subtype.ext_val⟩
+⟨coe, λ _ _, subtype.ext_val⟩
+
+@[simp] lemma coe_subtype {α} (p : α → Prop) : ⇑(subtype p) = coe := rfl
 
 /-- Choosing an element `b : β` gives an embedding of `punit` into `β`. -/
 def punit {β : Sort*} (b : β) : punit ↪ β :=

src/measure_theory/outer_measure.lean

@@ -80,15 +80,15 @@ begin
     cases decode2 β n with b,
     { exact (h (by simp [m0])).elim },
     { exact rfl } },
-  refine tsum_eq_tsum_of_ne_zero_bij (λ n h, option.get (H n h)) _ _ _,
-  { intros m n hm hn e,
+  refine tsum_eq_tsum_of_ne_zero_bij (λ a, option.get (H a.1 a.2)) _ _ _,
+  { rintros ⟨m, hm⟩ ⟨n, hn⟩ e,
     have := mem_decode2.1 (option.get_mem (H n hn)),
     rwa [← e, mem_decode2.1 (option.get_mem (H m hm))] at this },
   { intros b h,
-    refine ⟨encode b, _, _⟩,
-    { convert h, simp [set.ext_iff, encodek2] },
+    refine ⟨⟨encode b, _⟩, _⟩,
+    { simp only [mem_support, encodek2] at h ⊢, convert h, simp [set.ext_iff, encodek2] },
     { exact option.get_of_mem _ (encodek2 _) } },
-  { intros n h,
+  { rintros ⟨n, h⟩, dsimp only [subtype.coe_mk],
     transitivity, swap,
     rw [show decode2 β n = _, from option.get_mem (H n h)],
     congr, simp [set.ext_iff, -option.some_get] }
@@ -300,7 +300,7 @@ let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑'i, m (f i) in
           (by simpa using hε' i),
       simpa [μ, infi_lt_iff] },
     refine le_trans _ (ennreal.tsum_le_tsum $ λ i, le_of_lt (hf i).2),
-    rw [← ennreal.tsum_prod, ← tsum_equiv equiv.nat_prod_nat_equiv_nat.symm],
+    rw [← ennreal.tsum_prod, ← equiv.nat_prod_nat_equiv_nat.symm.tsum_eq],
     swap, {apply_instance},
     refine infi_le_of_le _ (infi_le _ _),
     exact Union_subset (λ i, subset.trans (hf i).1 $

src/measure_theory/probability_mass_function.lean

@@ -24,7 +24,7 @@ lemma has_sum_coe_one (p : pmf α) : has_sum p 1 := p.2
 
 lemma summable_coe (p : pmf α) : summable p := (p.has_sum_coe_one).summable
 
-@[simp] lemma tsum_coe (p : pmf α) : (∑'a, p a) = 1 := tsum_eq_has_sum p.has_sum_coe_one
+@[simp] lemma tsum_coe (p : pmf α) : (∑'a, p a) = 1 := p.has_sum_coe_one.tsum_eq
 
 def support (p : pmf α) : set α := {a | p.1 a ≠ 0}
 

src/measure_theory/set_integral.lean

@@ -310,7 +310,7 @@ lemma integral_on_Union (s : ℕ → set α) (f : α → β) (hm : ∀i, is_meas
   (hd : ∀ i j, i ≠ j → s i ∩ s j = ∅) (hfm : measurable_on (Union s) f) (hfi : integrable_on (Union s) f) :
   (∫ a in (Union s), f a) = ∑'i, ∫ a in s i, f a :=
 suffices h : tendsto (λn:finset ℕ, ∑ i in n, ∫ a in s i, f a) at_top (𝓝 $ (∫ a in (Union s), f a)),
-  by { rwa tsum_eq_has_sum },
+  by { rwa has_sum.tsum_eq },
 begin
   have : (λn:finset ℕ, ∑ i in n, ∫ a in s i, f a) = λn:finset ℕ, ∫ a in (⋃i∈n, s i), f a,
   { funext,

src/order/filter/at_top_bot.lean

@@ -19,7 +19,7 @@ Then we prove many lemmas like “if `f → +∞`, then `f ± c → +∞`”.
 variables {α β γ : Type*}
 
 open set
-open_locale classical filter
+open_locale classical filter big_operators
 
 namespace filter
 /-- `at_top` is the filter representing the limit `→ ∞` on an ordered set.
@@ -516,4 +516,51 @@ lemma tendsto_at_top_of_monotone_of_subseq {ι ι' α : Type*} [preorder ι] [pr
   tendsto u at_top at_top :=
 tendsto_at_top_of_monotone_of_filter h (map_ne_bot hl) (tendsto_map' H)
 
+/-- Let `f` and `g` be two maps to the same commutative monoid. This lemma gives a sufficient
+condition for comparison of the filter `at_top.map (λ s, ∏ b in s, f b)` with
+`at_top.map (λ s, ∏ b in s, g b)`. This is useful to compare the set of limit points of
+`Π b in s, f b` as `s → at_top` with the similar set for `g`. -/
+@[to_additive]
+lemma map_at_top_finset_prod_le_of_prod_eq [comm_monoid α] {f : β → α} {g : γ → α}
+  (h_eq : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b) :
+  at_top.map (λs:finset β, ∏ b in s, f b) ≤ at_top.map (λs:finset γ, ∏ x in s, g x) :=
+by rw [map_at_top_eq, map_at_top_eq];
+from (le_infi $ assume b, let ⟨v, hv⟩ := h_eq b in infi_le_of_le v $
+  by simp [set.image_subset_iff]; exact hv)
+
 end filter
+
+open filter finset
+
+/-- Let `g : γ → β` be an injective function and `f : β → α` be a function from the codomain of `g`
+to a commutative monoid. Suppose that `f x = 1` outside of the range of `g`. Then the filters
+`at_top.map (λ s, ∏ i in s, f (g i))` and `at_top.map (λ s, ∏ i in s, f i)` coincide.
+
+The additive version of this lemma is used to prove the equality `∑' x, f (g x) = ∑' y, f y` under
+the same assumptions.-/
+@[to_additive]
+lemma function.injective.map_at_top_finset_prod_eq [comm_monoid α] {g : γ → β}
+  (hg : function.injective g) {f : β → α} (hf : ∀ x ∉ set.range g, f x = 1) :
+  map (λ s, ∏ i in s, f (g i)) at_top = map (λ s, ∏ i in s, f i) at_top :=
+begin
+  apply le_antisymm; refine map_at_top_finset_prod_le_of_prod_eq (λ s, _),
+  { refine ⟨s.preimage (hg.inj_on _), λ t ht, _⟩,
+    refine ⟨t.image g ∪ s, finset.subset_union_right _ _, _⟩,
+    rw [← finset.prod_image (hg.inj_on _)],
+    refine (prod_subset (subset_union_left _ _) _).symm,
+    simp only [finset.mem_union, finset.mem_image],
+    refine λ y hy hyt, hf y (mt _ hyt),
+    rintros ⟨x, rfl⟩,
+    exact ⟨x, ht (finset.mem_preimage.2 $ hy.resolve_left hyt), rfl⟩ },
+  { refine ⟨s.image g, λ t ht, _⟩,
+    simp only [← prod_preimage _ _ (hg.inj_on _) _ (λ x _, hf x)],
+    exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩ }
+end
+
+/-- Let `g : γ → β` be an injective function and `f : β → α` be a function from the codomain of `g`
+to an additive commutative monoid. Suppose that `f x = 0` outside of the range of `g`. Then the
+filters `at_top.map (λ s, ∑ i in s, f (g i))` and `at_top.map (λ s, ∑ i in s, f i)` coincide.
+
+This lemma is used to prove the equality `∑' x, f (g x) = ∑' y, f y` under
+the same assumptions.-/
+add_decl_doc function.injective.map_at_top_finset_sum_eq