EqOnSource.symm / .trans

Stream: Is there code for X?

[Winston Yin (尹維晨)]

Is there any reason why there are no symm / trans lemmas for PartialEquiv.EqOnSource and PartialHomeomorph.EqOnSource? I would have to rely on Setoid.symm and Setoid.trans from their setoid instances, but that's not obvious at all. It would be nice to be able to write h.symm or h.trans h' where h : e ≈ e' and h' : e' ≈ e''.

My second question is why dot notation doesn't work in the following:

import Mathlib.Logic.Equiv.PartialEquiv

theorem PartialEquiv.EqOnSource.symm {α β : Type*} {e e' : PartialEquiv α β} (h : e ≈ e') : e' ≈ e :=
  Setoid.symm h

variable {e e' : PartialEquiv α β} (h : e ≈ e')
#check h.symm -- invalid field notation, function 'PartialEquiv.EqOnSource.symm' does not have argument with type (PartialEquiv.EqOnSource ...) that can be used, it must be explicit or implicit with a unique name

but the following works:

theorem PartialEquiv.EqOnSource.symm {α β : Type*} {e e' : PartialEquiv α β} (h : PartialEquiv.EqOnSource e e') : e' ≈ e :=
  Setoid.symm h

variable {e e' : PartialEquiv α β} (h : e ≈ e')
#check h.symm -- works

[Yury G. Kudryashov]

It used to work with dot notation in Lean 3 (at least, community edition).

[Yury G. Kudryashov]

While porting, we tried not to change API.

[Winston Yin (尹維晨)]

Did .symm and .trans work automatically for any instance of Setoid?

[Yury G. Kudryashov]

The dot notation doesn't work because Lean looks for an argument of type PartialEquiv.EqOnSource without unfolding any definitions.

[Yury G. Kudryashov]

Winston Yin (尹維晨) said:

Did .symm and .trans work automatically for any instance of Setoid?

Not tested and I doubt that: the type of e ≈ e' is not Setoid. One possible solution is to drop the instances and add notations.

[Yury G. Kudryashov]

But this should be discussed with other active users of PartialEquivs/PartialHomeomorphs before you start working on this.

[Winston Yin (尹維晨)]

This kind of instance/notation refactor is currently beyond me...