Let X, d, A, B and x 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.
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 HV1open: open_in X Tx V1.
An exact proof term for the current goal is (open_inI X Tx V1 HTx HV1Tx).
We prove the intermediate claim HexN1: ∃N1 : set, N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1.
An exact proof term for the current goal is (open_in_metric_topology_has_eps_ball_sub X d V1 x1 Hm HV1open Hx1V1).
Apply HexN1 to the current goal.
Let N1 be given.
Assume HN1: N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1.
We use x1 to witness the existential quantifier.
We use V1 to witness the existential quantifier.
We use N1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hx1pair.
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 HU1eq: U1 = (B ∩ (X ∖ A)).
Use reflexivity.
We prove the intermediate claim HV1clsub: closure_of X Tx V1 ⊆ (B ∩ (X ∖ A)).
rewrite the current goal using HU1eq (from right to left).
An exact proof term for the current goal is HV1clsubU1.
An exact proof term for the current goal is (andI (V1 ∈ Tx ∧ x1 ∈ V1) (closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))) HV1pair HV1clsub).
An exact proof term for the current goal is HN1.
∎