rewriting and let

Stream: new members

[Robin Carlier]

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]

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

[Ruben Van de Velde]

change would work

[Damiano Testa]

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

[Ruben Van de Velde]

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

[Robin Carlier]

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

[Ruben Van de Velde]

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

[Eric Rodriguez]

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

[Robin Carlier]

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]

congr_fun?

[Eric Rodriguez]

(docs#congr_fun)

[Robin Carlier]

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

[Robin Carlier]

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]

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

[Eric Rodriguez]

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]

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