Product of two `Fintype`s is a `Fintype`

Stream: Is there code for X?

[Jihoon Hyun]

I didn't search for it deeply, but it is absent at Mathlib.Data.Fintype.Basic.
Also, the version below uses DecidableEq, while I think there can be a version which DecidableEq is removed.
Do you have any ideas or comments?

instance ofProduct [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] : Fintype (α × β) :=
  ⟨Finset.univ.biUnion fun a : α => (Finset.univ.biUnion fun b : β => {(a, b)}), by
    intro x; simp; exists x.1, x.2⟩

[Ruben Van de Velde]

instFintypeProd Mathlib.Data.Fintype.Prod

[Jihoon Hyun]

Thanks for checking it out!