finset.coe_product

Stream: Is there code for X?

[Yaël Dillies]

Am I dumb or are we missing this?

import data.finset.prod

lemma finset.coe_product (s : finset α) (t : finset β) :
  (s.product t : set (α × β)) = (s : set α).prod t :=
begin
  ext,
  simp,
end

[Eric Wieser]

I assume something like finset.ext $ λ _, finset.mem_product works too?

[Eric Wieser]

I think it's missing, I'd expect it right below docs#finset.mem_product

[Yaël Dillies]

Yeah me too.

[Yaël Dillies]

And I swear I used it before, so I formally concluded I was crazy.