removing statements from hypothesis

Stream: new members

[Calle Sönne]

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]

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]

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

[Patrick Massot]

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

[Calle Sönne]

(deleted)

[Patrick Massot]

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]

oh, I hadn't noticed their absence

[Patrick Massot]

You would have noticed if they had returned.

[Eric Wieser]

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]

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