Let X, d, x and r be given.
Assume Hm: metric_on X d.
Assume Hx: x ∈ X.
Assume Hr: Rlt 0 r.
Assume Hempty: open_ball X d x r = Empty.
We prove the intermediate claim Hxin: x ∈ open_ball X d x r.
An exact proof term for the current goal is (center_in_open_ball X d x r Hm Hx Hr).
We prove the intermediate claim HxinEmpty: x ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is Hxin.
An exact proof term for the current goal is (EmptyE x HxinEmpty).
∎