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 Hex: ∃x1 : set, ∃V1 : set, ∃N1 : set, (x1 ∈ B ∧ x1 ∉ A) ∧ (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))) ∧ (N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1).
An exact proof term for the current goal is (baire_step_metric_ball X d A B x Hm HxX HB HxB HAcl HAint).
Apply Hex to the current goal.
Let x1 be given.
Assume Hex1: ∃V1 : set, ∃N1 : set, (x1 ∈ B ∧ x1 ∉ A) ∧ (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))) ∧ (N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1).
Apply Hex1 to the current goal.
Let V1 be given.
Assume Hex2: ∃N1 : set, (x1 ∈ B ∧ x1 ∉ A) ∧ (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))) ∧ (N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1).
Apply Hex2 to the current goal.
Let N1 be given.
Assume Hpack: (x1 ∈ B ∧ x1 ∉ A) ∧ (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))) ∧ (N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1).
We prove the intermediate claim Hleft: (x1 ∈ B ∧ x1 ∉ A) ∧ (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))).
An exact proof term for the current goal is (andEL ((x1 ∈ B ∧ x1 ∉ A) ∧ (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A)))) (N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1) Hpack).
We prove the intermediate claim HN1pack: N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1.
An exact proof term for the current goal is (andER ((x1 ∈ B ∧ x1 ∉ A) ∧ (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A)))) (N1 ∈ ω ∧ open_ball X d x1 (eps_ N1) ⊆ V1) Hpack).
We prove the intermediate claim Hx1pair: x1 ∈ B ∧ x1 ∉ A.
An exact proof term for the current goal is (andEL (x1 ∈ B ∧ x1 ∉ A) (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))) Hleft).
We prove the intermediate claim HV1pack: V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A)).
An exact proof term for the current goal is (andER (x1 ∈ B ∧ x1 ∉ A) (V1 ∈ Tx ∧ x1 ∈ V1 ∧ closure_of X Tx V1 ⊆ (B ∩ (X ∖ A))) Hleft).
We prove the intermediate claim HV1Tx: V1 ∈ Tx.
Apply HV1pack to the current goal.
Assume HV1pair HV1cl.
Apply HV1pair to the current goal.
Assume HV1Tx Hx1V1.
An exact proof term for the current goal is HV1Tx.
We prove the intermediate claim Hx1V1: x1 ∈ V1.
Apply HV1pack to the current goal.
Assume HV1pair HV1cl.
Apply HV1pair to the current goal.
Assume HV1Tx Hx1V1.
An exact proof term for the current goal is Hx1V1.
We prove the intermediate claim HV1clsub: closure_of X Tx V1 ⊆ (B ∩ (X ∖ A)).
Apply HV1pack to the current goal.
Assume HV1pair HV1cl.
An exact proof term for the current goal is HV1cl.
We prove the intermediate claim HN1O: N1 ∈ ω.
An exact proof term for the current goal is (andEL (N1 ∈ ω) (open_ball X d x1 (eps_ N1) ⊆ V1) HN1pack).
We prove the intermediate claim HB1subV1: open_ball X d x1 (eps_ N1) ⊆ V1.
An exact proof term for the current goal is (andER (N1 ∈ ω) (open_ball X d x1 (eps_ N1) ⊆ V1) HN1pack).
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 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).
Set B1 to be the term open_ball X d x1 (eps_ N1).
We prove the intermediate claim HB1def: B1 = open_ball X d x1 (eps_ N1).
Use reflexivity.
We prove the intermediate claim Heps1R: eps_ N1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N1) (SNo_eps_SNoS_omega N1 HN1O)).
We prove the intermediate claim Heps1Pos: Rlt 0 (eps_ N1).
An exact proof term for the current goal is (RltI 0 (eps_ N1) real_0 Heps1R (SNo_eps_pos N1 HN1O)).
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 (eps_ N1) Hm Hx1X Heps1Pos).
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 (eps_ N1) Hm Hx1X Heps1Pos).
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 HclB1subU: closure_of X Tx B1 ⊆ (B ∩ (X ∖ A)).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx B1) (closure_of X Tx V1) (B ∩ (X ∖ A)) HclB1subclV1 HV1clsub).
We use x1 to witness the existential quantifier.
We use N1 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.
An exact proof term for the current goal is Hx1pair.
An exact proof term for the current goal is HB1def.
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) HclB1subU).
∎