Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 25 2018 at 19:03):

rw

view this post on Zulip Alexandru-Andrei Bosinta (Nov 25 2018 at 19:05):

Oh yes, thank you.

view this post on Zulip 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.

view this post on Zulip 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