## Stream: new members

### Topic: Replacing rw with terms

#### Andreas Swerdlow (Sep 15 2018 at 13:37):

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 (Sep 15 2018 at 13:40):

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 (Sep 15 2018 at 13:41):

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 (Sep 15 2018 at 13:41):

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

#### Kevin Buzzard (Sep 15 2018 at 13:42):

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 (Sep 15 2018 at 15:01):

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

#### Kevin Buzzard (Sep 15 2018 at 16:55):

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.

Last updated: May 15 2021 at 00:39 UTC