Let X, d, A, B, x and a be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HB: B ∈ metric_topology X d.
Assume HxB: x ∈ B.
Assume HAcl: closed_in X (metric_topology X d) A.
Assume HAint: interior_of X (metric_topology X d) A = Empty.
Assume HaR: a ∈ R.
Assume Ha0: Rlt 0 a.
Set Tx to be the term metric_topology X d.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (metric_spaces_regular X d Hm).
We prove the intermediate claim HnotSub: ¬ (B ⊆ A).
An exact proof term for the current goal is (point_in_open_empty_interior_not_subset X Tx A B x HTx HAint HB HxB).
We prove the intermediate claim Hexx1: ∃x1 : set, x1 ∈ B ∧ x1 ∉ A.
An exact proof term for the current goal is (not_subset_ex_elem A B HnotSub).
Apply Hexx1 to the current goal.
Let x1 be given.
Assume Hx1pair: x1 ∈ B ∧ x1 ∉ A.
We prove the intermediate claim Hx1B: x1 ∈ B.
An exact proof term for the current goal is (andEL (x1 ∈ B) (x1 ∉ A) Hx1pair).
We prove the intermediate claim Hx1notA: x1 ∉ A.
An exact proof term for the current goal is (andER (x1 ∈ B) (x1 ∉ A) Hx1pair).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx B HTx HB).
We prove the intermediate claim Hx1X: x1 ∈ X.
An exact proof term for the current goal is (HBsubX x1 Hx1B).
We prove the intermediate claim HAcOpen: open_in X Tx (X ∖ A).
An exact proof term for the current goal is (open_of_closed_complement X Tx A HAcl).
We prove the intermediate claim HAcTx: X ∖ A ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ A) HAcOpen).
Set U1 to be the term B ∩ (X ∖ A).
We prove the intermediate claim HU1Tx: U1 ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_axiom X Tx HTx B HB (X ∖ A) HAcTx).
We prove the intermediate claim Hx1U1: x1 ∈ U1.
We prove the intermediate claim HU1def: U1 = B ∩ (X ∖ A).
Use reflexivity.
rewrite the current goal using HU1def (from left to right).
An exact proof term for the current goal is (binintersectI B (X ∖ A) x1 Hx1B (setminusI X A x1 Hx1X Hx1notA)).
We prove the intermediate claim HexV1: ∃V1 : set, V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ U1.
An exact proof term for the current goal is (regular_space_shrink_neighborhood X Tx x1 U1 Hreg Hx1X HU1Tx Hx1U1).
Apply HexV1 to the current goal.
Let V1 be given.
Assume HV1: V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ U1.
We prove the intermediate claim HV1pair: V1 ∈ Tx ∧ x1 ∈ V1.
An exact proof term for the current goal is (andEL (V1 ∈ Tx ∧ x1 ∈ V1) (closure_of X Tx V1 ⊆ U1) HV1).
We prove the intermediate claim HV1Tx: V1 ∈ Tx.
An exact proof term for the current goal is (andEL (V1 ∈ Tx) (x1 ∈ V1) HV1pair).
We prove the intermediate claim Hx1V1: x1 ∈ V1.
An exact proof term for the current goal is (andER (V1 ∈ Tx) (x1 ∈ V1) HV1pair).
We prove the intermediate claim HV1clsubU1: closure_of X Tx V1 ⊆ U1.
An exact proof term for the current goal is (andER (V1 ∈ Tx ∧ x1 ∈ V1) (closure_of X Tx V1 ⊆ U1) HV1).
We prove the intermediate claim Hexr1: ∃r1 : set, r1 ∈ R ∧ Rlt 0 r1 ∧ open_ball X d x1 r1 ⊆ V1 ∧ Rlt r1 a.
An exact proof term for the current goal is (metric_topology_neighborhood_contains_ball_bounded X d x1 V1 a Hm Hx1X HV1Tx Hx1V1 HaR Ha0).
Apply Hexr1 to the current goal.
Let r1 be given.
Assume Hr1pack.
We prove the intermediate claim Hr1pair0: (r1 ∈ R ∧ Rlt 0 r1 ∧ open_ball X d x1 r1 ⊆ V1) ∧ Rlt r1 a.
An exact proof term for the current goal is Hr1pack.
We prove the intermediate claim Hr1main: (r1 ∈ R ∧ Rlt 0 r1 ∧ open_ball X d x1 r1 ⊆ V1).
An exact proof term for the current goal is (andEL (r1 ∈ R ∧ Rlt 0 r1 ∧ open_ball X d x1 r1 ⊆ V1) (Rlt r1 a) Hr1pair0).
We prove the intermediate claim Hr1a: Rlt r1 a.
An exact proof term for the current goal is (andER (r1 ∈ R ∧ Rlt 0 r1 ∧ open_ball X d x1 r1 ⊆ V1) (Rlt r1 a) Hr1pair0).
We prove the intermediate claim Hr1pair1: (r1 ∈ R ∧ Rlt 0 r1) ∧ open_ball X d x1 r1 ⊆ V1.
An exact proof term for the current goal is Hr1main.
We prove the intermediate claim Hr1pair2: r1 ∈ R ∧ Rlt 0 r1.
An exact proof term for the current goal is (andEL (r1 ∈ R ∧ Rlt 0 r1) (open_ball X d x1 r1 ⊆ V1) Hr1pair1).
We prove the intermediate claim HB1subV1: open_ball X d x1 r1 ⊆ V1.
An exact proof term for the current goal is (andER (r1 ∈ R ∧ Rlt 0 r1) (open_ball X d x1 r1 ⊆ V1) Hr1pair1).
We prove the intermediate claim Hr1R: r1 ∈ R.
An exact proof term for the current goal is (andEL (r1 ∈ R) (Rlt 0 r1) Hr1pair2).
We prove the intermediate claim Hr10: Rlt 0 r1.
An exact proof term for the current goal is (andER (r1 ∈ R) (Rlt 0 r1) Hr1pair2).
Set B1 to be the term open_ball X d x1 r1.
We prove the intermediate claim HB1def: B1 = open_ball X d x1 r1.
Use reflexivity.
We prove the intermediate claim HB1Tx: B1 ∈ Tx.
rewrite the current goal using HB1def (from left to right).
An exact proof term for the current goal is (open_ball_in_metric_topology X d x1 r1 Hm Hx1X Hr10).
We prove the intermediate claim Hx1B1: x1 ∈ B1.
rewrite the current goal using HB1def (from left to right).
An exact proof term for the current goal is (center_in_open_ball X d x1 r1 Hm Hx1X Hr10).
We prove the intermediate claim HB1subV1': B1 ⊆ V1.
rewrite the current goal using HB1def (from left to right).
An exact proof term for the current goal is HB1subV1.
We prove the intermediate claim HV1subX: V1 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V1 HTx HV1Tx).
We prove the intermediate claim HclB1subclV1: closure_of X Tx B1 ⊆ closure_of X Tx V1.
An exact proof term for the current goal is (closure_monotone X Tx B1 V1 HTx HB1subV1' HV1subX).
We prove the intermediate claim HclB1subU1: closure_of X Tx B1 ⊆ U1.
An exact proof term for the current goal is (Subq_tra (closure_of X Tx B1) (closure_of X Tx V1) U1 HclB1subclV1 HV1clsubU1).
We prove the intermediate claim HU1eq: U1 = (B ∩ (X ∖ A)).
Use reflexivity.
We use x1 to witness the existential quantifier.
We use r1 to witness the existential quantifier.
We use B1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hx1pair.
An exact proof term for the current goal is (andI (r1 ∈ R ∧ Rlt 0 r1) (Rlt r1 a) Hr1pair2 Hr1a).
An exact proof term for the current goal is HB1def.
We prove the intermediate claim HclB1sub: closure_of X Tx B1 ⊆ (B ∩ (X ∖ A)).
rewrite the current goal using HU1eq (from right to left).
An exact proof term for the current goal is HclB1subU1.
An exact proof term for the current goal is (andI (B1 ∈ Tx ∧ x1 ∈ B1) (closure_of X Tx B1 ⊆ (B ∩ (X ∖ A))) (andI (B1 ∈ Tx) (x1 ∈ B1) HB1Tx Hx1B1) HclB1sub).
∎