Eliminate part of a product type from `tsum`

Stream: Is there code for X?

[Devon Tuma]

Is there a simple way to show this lemma? :

lemma tsum_prod_eq_tsum_fst {α β γ : Type*} [add_comm_monoid α] [topological_space α] [t2_space α]
  {f : β × γ → α} (c : γ) (h : ∀ c' ≠ c, ∀ b, f (b, c') = 0) :
  ∑' (x : β × γ), f x = ∑' (b : β), f (b, c) :=
begin
  refine tsum_eq_tsum_of_ne_zero_bij (λ b, (b.1, c)) (λ x x' hx, _) (λ x hx, _) (λ x, rfl),
  { simpa only [eq_self_iff_true, and_true, prod.eq_iff_fst_eq_snd_eq] using hx },
  { cases x with b c',
    have hc : c' = c := by_contra (λ hc, hx $ h c' hc b),
    refine ⟨⟨b, by rwa [function.mem_support, ← hc]⟩, _⟩,
    simp only [prod.mk.inj_iff, eq_self_iff_true, true_and, hc] }
end

There is a obvious simpler proof using tsum_prod and tsum_eq_single, but that requires a summable hypothesis, which makes it more difficult to use and I'd rather avoid

[Eric Wieser]

A little shorter:

lemma tsum_prod_eq_tsum_fst {α β γ : Type*} [add_comm_monoid α] [topological_space α] [t2_space α]
  {f : β × γ → α} (c : γ) (h : ∀ c' ≠ c, ∀ b, f (b, c') = 0) :
  ∑' (x : β × γ), f x = ∑' (b : β), f (b, c) :=
begin
  refine tsum_eq_tsum_of_ne_zero_bij
    (λ b, (b, c)) (λ x x' hx, (congr_arg prod.fst hx : _)) (λ x (hx : f x ≠ _), _) (λ x, rfl),
  cases x with b c',
  obtain rfl : c' = c := by_contra (λ hc, hx $ h c' hc b),
  exact ⟨⟨b, hx⟩, rfl⟩
end

[Devon Tuma]

Would this be something worth opening a PR for (as well as the symmetric version of it)?

[Floris van Doorn]

I feel like this lemma is too specialized for mathlib. Here is a sequence of lemmas that make this lemma easier:

import topology.algebra.infinite_sum

open function set

variables {α β γ : Type*} [add_comm_monoid α] [topological_space α] [t2_space α]

lemma tsum_subtype_eq_of_support_subset {f : β → α} {s : set β} (hs : support f ⊆ s) :
  ∑' x : s, f x = ∑' x, f x :=
tsum_eq_tsum_of_has_sum_iff_has_sum $ λ x, has_sum_subtype_iff_of_support_subset hs

lemma tsum_univ (f : β → α) : ∑' x : (univ : set β), f x = ∑' x, f x :=
tsum_subtype_eq_of_support_subset $ subset_univ _

lemma tsum_image {g : γ → β} (f : β → α) {s : set γ} (hg : inj_on g s) :
  ∑' x : g '' s, f x = ∑' x : s, f (g x) :=
((equiv.set.image_of_inj_on _ _ hg).tsum_eq (λ x, f x)).symm

lemma tsum_range {g : γ → β} (f : β → α) (hg : injective g) :
  ∑' x : range g, f x = ∑' x, f (g x) :=
by rw [← image_univ, tsum_image f (hg.inj_on _), tsum_univ (f ∘ g)]

lemma tsum_prod_eq_tsum_fst
  {f : β × γ → α} (c : γ) (h : ∀ b, ∀ c' ≠ c, f (b, c') = 0) :
  ∑' (x : β × γ), f x = ∑' (b : β), f (b, c) :=
begin
  have : support f ⊆ range (λ x, (x, c)),
  { rintros ⟨b, c'⟩ hx, obtain rfl := of_not_not ((h _ _).mt hx.out), exact mem_range_self _ },
  rw [← tsum_subtype_eq_of_support_subset this, tsum_range f (prod.mk.inj_right c)]
end

I will PR all preliminary lemmas.

[Floris van Doorn]

#16671