# Zulip Chat Archive

## Stream: maths

### Topic: dfinsupp of product is dfinsupp of dfinsupp

#### Eric Wieser (Jul 22 2020 at 11:57):

I'm trying to obtain the equivalence in the following, `(Π₀ (ij : ii × jj), β ij.1 ij.2) ≃ (Π₀ i j, β i j)`

```
import data.dfinsupp
universes u v w
-- requirements of Π₀
variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii → jj → Type w) [Π i j, has_zero (β i j)]
example : (Π₀ (ij : ii × jj), β ij.1 ij.2) ≃ (Π₀ i j, β i j) := sorry
```

I initially posted this over at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/dfinsupp.20of.20product.20is.20dfinsupp.20of.20dfinsupp/near/204537032.

Over there, you can see a definition of the forward transformation, `(Π₀ (ij : ii × jj), β ij.1 ij.2)) → (Π₀ i, Π₀ j, β i j)`

, but I'm struggling to de-sorry the reverse transformation.

I suspect my issue here is a lack of familiarity with quotient types in lean.

Help finishing those definitions would be greatly appreciated!

#### Reid Barton (Jul 22 2020 at 11:58):

do you need this for a random `β`

, or are they actually at least `add_comm_monoid`

?

#### Eric Wieser (Jul 22 2020 at 11:59):

Ideally a random `β`

#### Eric Wieser (Jul 22 2020 at 11:59):

I think the add_comm_monoid version probably applies better to `direct_sum`

than to `dfinsupp`

#### Eric Wieser (Jul 22 2020 at 12:01):

I was also trying to avoid needing the decidability of `{f : β i j}, f = 0`

, which is required if I try to use `.support`

#### Eric Wieser (Jul 22 2020 at 12:02):

(hence my attempts to go through `pre_support`

instead.)

#### Eric Wieser (Jul 22 2020 at 14:45):

I've made a PR at https://github.com/leanprover-community/mathlib/pull/3515 which contains the bits of the proof I was able to put together, so that it's not completely lost to zulip streams.

#### Utensil Song (Jul 23 2020 at 12:01):

I don't understand why there would be "goals accomplished" and

```
tactic failed, result contains meta-variables
state:
no goals
```

at the same time for the following #mwe related to this PR:

#### Utensil Song (Jul 23 2020 at 12:02):

```
import data.dfinsupp
import tactic
universes u v w
namespace dfinsupp.prod
variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables {β : ii → jj → Type w} [Π i j, has_zero (β i j)]
def prod_to_nested (f : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j := begin
apply quotient.lift_on f,
intros a b h,
unfold has_equiv.equiv at h,
unfold setoid.r at h,
apply quotient.sound,
intro i,
simp [h], -- goals accomplished
end -- result contains meta-variables
```

#### Anne Baanen (Jul 23 2020 at 12:04):

This happens when tactics claim to have solved all the metavariables (i.e. there are no more goals), but there are still metavariables that need to be filled out. You can use the `recover`

tactic to get the missing goal.

#### Anne Baanen (Jul 23 2020 at 12:08):

More specifically, the line `apply quotient.sound,`

causes a goal to be hidden, I guess because the tactic expects that it will be filled by unification. If you write `refine quotient.sound _,`

instead, the goal will still be around.

#### Chris Hughes (Jul 23 2020 at 15:52):

I did manage to prove this, but it's not pretty (link). I think this might be a case of the #xy problem. `dfinsupp`

is not really intended to be used unless the `β i`

are `add_comm_monoid`

s, in fact it shouldn't really be used directly as `dfinsupp`

, but you should use `direct_sum`

instead most of the time for the interface. It is strange to want to use it with just `has_zero`

, and the library really isn't set up for that usage.

#### Eric Wieser (Jul 23 2020 at 21:59):

This is just an x problem, I decided it was more challenging than my original y problem

#### Eric Wieser (Jul 24 2020 at 07:42):

Although I think if you're willing to assume`[Π i j, decidable_eq (β i j)]`

, there are some shorter solutions - my difficulty was trying to avoid that assumption

Last updated: May 14 2021 at 20:13 UTC