Replacing rw with terms

Stream: new members

[Andreas Swerdlow]

I have some proofs written in tactic mode that contain a lot of rewrites, including rewrites of hypotheses. Is there a way to easily convert such proofs into term mode. I know about eq.subst but can’t see a way to do this that won’t take aeons.

Apologies in advance I’m away so won’t be replying quickly.

[Kevin Buzzard]

The term mode version of rw is the rather harder to use \t, which is notation for eq.subst, which you already know about. In special cases you can be lucky -- e.g. if your goal is X and you want to rewrite H : X <-> Y then you can just apply H.2. But if it's a more complicated rewrite then you either briefly drop into tactic mode with by rw [A,B,C] or grit your teeth and wrestle with the triangle (which is far more picky about metavariables for some reason; giving things explicit types sometimes helps).

[Chris Hughes]

Generally rw's should be done in tactic mode, but often you can replace a bunch of rewrites with a simp, with carefully chosen lemmas in the []

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/fb1a93300ab05e86835f154e2b6156ef2ceaf77d/commutative_algebra/hilbert_basis.lean#L22

[Kevin Buzzard]

I was working on that today. Originally all proofs were in tactic mode. I then managed to turn most stuff into term mode, but failed on that last line so left the rewrite in.

[Andreas Swerdlow]

Is there any advantage to term mode in a case like this?

[Kevin Buzzard]

I think term mode proofs are less likely to break, or perhaps they break in very predictable ways. But I honestly don't know. I just get the feeling that the mathlib people like term mode better if possible, so that's what I'm working towards. I don't have any maintainer experience.