Product of `univ : finset (option α)`

Stream: maths

[Anne Baanen]

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]

I would show that univ : finset (option β) is the same as insert none (erase none univ)

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Chris Hughes]

What is LateX for option.none?

[Patrick Massot]

I guess it depends on context.

[Chris Hughes]

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]

I think I understand the statement now.

[Kevin Buzzard]

Here's a proof.

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

[Anne Baanen]

Ah, prod_bij is what I was missing!

[Anne Baanen]

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

[Chris Hughes]

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]

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]

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

[Kevin Buzzard]

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]

(deleted)