Let X and x be given.
Assume Hx: x ∈ X.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ open_ball X (discrete_metric X) x 1.
We will prove y ∈ {x}.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X (discrete_metric X) x 1 y Hy).
We prove the intermediate claim Hlt: Rlt (apply_fun (discrete_metric X) (x,y)) 1.
An exact proof term for the current goal is (open_ballE2 X (discrete_metric X) x 1 y Hy).
We prove the intermediate claim Hlt': Rlt (If_i (x = y) 0 1) 1.
We will prove Rlt (If_i (x = y) 0 1) 1.
rewrite the current goal using (discrete_metric_apply X x y Hx HyX) (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
Apply xm (x = y) to the current goal.
Assume Heq: x = y.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (SingI x).
Assume Hneq: ¬ (x = y).
We prove the intermediate claim Hval: If_i (x = y) 0 1 = 1.
An exact proof term for the current goal is (If_i_0 (x = y) 0 1 Hneq).
Apply FalseE to the current goal.
We prove the intermediate claim Hbad: Rlt 1 1.
We will prove Rlt 1 1.
rewrite the current goal using Hval (from right to left) at position 1.
An exact proof term for the current goal is Hlt'.
An exact proof term for the current goal is ((not_Rlt_refl 1 real_1) Hbad).
Let y be given.
Assume Hy: y ∈ {x}.
We will prove y ∈ open_ball X (discrete_metric X) x 1.
We prove the intermediate claim HyEq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using HyEq (from left to right).
Apply open_ballI to the current goal.
An exact proof term for the current goal is Hx.
rewrite the current goal using (discrete_metric_apply X x x Hx Hx) (from left to right).
rewrite the current goal using (If_i_1 (x = x) 0 1) (from left to right).
An exact proof term for the current goal is Rlt_0_1.
Use reflexivity.
∎