Rewriting on objects that haven't been introduced

Stream: new members

[Abhimanyu Pallavi Sudhir]

I have the following term in my goal:

tendsto (λ (h : ℝ), ((f + g) (x + h) - (f x + g x) - (f' x + g' x) * h) / h) (nhds 0) (nhds (0 + 0))

And want to rewrite pi.add_apply to the (f + g) (x + h) term. But I can't, since h is not really a variable. Is there any way to work with rewrites on h without introducing everything before it?

[Patrick Massot]

simp can do it

[Patrick Massot]

Try simp only [pi.add_apply]

[Patrick Massot]

In this case it's probably definitionaly true, so you could probably also use change

[Abhimanyu Pallavi Sudhir]

Ok, sure, that works here -- but in a situation where the rewrite can't be done with simp (e.g. if it involves \l), is there a more general solution? I mean, what is simp actually using behind the scenes?

[Patrick Massot]

something like tendsto (λ (h : ℝ), (f (x + h) + g (x + h) - (f x + g x) - (f' x + g' x) * h) / h) (nhds 0) (nhds (0 + 0))

[Patrick Massot]

conv can be the answer

[Patrick Massot]

but simp can also go under binders sometimes

[Abhimanyu Pallavi Sudhir]

Hm, hadn't heard of conv. Interesting.

[Patrick Massot]

https://github.com/leanprover/mathlib/blob/master/docs/extras/conv.md

[Abhimanyu Pallavi Sudhir]

One more question -- to get the goal in the form above with nhds(0 + 0) and stuff, I couldn't just use a simple rewrite rw ←zero_add, because rw becomes too overzealous and turns both 0s to 0+0 (instead I had to have a statement that the new goal implies the old goal and prove that by rw zero_add). Is there any way to gain some control over the rewrite and make it transform things one at a time?

[Patrick Massot]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/rewrite_cfg and also the conv doc I mentioned in my previous answer

[Abhimanyu Pallavi Sudhir]

Thanks, I'll have a look at it.