apf function/tactic?

Stream: lean4

[Siddhartha Gadgil]

Sorry for a basic question: what is the "apf" function in lean 4, deducing f(a) = f(b) from a = b (I searched documentation and could not easily find it). Alternatively a tactic for this.

[Mario Carneiro]

that theorem is usually called congrArg

[Mario Carneiro]

I don't know what "apf" is, is that the HoTT name?

[Mario Carneiro]

the tactic is congr in lean 3 but I'm not sure lean 4 has it yet

[Siddhartha Gadgil]

Thanks. Just found that in the source. Yes congrArg is what I need.
Yes, the "HoTT" name.

[Sebastian Ullrich]

Rewriting with rw or simp usually obviates the need for congrArg/Fun