## Stream: new members

### Topic: Apply function on both sides of equality

#### Pedro Minicz (May 19 2020 at 02:17):

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 (May 19 2020 at 02:19):

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

#### Pedro Minicz (May 19 2020 at 02:24):

Thank you! Are there any alternatives?

#### Yury G. Kudryashov (May 19 2020 at 02:26):

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

#### Yury G. Kudryashov (May 19 2020 at 02:28):

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 (May 19 2020 at 02:44):

You can also rw <- h for a similar result

Last updated: May 12 2021 at 05:19 UTC