Let X, d, x and r be given.

Assume Hm: metric_on X d.

Assume Hx: x ∈ X.

Assume Hr: Rlt 0 r.

An exact proof term for the current goal is (open_in_elem X (metric_topology X d) (open_ball X d x r) (open_ball_open_in_metric_topology X d x r Hm Hx Hr)).

∎