Unique differentiability and definitional equality

Stream: maths

[Gabriel Ebner]

The types Π i, E i and pi_Lp p hp E are definitionally equal, but they have different norms (L^∞ and L^p, resp.). Is there a reason why unique_diff_on (s : Π i, E i) and unique_diff_on (s : pi_Lp p hp) should be definitionally equal?
(It is clear that they should be equivalent because everything is finite-dimensional. I'm asking because this broke while debugging #7124. Apparently you could use a proof of unique_diff_on for L^∞ where a proof for L^2 was expected.)

[Gabriel Ebner]

On second thought, this is probably because unique_diff_on never mentions the norm of the tuple, and the topologies are definitionally equal.

[Sebastien Gouezel]

I had never noticed that this definition only depends on the topology! We should probably refactor the typeclasses in unique_diff_on to make this more obvious.

[Yury G. Kudryashov]

/me used unique_diff_on.pi without realizing that Lean does some heavy identifying under the hood.