## 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


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_monoids, 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