# Zulip Chat Archive

## Stream: Is there code for X?

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

#### Eric Wieser (Jul 21 2020 at 11:39):

Is there anything in mathlib resembling the sorry here?

```
import data.dfinsupp
import tactic
universes u v w
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
```

#### Scott Morrison (Jul 21 2020 at 12:29):

Quite possibly not. `dfinsupp`

is not very well developed.

#### Eric Wieser (Jul 21 2020 at 14:07):

Is `≃`

the right statement to try to make?

#### Scott Morrison (Jul 21 2020 at 14:10):

Depends what you need it for. Lots of algebra structures are going to be compatible with this equivalence, too.

#### Eric Wieser (Jul 21 2020 at 16:26):

I can make a start on this with:

```
def prod_to_nested (f : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j := begin
fapply quotient.lift_on f,
exact λ fij, ⟦{
to_fun := λ i, ⟦ {
to_fun := λ j, fij.to_fun (i, j),
pre_support := fij.pre_support.map (λ (ij : ii × jj), ij.snd),
zero := λ j, begin
obtain hin | h0 := fij.zero (i, j),
{apply or.inl, rw multiset.mem_map, use (i, j), simp only [hin, eq_self_iff_true, and_self]},
{exact or.inr h0},
end
} ⟧,
pre_support := fij.pre_support.map (λ ij, ij.fst),
zero := λ i, begin
have h := λ j, fij.zero (i, j),
rw multiset.mem_map,
sorry
end
}⟧,
exact λ a b H, quotient.sound $ λ i, by {
simp [H (i, _)],
exact λ j, by simp [H (i, j)]
},
end
```

although this all feels super awkward

#### Eric Wieser (Jul 21 2020 at 18:27):

Updated the above to be sorry-free, would appreciate feedback on whether I'm missing a trick.

In paticular, the ` λ j, (fij.zero (i, j)).elim`

proof is repeated twice, and I'm not sure how to remove it.

#### Eric Wieser (Jul 21 2020 at 19:30):

The other direction is proving even more challenging:

```
def nested_to_prod (f : Π₀ i j, β i j) : Π₀ (ij : ii × jj), β ij.1 ij.2 := begin
fapply quotient.lift_on f,
{
intro fi,
refine ⟦{
to_fun := λ ij, fi.to_fun ij.fst ij.snd,
pre_support := fi.pre_support.product (begin
let j_sets := fi.pre_support.map (λ i, begin
let fi_val := (fi.to_fun i),
/- This is unprovable, I think lift_on is the wrong approach, or I need to return a clever quotient -/
exact quotient.lift_on fi_val
dfinsupp.pre.pre_support
(λ a b H, begin
sorry
end)
end),
/- should be union of j_sets -/
exact (sorry : multiset jj),
end),
zero := λ ij, begin
rw multiset.mem_product,
cases fi.zero ij.fst,
{ left, simp [h], sorry},
{ right, simp [h] }
end
}⟧,
},
exact λ a b H, quotient.sound $ λ ij, by simp [H ij.fst],
end
```

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

Would this be more suited to #general, now that it's established the answer to "is there code for X in mathlib" is no?

#### Johan Commelin (Jul 22 2020 at 11:52):

Yes, or `#maths`

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

Shall I repost, or ask someone with the magic bit to move it?

#### Johan Commelin (Jul 22 2020 at 11:52):

I think reposting is easier

#### Johan Commelin (Jul 22 2020 at 11:52):

Just add a link to this thread

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

Last updated: May 07 2021 at 21:10 UTC