# Zulip Chat Archive

## Stream: maths

### Topic: Product of `univ : finset (option α)`

#### Anne Baanen (Mar 02 2020 at 13:35):

What is the best approach to proving the following goal:

example {α β : Type} {x : α} {v : β → α} [comm_monoid α] [fintype β] : finset.univ.prod (λ (i : option β), i.elim x v) = x * finset.univ.prod v := sorry

I guess `finset.sum_insert`

would be the first step?

#### Johan Commelin (Mar 02 2020 at 13:42):

I would show that `univ : finset (option β)`

is the same as `insert none (erase none univ)`

#### Johan Commelin (Mar 02 2020 at 13:42):

After that, I think there are enough library lemmas to just follow your nose.

#### Johan Commelin (Mar 02 2020 at 13:43):

(Just a guess...) If you get stuck, then you've certainly found a hole in the library.

#### Patrick Massot (Mar 02 2020 at 13:49):

I can't even parse the statement. Can someone translate this into LaTeX for me?

#### Chris Hughes (Mar 02 2020 at 13:50):

What is LateX for `option.none`

?

#### Patrick Massot (Mar 02 2020 at 13:50):

I guess it depends on context.

#### Chris Hughes (Mar 02 2020 at 13:50):

Here's a proof.

calc univ.prod (λ (i : option β), i.elim x v) = x * (univ.erase (none)).prod (λ (i : option β), i.elim x v) : begin conv_lhs { rw [← insert_erase (mem_univ (none : option β))] }, rw [prod_insert (not_mem_erase _ _)], refl end ... = x * finset.univ.prod v : begin refine congr_arg2 _ rfl (prod_bij (λ a _, some a) _ _ _ _).symm, { simp }, { intros, refl }, { simp }, { assume b, cases b with b, { simp }, { intro, use b, simp } } end

#### Patrick Massot (Mar 02 2020 at 13:51):

I think I understand the statement now.

#### Kevin Buzzard (Mar 02 2020 at 14:00):

Here's a proof.

but where's your proof that it's the best approach? ;-)

#### Anne Baanen (Mar 02 2020 at 14:00):

Ah, `prod_bij`

is what I was missing!

#### Anne Baanen (Mar 02 2020 at 14:01):

Would it be worth it to include this in mathlib (as a `@[simp]`

lemma)?

#### Chris Hughes (Mar 02 2020 at 14:01):

`prod_bij`

is really handy. We need docs that say things like `prod_bij`

is how you prove a lot of things about products.

#### Kevin Buzzard (Mar 02 2020 at 14:06):

Patrick Massot said:

I can't even parse the statement. Can someone translate this into LaTeX for me?

It says $x\prod_{i\in\beta}v(i)=x\prod_{i\in\beta}v(i)$

#### Patrick Massot (Mar 02 2020 at 14:08):

That translation explains why this is a hard Lean problem. Empty math implies hard Lean almost surely.

#### Kevin Buzzard (Mar 02 2020 at 14:09):

Nice proof Chris. This is exactly, I guess, why one needs `prod_bij`

: it says "the products over two sets that mathematicians might not be able to tell the difference between, are equal"

#### Yury G. Kudryashov (Mar 02 2020 at 14:10):

(deleted)

Last updated: May 06 2021 at 18:20 UTC