!4#4345 Analysis.NormedSpace.PiLp

Stream: mathlib4

[Ruben Van de Velde]

I have a rfl failing here that I don't really know how to debug, if anyone feels like taking a look

[Jireh Loreaux]

@Ruben Van de Velde I haven't understood what's going on completely, but I have a proof that compiles (very ugly). My guess is that this is a result of some interplay between new structures (since a LinearIsometryEquiv extends LinearEquiv) and maybe Lean not seeing a term of PiLp as a function (note that the second ext was necessary in order for the LinearEquiv.PiCongrLeft'_symm_apply to apply.

[Jireh Loreaux]

So, this needs some more love, but hopefully it helps for the next person who takes a look.

[Ruben Van de Velde]

Thanks! I'll try and take a look later tonight if nobody beats me to it