Topology.Algebra.MulAction !4#2013

Stream: mathlib4

[Moritz Doll]

In this PR there is one error left and I have no idea how to fix it: we have a statement about continuity with a specific topology, but in the proof Lean seems to forget what the topology is supposed to be. Code:
https://github.com/leanprover-community/mathlib4/pull/2013/files#diff-6fbe09f46d499557f39aa50ba472af8c50434af5f30365bcb77c018bf486c7ceR178-R187

[Eric Wieser]

This is a known problem, {} notation for constructors doesn't work when the instance arguments to the constructor aren't canonical

[Eric Wieser]

I pushed a fix

[Moritz Doll]

I've tried it with ⟨..⟩, but that did not work either. It did not cross my mind to use ContinuousSMul.mk. To me it sounds that this is a Lean error, right?

[Eric Wieser]

I asked about this before, it's apparently somewhat by design

[Eric Wieser]

There's a thread I can't search for on mobile about (_)

[Yury G. Kudryashov]

You can do, e.g., letI := yourInstance; { ... }

[Kevin Buzzard]

Eric Wieser said:

This is a known problem, {} notation for constructors doesn't work when the instance arguments to the constructor aren't canonical

What does canonical mean in this context?

[Yury G. Kudryashov]

"Canonical" means "can be found by instance search, not unification"