## Stream: general

### Topic: Type error on dfinsupp add

#### Eric Wieser (Apr 22 2021 at 11:07):

How can I write this theorem statement in a way that will be accepted by the elaborator?

import data.dfinsupp
import data.finsupp.basic

variables {ι : Type*} {M : Type*}

/-- Interpret a homogenous dfinsupp as a finsupp. -/
def dfinsupp.to_finsupp [decidable_eq ι] [has_zero M] [Π m : M, decidable (m ≠ 0)]
(f : Π₀ i : ι, M) : ι →₀ M :=
⟨f.support, f, λ i, by simp only [dfinsupp.mem_support_iff]⟩

def my_add [add_zero_class M] (f g : Π₀ i : ι, M) : Π₀ i : ι, M := f + g

#lint -- all the arguments above were necessary

-- yet lean can't resolve this addition
@[simp] lemma to_finsupp_add [decidable_eq ι] [add_zero_class M] [Π m : M, decidable (m ≠ 0)]
(f g : Π₀ i : ι, M) :
dfinsupp.to_finsupp (f + g) = (f.to_finsupp + g.to_finsupp : ι →₀ M) :=
sorry -- finsupp.coe_fn_injective rfl would solve this if the statement were accepted


#### Eric Wieser (Apr 22 2021 at 11:09):

The word lemma gives me the error:

type mismatch at application
f.to_finsupp
term
f
has type
Π₀ (i : ι), M : Type (max u_1 u_2)
but is expected to have type
Π₀ (i : ?m_1), ?m_2 : Type (max ? ?)
Untitled-2: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch at application
f.to_finsupp
term
f
has type
Π₀ (i : ι), M : Type (max u_1 u_2)
but is expected to have type
Π₀ (i : ?m_1), ?m_2 : Type (max ? ?)


and the + give me four errors, all roughly

type mismatch at application
term
f
has type
Π₀ (i : ι), M : Type (max u_1 u_2)
but is expected to have type
Π₀ (i : ?m_1), ?m_2 : Type (max ? ?)


#### Eric Wieser (Apr 22 2021 at 11:25):

If I add underscores everywhere then it works:

@[simp] lemma to_finsupp_add [add_zero_class M] [Π m : M, decidable (m ≠ 0)] (f g : Π₀ i : ι, M) :
@dfinsupp.to_finsupp _ M _ _ _ (f + g) =
(@dfinsupp.to_finsupp _ M _ _ _ f + @dfinsupp.to_finsupp _ M _ _ _ g : ι →₀ M) :=
finsupp.coe_fn_injective $dfinsupp.coe_add _ _  What's going on here? Why can't it infer M from the types of f and g? #### Eric Wieser (Apr 22 2021 at 11:34): It also seems there are different elaboration rules for dot notation - this works, but changing any of the to_finsupp calls to use dot notation fails: @[simp] lemma to_finsupp_add [add_zero_class M] [Π m : M, decidable (m ≠ 0)] (f g : Π₀ i : ι, M) : (dfinsupp.to_finsupp (f + g) : ι →₀ M) = (dfinsupp.to_finsupp f + dfinsupp.to_finsupp g) := finsupp.coe_fn_injective$ dfinsupp.coe_add _ _


Last updated: Aug 03 2023 at 10:10 UTC