Apply function on both sides of equality

Stream: new members

[Pedro Minicz]

Say I have a = b * c as my goal, with a b c : ℝ and h : a / c = b as my hypothesis. How do I apply λ x, x * c to both sides of h? There was a thread asking this very question a few days ago, but I didn't manage to find it.

[Yury G. Kudryashov]

https://leanprover-community.github.io/mathlib_docs/tactics.html#apply_fun

[Pedro Minicz]

Thank you! Are there any alternatives?

[Yury G. Kudryashov]

replace h := congr_arg (λ x, x * c) h

[Yury G. Kudryashov]

In this particular case you can also apply a lemma (search with #library_search or guess name like eq_mul_of_div_eq - not tested)

[Reid Barton]

You can also rw <- h for a similar result