Failed to synthesize AddTorsor

Stream: mathlib4

[Stephan Maier]

Hi, I have tried to make the following code compile (note, it works in the online editor but for the problem I am about to describe). I get the message 'failed to synthesize AddTorsor ↥a.direction ↥a'. This is puzzling as the AddTorsor is actually given by AffineSubspace.toAddTorsor as used below.
Thanks for any hint the might help to resolve the situation.
Cheers, Stephan

import Mathlib

class XXX
  (𝕜x : Type*) [LinearOrderedField 𝕜x]
  {Vx : Type*} [AddCommGroup Vx] [Module 𝕜x Vx]
  (Px : Type*) [AddTorsor Vx Px]: Prop

variable {𝕜 : Type*} [LinearOrderedField 𝕜]
variable {V : Type*} [AddCommGroup V] [Module 𝕜 V]
variable {P : Type*} [AddTorsor V P]

set_option diagnostics true
theorem xxx {a : AffineSubspace 𝕜 P} [hane : Nonempty a] (x : XXX 𝕜 P) :
    @XXX 𝕜 _ ↥a.direction _ _ ↥a a.toAddTorsor where --check the comment that is shown at "where"

[Eric Wieser]

This is the same issue that @Yaël Dillies ran into the other day. If you pass a typeclass argument manually, then you can't use where notation

[Yaël Dillies]

#lean4 > Non-canonical instances kill where notation

[Stephan Maier]

Eric Wieser said:

This is the same issue that Yaël Dillies ran into the other day. If you pass a typeclass argument manually, then you can't use where notation

Great, what a speedy reply! Thanks. The discussion is pretty involved. The question is whether there is a way to get round the problem? Any thoughts? What I need is simply this: I am working in an affine space, but all objects of concern happen to live in an affine subspace. I wish to pass to this affine subspace (for example, it may be finite dimensional and that helps the maths etc.). It appears that there is no way around using toAddTorsor...

[Eric Wieser]

I think the usual approach in your specific case is to attribute [local instance] AffineSubspace.toAddTorsor

[Stephan Maier]

Eric Wieser said:

attribute [local instance] AffineSubspace.toAddTorsor

Yeah! The following compiles! I will check if it does what it is intended to do. Lean is full of pleasant surprises ;-)
Sorry to ask: Why does this work? A reference I could check?

import Mathlib

class XXX
  (𝕜x : Type*) [LinearOrderedField 𝕜x]
  {Vx : Type*} [AddCommGroup Vx] [Module 𝕜x Vx]
  (Px : Type*) [AddTorsor Vx Px]: Prop

variable {𝕜 : Type*} [LinearOrderedField 𝕜]
variable {V : Type*} [AddCommGroup V] [Module 𝕜 V]
variable {P : Type*} [AddTorsor V P]

attribute [local instance] AffineSubspace.toAddTorsor
theorem xxx {a : AffineSubspace 𝕜 P} [hane : Nonempty a] (x : XXX 𝕜 P) :
    @XXX 𝕜 _ ↥a.direction _ _ ↥a a.toAddTorsor where

[Eric Wieser]

You can also drop the @ now

[Stephan Maier]

Eric Wieser said:

You can also drop the @ now

Yeah. It works. In pactice, I have more stuff to pass on. Is there a way to pass the (relative) topology also using an attribute-trick to bypass the @ ?

import Mathlib

class XXX
  (𝕜x : Type*) [LinearOrderedField 𝕜x]
  {Vx : Type*} [AddCommGroup Vx] [Module 𝕜x Vx]
  (Px : Type*) [AddTorsor Vx Px] [TopologicalSpace Px] : Prop

variable {𝕜 : Type*} [LinearOrderedField 𝕜]
variable {V : Type*} [AddCommGroup V] [Module 𝕜 V]
variable {P : Type*} [AddTorsor V P] [top : TopologicalSpace P]

attribute [local instance] AffineSubspace.toAddTorsor
--attribute [local instance] TopologicalSpace.induced
theorem xxx {a : AffineSubspace 𝕜 P} [hane : Nonempty a] (x : XXX 𝕜 P) :
    @XXX 𝕜 _ _ _ _ a _ (TopologicalSpace.induced a.subtype top) where

[Eric Wieser]

I think you can safely make that a global instance

[Eric Wieser]

instance AffineSubspace.instTopologicalSpace : TopologicalSpace s := .induced s.subtype inferInstance or similar

[Stephan Maier]

Eric Wieser said:

I think you can safely make that a global instance

Thanks, Eric. Will do. I was trying to avoid this as it sometimes is hard to track what kind of behaviour this generates elsewhere. The more local the better. But there is a limit to using the tedious @ !
Yours, Stephan