Zulip Chat Archive

Stream: new members

Topic: Question about `classical.some`

Pedro Minicz (Aug 12 2020 at 17:26):

Do we have that classical.some (Exists.intro x hx) = x?

variables {x : ℕ} (hx : x = 1)

set_option pp.proofs true

example : classical.some (Exists.intro x hx) = x :=
sorry

example : classical.some (Exists.intro x hx) = 1 :=
sorry

Reid Barton (Aug 12 2020 at 17:32):

No, certainly not

Reid Barton (Aug 12 2020 at 17:33):

because Exists.intro x hx = Exists.intro x' hx' even if x and x' are different

Last updated: Dec 20 2023 at 11:08 UTC