Apply a function to both sides of an equality relationship

Stream: new members

[Ryan Smith]

Specific question but broader context:

If I have (z w : \C) and I have (h : z = w), is there an obvious way to get z.re = w.re ? In this specific case there may be a theorem for it but I've also had examples where I had matrix equality and wished to deduce that their traces as the same. It almost seems like a meta theorem that equality is preserved under any well defined function, so is what I'm looking for a theorem or maybe a tactic?

[Aaron Liu]

congrArg Complex.re h

[Weiyi Wang]

or apply_fun Complex.re at h as a tactic (didn't test if this works)

[Heather Macbeth]

The slick way, which works even to apply several functions in succession to several hypotheses, is congr(Complex.re $h) (more generally, congr(f $h1 / 6 + 3 + $h2))

[Ryan Smith]

Are those tactics? The apply_fun method seems to work to allow me to rewrite hypotheses, which can be nice. congr seems invalid for rewriting?

[Kevin Buzzard]

If you're not sure how to use something then one tip is to search for it in mathlib and see how others are using it.

[Robin Arnez]

Ryan Smith schrieb:

congr seems invalid for rewriting?

congr(...) is a term, so e.g. have h' := congr(Complex.re $h)

[Kenny Lau]

congr(($h).re)