typeclass instance problem with singleton

Stream: mathlib4

[Maxwell Thum]

theorem smul_singleton : s • {b} = (· • b) '' s is giving me

typeclass instance problem is stuck, it is often due to metavariables
  Singleton β ?m.3944

The type should be Set \b, right? If so, how do I tell Lean this?

[Heather Macbeth]

@Maxwell Thum Please give imports or a link to the line in a branch.

[Maxwell Thum]

The imports are

import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Set.Pairwise
import Mathlib.Data.Set.Pointwise.Basic
import Mathlib.Tactic.ByContra

[Maxwell Thum]

Here is a link to the line in a recent PR (I think) https://github.com/leanprover-community/mathlib4/pull/1473/commits/813e3d1c41c962f98567d495a03b5d5643c91d4c#diff-bb3fe98a6d8a82c76f7f4bd9412449f57c1e421d63c526705c14dab92432dc86R138

[Heather Macbeth]

That link doesn't work, but this does:
https://github.com/leanprover-community/mathlib4/blob/813e3d1c41c962f98567d495a03b5d5643c91d4c/Mathlib/Data/Set/Pointwise/Smul.lean#L138

[Heather Macbeth]

However, it looks like that branch isn't up to date with any work you have done. Can you please push so we can look at it in context?

[Heather Macbeth]

Alternatively, provide a #mwe (the imports, but also variable declarations, etc).

[Maxwell Thum]

I don't think I've significantly changed the context, but I'll still push; I'll just be a minute.

[Maxwell Thum]

Okay, here it is. https://github.com/leanprover-community/mathlib4/blob/port/Data.Set.Pointwise.Smul/Mathlib/Data/Set/Pointwise/Smul.lean#L144

[Heather Macbeth]

Maxwell Thum said:

I don't think I've significantly changed the context

(You changed [HasSmul α β] to [SMul α β], which made the line make sense!)

[Heather Macbeth]

Maxwell Thum said:

The type should be Set \b, right? If so, how do I tell Lean this?

OK, yes. You want

theorem smul_singleton : s • ({b} : Set β) = (· • b) '' s :=

[Heather Macbeth]

It's unfortunate that this change is needed, but my guess is that it falls into a well-known class of behaviour where Lean 4 (unlike Lean 3) can't use one side of an equation to help elaborate the other. (edit: see below)

[Maxwell Thum]

Perfect; thank you!

[Heather Macbeth]

Actually, I don't think I've seen this problem before. Does anyone want to try to make an import-free example? This fails in Lean 4:

import Mathlib.Data.Set.NAry
import Mathlib.Algebra.Group.Defs

variable [SMul α β] {s : Set α} {b : β}

instance Set.hasSmul : SMul (Set α) (Set β) := ⟨Set.image2 SMul.smul⟩

example : Set β := s • {b} -- fails

and this works in Lean 3:

import data.set.n_ary
import algebra.group.defs

variables {α β : Type} [has_smul α β] {s : set α} {b : β}

instance Set.hasSmul : has_smul (set α) (set β) := ⟨set.image2 has_smul.smul⟩

example : set β := s • {b}

[Heather Macbeth]

I notice that this works in Lean 4:

example : Set β := SMul.smul s {b}

So maybe the problem is our having added the extra layer of HSMul. I'm really not convinced that change was a good idea ...