Function.uncurry_curry does not require funext

Stream: lean4

[Tasiro]

I just noticed that since Lean supports eta-conversion, Function.uncurry_curry does not actually require a funext, because rfl is enough. That should probably also be the case for the same theorem for Sigma in Mathlib.

Does this actually make a difference somewhere (maybe because funext uses Quot.sound)?

[Eric Wieser]

Changing proofs to rfl is generally a (small) improvement, since then they can be used by dsimp.

[Eric Wieser]

But otherwise de-funexting proofs is not worth anyone's time to review