Coercion of pi types by coercing their return type

Stream: general

[Eric Wieser]

Currently, lean/mathlib won't automatically coerce f : Π i j, i ≤ j → G i →+* G j to Π i j, i ≤ j → G i → G j, which requires me to write the clumsy (λ i j h, f i j h) whenever I want the coercion.

• Is this something we should fix by defining a has_coe instance for pi types in mathlib?
• Is this something that lean 4 could improve?
• Or is having this happen automatically just a bad idea?