Zulip Chat Archive

Stream: new members

Topic: Apply function on both sides of equality


view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 19 2020 at 02:19):

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

view this post on Zulip Pedro Minicz (May 19 2020 at 02:24):

Thank you! Are there any alternatives?

view this post on Zulip Yury G. Kudryashov (May 19 2020 at 02:26):

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

view this post on Zulip 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)

view this post on Zulip 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