## Stream: new members

### Topic: n = m, n in set s implies m in set s

#### Alexandru-Andrei Bosinta (Nov 25 2018 at 19:03):

How do you prove this in tactic mode? Or if you know how to get to term mode while in tactic mode in the middle of the proof, a term proof would also work.

#### Kevin Buzzard (Nov 25 2018 at 19:03):

rw

#### Alexandru-Andrei Bosinta (Nov 25 2018 at 19:05):

Oh yes, thank you.

#### Kevin Buzzard (Nov 25 2018 at 19:06):

It's easier in tactic mode than term mode :-) In term mode you have to use the dreaded triangle \t, which I have very limited success with.

#### Kevin Buzzard (Nov 25 2018 at 19:06):

that triangle should have an "!" in the middle of it.

Last updated: May 08 2021 at 04:14 UTC