## 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