Element in set is too restricted

Stream: new members

[Raphael Appenzeller]

(mwe below). My goal state is:

a b :  ℝ
⊢  ∀ (x : ↥{x : ℝ | a ≤ x ∧ x ≤ b}), dist x x = 0 :=

and I try to change ... |x-x| = 0, but Lean is not comfortable subtracting x from x, as it is in a special set, which may not contain 0. How can I convince Lean that it should think of x as an element in ℝ ? The error I get is:

failed to synthesize type class instance for
a b : ℝ,
x : ↥{x : ℝ | a ≤ x ∧ x ≤ b}
⊢ has_zero ↥{x : ℝ | a ≤ x ∧ x ≤ b}
state:
a b : ℝ
⊢ ∀ (x : ↥{x : ℝ | a ≤ x ∧ x ≤ b}), dist x x = 0

Minimal Working example:

import tactic
import topology.metric_space.basic
import data.real.basic

namespace metric_space
variables {X : Type} [metric_space X]

noncomputable def interval (a b : ℝ ) : metric_space {x : ℝ | a ≤ x ∧ x ≤ b }  :=
{
    dist := λ x y ,  |x-y|,
    dist_self :=
    begin
      change ∀ (x : {x : ℝ | a ≤ x ∧ x ≤ b}), |x-x| = 0,
    end,
    dist_comm := sorry,
    dist_triangle := sorry,
    eq_of_dist_eq_zero := sorry,
}

[Julian Berman]

I think you put the coercion further inward. (I know nothing about the math you're doing, but...)

[Julian Berman]

change ∀ (x : {x : ℝ | a ≤ x ∧ x ≤ b}), |(x : ℝ)-x| = 0,

[Julian Berman]

seems to work.

[Raphael Appenzeller]

Thanks a lot! This worked.