Zulip Chat Archive

Stream: new members

Topic: Unfolding set membership


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:24):

dsimp?

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:25):

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

view this post on Zulip 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.

view this post on Zulip Wojtek Wawrów (Jun 19 2020 at 15:26):

Ah that makes sense

view this post on Zulip 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.

view this post on Zulip Wojtek Wawrów (Jun 19 2020 at 15:28):

Great, that worked, thanks!


Last updated: May 14 2021 at 07:19 UTC