Zulip Chat Archive

Stream: lean4

Topic: exact? failure

Kevin Buzzard (Sep 04 2023 at 13:31):

Bhavik pointed this out to me:

import Mathlib.Data.Real.Basic

example {x y : ℝ} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by exact? -- fails
-- le_antisymm hxy hyx

I would expect exact? to work here.

Alex J. Best (Sep 04 2023 at 13:38):

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Exact.3F.20fails.20on.20le_antisymm/near/388994247

Kevin Buzzard (Sep 04 2023 at 13:38):

Sorry, thanks.

Alex J. Best (Sep 04 2023 at 13:42):

Well actually it seems you posted first! I just happened to answer there :smile:

Last updated: Dec 20 2023 at 11:08 UTC