Zulip Chat Archive

Stream: new members

Topic: removing statements from hypothesis


view this post on Zulip Calle Sönne (Dec 10 2020 at 16:42):

I have the following hypothesis:

H1: is_open (u  s)  is_open (v  s)  is_closed s  s  u  s  v  s  u  s  (v  s) =   s  u  s  s  s  v  s  s

So at the end of this implication chain I have two s ⊆ s, is there any way for me to remove these?

view this post on Zulip Calle Sönne (Dec 10 2020 at 16:44):

I might add that my goal is of the form

s  u  s  v

which i why I want to remove the s ⊆ s

view this post on Zulip Calle Sönne (Dec 10 2020 at 16:48):

Okay I managed to solve it using simp [set.subset.refl] at H1. Thought I tried that before :sweat_smile:

view this post on Zulip Patrick Massot (Dec 10 2020 at 16:49):

You wrote clean again, which is punished with red rectangles.

view this post on Zulip Calle Sönne (Dec 10 2020 at 16:51):

(deleted)

view this post on Zulip Patrick Massot (Dec 10 2020 at 16:55):

This is bad because for a few seconds I thought Zulip rolled back to the old pygments highlighting library which gave us all those red rectangles in the past.

view this post on Zulip Mario Carneiro (Dec 10 2020 at 17:18):

oh, I hadn't noticed their absence

view this post on Zulip Patrick Massot (Dec 10 2020 at 17:19):

You would have noticed if they had returned.

view this post on Zulip Eric Wieser (Dec 10 2020 at 17:25):

Note that clean happens because you type ```lean , and then zulip pops up an unhelpful suggestion box that is annoying to dismiss whose second option is clean

view this post on Zulip Eric Wieser (Dec 10 2020 at 17:26):

If you just type ``` you get lean by default and no annoying box


Last updated: May 12 2021 at 23:13 UTC