## Stream: new members

### Topic: Unfolding set membership

#### Wojtek Wawrów (Jun 19 2020 at 15:24):

I'm checking out the second challenge from here https://github.com/kbuzzard/xena/blob/master/Maths_Challenges/README.md
I'm still a little anxious about doing the proofs backwards, so I was trying to do it forwards, without apply. Unfolding a bunch of times gives
a ∈ {b : ℝ | ∀ (s : ℝ), s ∈ upper_bounds S → b ≤ s},
is there a way to turn this directly into ∀ (s : ℝ), s ∈ upper_bounds S → a ≤ s?

#### Kevin Buzzard (Jun 19 2020 at 15:24):

dsimp?

#### Kevin Buzzard (Jun 19 2020 at 15:25):

If dsimp works then note that this shows that what you are looking at, and what you want to be looking at, are equal by definition. Hence, if you are not planning on using a tactic like rw or simp, you can just pretend that the goal says what you want it to say (because in some sense it already does).

#### Kevin Buzzard (Jun 19 2020 at 15:25):

i.e. (assuming it's your goal) you might find that intro s just works anyway

#### Kevin Buzzard (Jun 19 2020 at 15:26):

and indeed you might find that you can just delete all the unfolds, because they only change things up to definition.

#### Wojtek Wawrów (Jun 19 2020 at 15:26):

Ah that makes sense

#### Kevin Buzzard (Jun 19 2020 at 15:27):

rw and simp are more fussy, they like things to be right on the nose ("syntactic equality"). Tactics like intro and exact are more lenient.

#### Wojtek Wawrów (Jun 19 2020 at 15:28):

Great, that worked, thanks!

Last updated: May 14 2021 at 07:19 UTC