n = m, n in set s implies m in set s

Stream: new members

[Alexandru-Andrei Bosinta]

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]

rw

[Alexandru-Andrei Bosinta]

Oh yes, thank you.

[Kevin Buzzard]

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]

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