# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: pi_instance for products

#### Adam Topaz (Dec 08 2020 at 16:25):

Do we have something like `pi_instance`

for binary products?

#### Eric Wieser (Dec 08 2020 at 16:31):

I assume you don't mean docs#pi.has_mul

#### Adam Topaz (Dec 08 2020 at 16:33):

Not exactly. There's this `pi_instance`

tactic that makes instances (usually of algebraic nature) for Pi-types automatically. I want something which is even simpler -- a tactic that does this for binary products (which mathematically are a special case of Pi-types, but not definitionally so).

#### Eric Wieser (Dec 08 2020 at 16:37):

Got it - so you want a `prod_instance`

tactic for building the proofs with instances over `prod A B`

?

#### Eric Wieser (Dec 08 2020 at 16:37):

(deleted)

#### Eric Wieser (Dec 08 2020 at 16:38):

Based on the content of `algebra/group/prod`

we don't have one: https://github.com/leanprover-community/mathlib/blob/3996bd428d1758fa6f790a2453bd679e10ad1897/src/algebra/group/prod.lean

#### Yury G. Kudryashov (Dec 09 2020 at 02:24):

Note that currently `pi_instance`

generates extra `id`

s, so we use it only to prove properties.

Last updated: May 16 2021 at 05:21 UTC