# Zulip Chat Archive

## Stream: general

### Topic: finset.prod and fin.cons

#### Yury G. Kudryashov (Jun 12 2020 at 05:10):

I'm trying to formulate a `simp`

lemma:

```
import data.fintype.card
open_locale big_operators
theorem fin.prod_univ_cons {M : Type*} [comm_monoid M] {n : ℕ} (x : M) (f : fin n → M) :
∏ i : fin (n + 1), (@fin.cons _ (λ _, M) x f i) = x * ∏ i : fin n, f i :=
sorry
```

and get the following error:

```
6:3: type mismatch at application
∏ (i : fin (n + 1)), fin.cons x f i
term
λ (i : fin (n + 1)), fin.cons x f i
has type
Π (i : fin (n + 1)), (λ (_x : fin (n + 1)), M) i : Type ?
but is expected to have type
fin (n + 1) → ?m_1 : Type ?
```

#### Yury G. Kudryashov (Jun 12 2020 at 05:11):

It seems that Lean can't unify `(λ _, β) i`

with `β`

. Is there any way to add this lemma without adding a non-dependent version of `fin.cons`

?

#### Mario Carneiro (Jun 12 2020 at 05:42):

give it the expected type

#### Mario Carneiro (Jun 12 2020 at 05:43):

```
theorem fin.prod_univ_cons {M : Type*} [comm_monoid M] {n : ℕ} (x : M) (f : fin n → M) :
(∏ i : fin (n + 1), @fin.cons _ (λ _, M) x f i : M) = x * ∏ i : fin n, f i :=
sorry
```

#### Mario Carneiro (Jun 12 2020 at 05:43):

`fin.cons`

should be `@[elab_as_eliminator]`

#### Yury G. Kudryashov (Jun 12 2020 at 05:56):

Do you mean `local attribute [elab_as_eliminator] fin.cons`

?

#### Yury G. Kudryashov (Jun 12 2020 at 05:57):

If I add `@[elab_as_eliminator]`

to the definition, the next few lemmas fail.

#### Mario Carneiro (Jun 12 2020 at 06:11):

I mean global `@[elab_as_eliminator]`

#### Mario Carneiro (Jun 12 2020 at 06:15):

Oof, yeah these are messy. I think either `cons`

should take an explicit motive argument, or it should be nondependent

#### Yury G. Kudryashov (Jun 12 2020 at 06:16):

@Sebastien Gouezel you use `fin.cons`

a lot in `multilinear`

maps. What's your experience? How often did you hit something like the issue described above?

#### Johan Commelin (Jun 12 2020 at 07:13):

Isn't that lemma already there?

#### Johan Commelin (Jun 12 2020 at 07:14):

I think I used the sum version last week

#### Johan Commelin (Jun 12 2020 at 07:16):

Nevermind, I was confusing it with src#fin.prod_univ_succ

#### Sebastien Gouezel (Jun 12 2020 at 07:33):

Yes, I encountered several times the issue that `(λ _, β) i`

and `β`

don't always unify. Since `fin.cons`

doesn't have too many implicit arguments, it wasn't too painful to provide explicitly the type to the `@`

version, though, and to add type annotations where necessary.

Last updated: Dec 20 2023 at 11:08 UTC