by_contradiction timeouts

Stream: general

[Bartosz Piotrowski]

Hi, when I try to use by_contradiction in the example below it timeouts, and I don't understand why... Or is it a bug? I would be grateful for help!

import tactic
import topology.metric_space.basic

example
  {α : Type} [metric_space α]
  {β : Type} [metric_space β]
  (f : α → β)
  (g : α → β)
  (h₁ : continuous f)
  (h₂ : continuous g)
  (s : set α)
  (h₃ : dense s)
  (h₄ : ∀ x ∈ s, f x = g x)
  : f = g :=
begin
  ext,
  by_contradiction h₅, -- timeout; why?
end

Edit: Lean version is 3.42.1

[Ruben Van de Velde]

Try classical, before ext,?

[Bartosz Piotrowski]

Ok, it works then. Thank you! But is it an intended behavior that it time-outs instead of printing some more informative error?

[Kevin Buzzard]

Probably Lean is looking for a proof that the equality is decidable but metric spaces are sufficiently complicated that it gets lost looking.

[Bartosz Piotrowski]

Ok, I see...

[Matt Diamond]

(deleted)

[Yury G. Kudryashov]

Note that we have this lemma for T2 topological spaces