## Stream: new members

### Topic: Tactics questions

#### Michael Stoll (Feb 21 2022 at 14:38):

Are there existing tactics doing the following?

• The equivalent of the sequence have subst : a = b := by ring, rw subst, clear subst. I.e., I want to replace a term a in my goal (or some assumption) by b, where a and b are living in a ring and a = b follows from the ring axioms.
• The equivalent of the sequence let x := a, have hx : x = a := by refl, rw ← hx. I.e., I want to introduce an abbreviation x for some term a (say, to hide irrelevant structure).

#### Patrick Massot (Feb 21 2022 at 14:39):

rw show a = b, by ring,

#### Patrick Massot (Feb 21 2022 at 14:40):

set x := a

#### Alex J. Best (Feb 21 2022 at 14:40):

Or rw (by ring : a = b) for the first

#### Patrick Massot (Feb 21 2022 at 14:42):

If you really think the term a is irrelevant you can even go as far as generalize : a = x

#### Michael Stoll (Feb 21 2022 at 14:42):

@Alex J. Best Thanks! I think I tried something like this, but I probably got the parentheses wrong...

#### Michael Stoll (Feb 21 2022 at 14:43):

@Patrick Massot In some cases, that would do, but in others, I will have to go back to the original terms.

#### Patrick Massot (Feb 21 2022 at 14:43):

Then you need to remember both answers :smile:

#### Patrick Massot (Feb 21 2022 at 14:44):

Compare

example (n : ℕ) : 1 + 1 + n = n + (1+1) :=
begin
generalize : 1 + 1 = x,
end

example (n : ℕ) : 1 + 1 + n = n + (1+1) :=
begin
set x := 1 + 1,
end


#### Patrick Massot (Feb 21 2022 at 14:44):

(you need to look at the tactic state of course)

#### Patrick Massot (Feb 21 2022 at 14:45):

Bonus: you can use set x := 1 + 1 with h, to also create an assumption h : x = 1 + 1

#### Michael Stoll (Feb 21 2022 at 14:46):

How can I mark the question as solved?

#### Patrick Massot (Feb 21 2022 at 14:47):

Please don't. This only generates noise

#### Alex J. Best (Feb 21 2022 at 14:47):

I don't think it does anymore? There is a small tick mark next to the title

#### Michael Stoll (Feb 21 2022 at 14:48):

Ah, OK, there is a button in the title bar. But I'll refrain from using it for now...

#### Alex J. Best (Feb 21 2022 at 14:51):

https://github.com/zulip/zulip/pull/20977 is what I was thinking of, it significantly reduced the noise from this feature imo

Oh, nice!

#### Patrick Massot (Feb 21 2022 at 14:53):

It seems resolving the topic still posts a new message, right?

#### Alex J. Best (Feb 21 2022 at 15:04):

Yes, just no notification for people who didnt reply to the thread, so I guess it depends on how you use the zulip feed whether you see them all show up or not

#### Michael Stoll (Feb 21 2022 at 15:06):

Then it should be OK to mark the topic as resolved, since it will affect only the two of you?

Last updated: Dec 20 2023 at 11:08 UTC