Conversions on an application head

Stream: lean4

[Son Ho]

If I have a term of the shape f x, is there a conversion which allows me to apply rewritings to f? I see I can use arg or congr to modify x, but I couldn't find a conversion which allows me to access the head of an application.

[Jireh Loreaux]

there's docs4#congr_fun (or docs4#congrFun), or you can just use the rw tactic.

[Jireh Loreaux]

If you are dealing with a bundled morphism from mathlib, then you may need docs4#FunLike.congr_fun

[Son Ho]

I hadn't understood we could directly apply theorems when performing conversions... That's perfect, thanks!