chore(logic/function/basic): Add function.update_apply (#5093)
chore(logic/function/basic): Add function.update_apply (#5093)

This makes it easier to eliminate `dite`s in simple situations when only `ite` is needed.






leanprover-community/mathlib,leanprover-community/mathlib