Unfolding set membership

Stream: new members

[Wojtek Wawrów]

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]

dsimp?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Wojtek Wawrów]

Ah that makes sense

[Kevin Buzzard]

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]

Great, that worked, thanks!