coe vs val naming

Stream: mathlib4

[Yakov Pechersky]

@Yury G. Kudryashov , in !4#1795, you named

#align filter.map_coe_Ioi_at_top Filter.map_val_Ioi_atTop

but in !4#2052

#align map_coe_Iio_at_top map_coe_Iio_atTop

Note that the former renames coe to val but the latter doesn't. This is a question for !4#3988

[Yury G. Kudryashov]

I don't know what's right. I changed coe to val sometimes.

[Mario Carneiro]

the official recommendation is to use the name of the function after coes are unfolded, because that's what is actually in the term in lean 4

[Mario Carneiro]

that function might itself be named coe of some kind, but if it is named val then you should use val in theorems