## Stream: new members

### Topic: removing statements from hypothesis

#### 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?

#### 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

#### 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:

#### Patrick Massot (Dec 10 2020 at 16:49):

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

(deleted)

#### 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.

#### Mario Carneiro (Dec 10 2020 at 17:18):

oh, I hadn't noticed their absence

#### Patrick Massot (Dec 10 2020 at 17:19):

You would have noticed if they had returned.

#### 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

#### 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