Function for taking apart applications

Stream: lean4

[Dominique Danco]

Does anyone know if a function exists that takes apart a chain of applications up to computation? Similar to this function in mathlib3: https://github.com/leanprover-community/mathlib/blob/54619e055bd8c9395572508c20fb2640f15b86dc/src/tactic/core.lean#L331