## Stream: general

### Topic: Combination of finsupp and dfinsupp

#### Antoine Labelle (Sep 28 2022 at 02:51):

The following is not found by apply_instance. What's the easiest way to prove it?

import linear_algebra.dfinsupp

variables (R : Type*) [add_comm_monoid R]
variables {ι : Type*} (α : ι → Type*)

example : add_comm_monoid (Π₀ i, (α i →₀ R)) := sorry


#### Heather Macbeth (Sep 28 2022 at 03:19):

@Antoine Labelle This is a common problem with the direct sum. The instance is there, docs#dfinsupp.add_comm_monoid, but doesn't elaborate for some reason.

#### Heather Macbeth (Sep 28 2022 at 03:20):

My usual workaround is to write a bunch of rubbish with @ to help Lean find it ... not sure if there's a better way.

#### Adam Topaz (Sep 28 2022 at 03:24):

In this case you could also use docs#direct_sum

#### Adam Topaz (Sep 28 2022 at 03:25):

import linear_algebra.dfinsupp
import linear_algebra.direct_sum.finsupp

variables (R : Type*) [add_comm_monoid R]
variables {ι : Type*} (α : ι → Type*)

open_locale direct_sum

example : add_comm_monoid (⨁ (i : ι), ⨁ (j : α i), R) := infer_instance

noncomputable
example : add_comm_monoid (⨁ (i : ι), α i →₀ R) := infer_instance


#### Adam Topaz (Sep 28 2022 at 03:25):

(which is defined with dfinsupp btw)

#### Adam Topaz (Sep 28 2022 at 03:25):

One sec, let me fix that code with the proper notation (fixed)

#### Antoine Labelle (Sep 28 2022 at 04:05):

@Adam Topaz I also asked a question about the use of direct_sum versus dfinsupp (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/direct_sum.20vs.20dfinsup), so if you want to explain what direct_sum does differently I would be interested.

#### Eric Wieser (Sep 28 2022 at 08:34):

Instead of adding a bunch of @s to help lean find it, you can also track down which instance it is that lean can't find, and add instance : the_missing_one := @the_existing_one _ _ _ ...

#### Riccardo Brasca (Sep 28 2022 at 08:37):

As a mathematician, I would say we should add all these instances, and use direct_sum in doing mathematics.

#### Eric Wieser (Sep 28 2022 at 08:46):

I think there are infinitely many such missing instances, so at best we can add them as we need them

#### Eric Wieser (Sep 28 2022 at 08:46):

I think Lean 4 fixes the bug causing the issue

#### Antoine Labelle (Sep 29 2022 at 00:23):

I tried adding the instance used by docs#dfinsupp.add_comm_monoid, but I get weird problems when I try to do this for modules. In the following code, the two definitions compile correctly but the second haveI in tactic environment fails. Any ideas?

import linear_algebra.dfinsupp

variables (R : Type*) [semiring R]
variables {ι : Type*} (α : ι → Type*)

noncomputable
def example1 : Π i, add_comm_monoid (α i →₀ R) := λ i, by apply_instance

noncomputable
def example2 : Π i, module R (α i →₀ R) := λ i, by apply_instance

include R ι α

example : true :=
begin
-- The second line fails, but it succeeds if I remove the first line.
haveI : Π i, add_comm_monoid (α i →₀ R) := λ i, by apply_instance,
haveI : Π i, module R (α i →₀ R) := λ i, by apply_instance,
end


#### Yaël Dillies (Sep 29 2022 at 06:29):

What happens if you replace the first haveI by letI?

#### Antoine Labelle (Sep 29 2022 at 13:01):

It works, thanks!

#### Eric Wieser (Sep 29 2022 at 14:25):

You should replace both!

#### Anne Baanen (Sep 29 2022 at 14:27):

The technical reason is that haveI, like lemma, forgets the definition, so it's like assuming each add_comm_monoid (α i →₀ R) has some random unknown add_comm_monoid structure. letI remembers that the add_comm_monoid structure actually derives from finsupp.

#### Anne Baanen (Sep 29 2022 at 14:27):

Basically, use haveI only with classes that live in Prop.

#### Antoine Labelle (Sep 29 2022 at 14:35):

I see, thanks for the explanation.

#### Yaël Dillies (Sep 29 2022 at 16:04):

Anne Baanen said:

Basically, use haveI only with classes that live in Prop.

This is a valid rule when proving a lemma, but the real rule is more "Use haveI unless you want to access the definition" because letI adds a let binding which will mess your defeq if you're constructing a definition.

Last updated: Dec 20 2023 at 11:08 UTC