Let Y, d, y and r be given.
Assume Hm: metric_on Y d.
Assume HyY: y ∈ Y.
Assume HrR: r ∈ R.
Assume HrPos: Rlt 0 r.
Set Ty to be the term metric_topology Y d.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y d Hm).
Let z be given.
Assume Hz: z ∈ closure_of Y Ty (open_ball Y d y r).
We will prove z ∈ open_ball Y d y (add_SNo r r).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λz0 : set ⇒ ∀U : set, U ∈ Ty → z0 ∈ U → U ∩ open_ball Y d y r ≠ Empty) z Hz).
Apply (xm (z ∈ open_ball Y d y (add_SNo r r))) to the current goal.
Assume HzIn: z ∈ open_ball Y d y (add_SNo r r).
An exact proof term for the current goal is HzIn.
Assume HzNot: ¬ (z ∈ open_ball Y d y (add_SNo r r)).
We prove the intermediate claim Hnlt: ¬ (Rlt (apply_fun d (y,z)) (add_SNo r r)).
Assume Hlt: Rlt (apply_fun d (y,z)) (add_SNo r r).
We prove the intermediate claim HzIn': z ∈ open_ball Y d y (add_SNo r r).
An exact proof term for the current goal is (open_ballI Y d y (add_SNo r r) z HzY Hlt).
An exact proof term for the current goal is (HzNot HzIn').
Set Uz to be the term open_ball Y d z r.
We prove the intermediate claim HUzTy: Uz ∈ Ty.
An exact proof term for the current goal is (open_ball_in_metric_topology Y d z r Hm HzY HrPos).
We prove the intermediate claim HzUz: z ∈ Uz.
An exact proof term for the current goal is (center_in_open_ball Y d z r Hm HzY HrPos).
We prove the intermediate claim HinterEmpty: Uz ∩ open_ball Y d y r = Empty.
Apply Empty_Subq_eq to the current goal.
Let w be given.
Assume Hw: w ∈ Uz ∩ open_ball Y d y r.
We will prove w ∈ Empty.
We prove the intermediate claim HwUz: w ∈ Uz.
An exact proof term for the current goal is (binintersectE1 Uz (open_ball Y d y r) w Hw).
We prove the intermediate claim HwBy: w ∈ open_ball Y d y r.
An exact proof term for the current goal is (binintersectE2 Uz (open_ball Y d y r) w Hw).
We prove the intermediate claim HwY: w ∈ Y.
An exact proof term for the current goal is (open_ballE1 Y d y r w HwBy).
We prove the intermediate claim Hzw: Rlt (apply_fun d (z,w)) r.
An exact proof term for the current goal is (open_ballE2 Y d z r w HwUz).
We prove the intermediate claim Hyw: Rlt (apply_fun d (y,w)) r.
An exact proof term for the current goal is (open_ballE2 Y d y r w HwBy).
We prove the intermediate claim Hsym: apply_fun d (z,w) = apply_fun d (w,z).
An exact proof term for the current goal is (metric_on_symmetric Y d z w Hm HzY HwY).
We prove the intermediate claim Hwz: Rlt (apply_fun d (w,z)) r.
rewrite the current goal using Hsym (from right to left).
An exact proof term for the current goal is Hzw.
We prove the intermediate claim Hle: Rle (apply_fun d (y,z)) (add_SNo (apply_fun d (y,w)) (apply_fun d (w,z))).
An exact proof term for the current goal is (metric_triangle_Rle Y d y w z Hm HyY HwY HzY).
We prove the intermediate claim Hsumlt: Rlt (add_SNo (apply_fun d (y,w)) (apply_fun d (w,z))) (add_SNo r r).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun d (y,w)) r (apply_fun d (w,z)) r Hyw Hwz).
We prove the intermediate claim Hlt: Rlt (apply_fun d (y,z)) (add_SNo r r).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (y,z)) (add_SNo (apply_fun d (y,w)) (apply_fun d (w,z))) (add_SNo r r) Hle Hsumlt).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt Hlt).
We prove the intermediate claim Hcl: ∀U : set, U ∈ Ty → z ∈ U → U ∩ open_ball Y d y r ≠ Empty.
An exact proof term for the current goal is (SepE2 Y (λz0 : set ⇒ ∀U : set, U ∈ Ty → z0 ∈ U → U ∩ open_ball Y d y r ≠ Empty) z Hz).
We prove the intermediate claim Hne: Uz ∩ open_ball Y d y r ≠ Empty.
An exact proof term for the current goal is (Hcl Uz HUzTy HzUz).
We prove the intermediate claim Hfalse: False.
An exact proof term for the current goal is (Hne HinterEmpty).
Apply FalseE to the current goal.
An exact proof term for the current goal is Hfalse.
∎