## Stream: Is there code for X?

### Topic: Summing over monoid_hom.range

#### Eric Wieser (Jan 08 2021 at 15:34):

I managed to stumble into this proof, but if feels super awkward for something so obvious:

@[to_additive]
lemma finset.prod_filter_univ_exists_eq {α β γ : Type*}
[fintype α] [fintype β] [comm_monoid γ]
(f : α → β) (h : function.injective f) {_ : decidable_pred (λ (b : β), ∃ a, f a = b)} (g : β → γ) :
∏ x in finset.filter (λ (b : β), ∃ a, f a = b) finset.univ, g x = ∏ a, g (f a) :=
begin
rw finset.prod_subtype (λ x, show x ∈ _ ↔ ∃ a, x = f a, from _),
rotate, apply_instance, { simp only [finset.mem_filter, finset.mem_univ, true_and] },
symmetry,
apply finset.prod_bij
(λ a ha, (⟨f a, a, rfl⟩ : {x // ∃ (a : α), x = f a}))
(λ a ha, finset.mem_univ _)
(λ a ha, _)
(λ a₁ a₂ ha₁ ha₂ heq, h (subtype.ext_iff.mp heq))
(λ b hb, let ⟨a, hb⟩ := b.prop in ⟨a, finset.mem_univ _, subtype.ext (by convert hb)⟩),
refl,
end

lemma finset.sum_filter_univ_mem_monoid_hom_range {α β γ : Type*}
[fintype α] [fintype β]
[group α] [group β] [add_comm_monoid γ]
(f : α →* β) (h : function.injective f) {_ : decidable_pred (λ (b : β), b ∈ f.range)} (g : β → γ) :
∑ x in finset.filter (λ (b : β), b ∈ f.range) finset.univ, g x = ∑ a, g (f a) :=
begin
exact finset.sum_filter_univ_exists_eq f h g,
end


Am I missing some lemmas that do most of the lifting for me?

#### Eric Wieser (Jan 08 2021 at 15:35):

Part of the problem seems to be the lack of a finset version of set.range (docs#finset.range is something completely different)

#### Eric Wieser (Jan 08 2021 at 16:37):

Aha!

lemma finset.filter_mem_range_univ {α β : Type*}
[fintype α] [fintype β] [decidable_eq β]
(f : α → β) {_ : decidable_pred (λ (b : β), b ∈ set.range f)} :
finset.filter (λ (b : β), b ∈ set.range f) finset.univ = finset.image f finset.univ :=
by { ext, simp }

lemma finset.prod_filter_univ_exists_eq {α β γ : Type*}
[fintype α] [fintype β] [comm_monoid γ]
(f : α → β) (h : function.injective f) {_ : decidable_pred (λ (b : β), ∃ a, f a = b)} (g : β → γ) :
∏ x in finset.filter (λ (b : β), ∃ a, f a = b) finset.univ, g x = ∏ a, g (f a) :=
begin
classical,
rw ←finset.prod_image (λ x _ y _ (z : f x = f y), h z),
refine finset.prod_congr (finset.filter_mem_range_univ f) (λ _ _, rfl),
end


Are these names sensible enough for inclusion in mathlib?

#### Eric Wieser (Jan 12 2021 at 12:37):

#5708 adds the first one under a better name

#### Kyle Miller (Jan 12 2021 at 20:14):

I usually use finset.univ.image f. Your very first lemma ends up basically being finset.prod_image in algebra.big_operators.basic:

lemma finset.prod_filter_univ_exists_eq {α β γ : Type*}
[fintype α] [fintype β] [comm_monoid γ]
(f : α → β) (h : function.injective f) {_ : decidable_pred (λ (b : β), ∃ a, f a = b)} (g : β → γ) :
∏ x in finset.univ.filter (λ (b : β), ∃ a, f a = b), g x = ∏ a, g (f a) :=
begin
haveI : decidable_eq β := by { classical, apply_instance },
have him : finset.univ.filter (λ (b : β), ∃ a, f a = b) = finset.univ.image f,
{ ext, simp, },
rw him,
apply finset.prod_image,
simp,
apply h,
end


#### Kyle Miller (Jan 12 2021 at 20:16):

Oh, missed that that was from Jan 8 (and I appear to have only read the first message).

#### Eric Wieser (Jan 12 2021 at 20:21):

Right, your him is roughly the lemma I PR'd

Last updated: May 07 2021 at 22:14 UTC