## Stream: new members

### Topic: rewriting and let

#### Robin Carlier (Jun 25 2021 at 18:56):

Hi ! stupid question, but is there a way to rewrite some equality that I defined using let? Say I have a goal foo = blah, and I do let bar := blah before_hand, how do I rewrite my goal as foo = bar?

#### Robin Carlier (Jun 25 2021 at 18:57):

I tried to just rw bar but Lean did not like it.

#### Ruben Van de Velde (Jun 25 2021 at 18:58):

change would work

#### Damiano Testa (Jun 25 2021 at 18:59):

I think that set [...] with h, instead of let, will produce a hypothesis h that you can use for rw.

#### Ruben Van de Velde (Jun 25 2021 at 18:59):

Alternatively, if you use set bar := blah with hbar,, you can use rw ←hbar,

#### Robin Carlier (Jun 25 2021 at 19:02):

Nice! So set works just like let? In practice, is it better to avoid let?

#### Ruben Van de Velde (Jun 25 2021 at 19:05):

I personally tend to avoid let, but I don't think that's mathlib policy, at least

#### Eric Rodriguez (Jun 25 2021 at 19:23):

I also tend to avoid let because of the aforementioned finickyness, but also simp_rw and simp only work to rewrite them

#### Robin Carlier (Jun 25 2021 at 19:30):

Thank you! I have a last silly question: is there a canonical syntax for turning an hypothesis of the form f = g where f and g are functions into an hypothesis of the form f x = g x (given some xin the domain of course)?

#### Eric Rodriguez (Jun 25 2021 at 19:31):

congr_fun?

#### Robin Carlier (Jun 25 2021 at 19:35):

So something like have neq_hyp := congr_fun ...?

#### Robin Carlier (Jun 25 2021 at 19:35):

It works but I was just wondering if there was a way to make it directly act on my f = g hypothesis rather than adding a new one.

#### Eric Rodriguez (Jun 25 2021 at 19:36):

I mean, if it's a goal state you can just rw it at the goal

#### Eric Rodriguez (Jun 25 2021 at 19:37):

you could also do rw function.funext_iff at h, specialize h x, but at that point you may just write replace h := congr_fun h x

#### Robin Carlier (Jun 25 2021 at 19:38):

Oh, I was not aware of the replacesyntax! Looks like what I want!

Last updated: Dec 20 2023 at 11:08 UTC