Let X, Tx, A, U and V be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Assume HUTx: U ∈ Tx.
Assume HVTx: V ∈ Tx.
Assume HAcov: A ⊆ U ∪ V.
We will prove ∃U0 : set, U0 ∈ Tx ∧ (A ∖ V) ⊆ U0 ∧ closure_of X Tx U0 ⊆ U ∧ (A ∖ U0) ⊆ V.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
Set A0 to be the term A ∖ V.
We prove the intermediate claim HA0cl: closed_in X Tx A0.
We prove the intermediate claim HVcl: closed_in X Tx (X ∖ V).
An exact proof term for the current goal is (closed_of_open_complement X Tx V HTx HVTx).
We prove the intermediate claim HA0eq: A0 = A ∩ (X ∖ V).
Apply set_ext to the current goal.
Let x be given.
Assume HxA0: x ∈ A0.
We will prove x ∈ A ∩ (X ∖ V).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (setminusE1 A V x HxA0).
We prove the intermediate claim HxnotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 A V x HxA0).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl x HxA).
An exact proof term for the current goal is (binintersectI A (X ∖ V) x HxA (setminusI X V x HxX HxnotV)).
Let x be given.
Assume Hx: x ∈ A ∩ (X ∖ V).
We will prove x ∈ A0.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A (X ∖ V) x Hx).
We prove the intermediate claim HxXnV: x ∈ X ∖ V.
An exact proof term for the current goal is (binintersectE2 A (X ∖ V) x Hx).
We prove the intermediate claim HxnotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 X V x HxXnV).
An exact proof term for the current goal is (setminusI A V x HxA HxnotV).
rewrite the current goal using HA0eq (from left to right).
An exact proof term for the current goal is (closed_binintersect X Tx A (X ∖ V) HAcl HVcl).
We prove the intermediate claim HA0subU: A0 ⊆ U.
Let x be given.
Assume HxA0: x ∈ A0.
We will prove x ∈ U.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (setminusE1 A V x HxA0).
We prove the intermediate claim HxnotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 A V x HxA0).
We prove the intermediate claim HxUV: x ∈ U ∪ V.
An exact proof term for the current goal is (HAcov x HxA).
Apply (binunionE U V x HxUV) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is HxU.
Assume HxV: x ∈ V.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotV HxV).
We prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ Tx ∧ A0 ⊆ U0 ∧ closure_of X Tx U0 ⊆ U.
An exact proof term for the current goal is (normal_space_shrink_closed X Tx A0 U Hnorm HA0cl HUTx HA0subU).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ A0 ⊆ U0 ∧ closure_of X Tx U0 ⊆ U.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
We prove the intermediate claim HU0left: U0 ∈ Tx ∧ A0 ⊆ U0.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ A0 ⊆ U0) (closure_of X Tx U0 ⊆ U) HU0).
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (A0 ⊆ U0) HU0left).
We prove the intermediate claim HU0pack: A0 ⊆ U0 ∧ closure_of X Tx U0 ⊆ U.
We prove the intermediate claim HU0left: U0 ∈ Tx ∧ A0 ⊆ U0.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ A0 ⊆ U0) (closure_of X Tx U0 ⊆ U) HU0).
We prove the intermediate claim HU0cl: closure_of X Tx U0 ⊆ U.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ A0 ⊆ U0) (closure_of X Tx U0 ⊆ U) HU0).
We prove the intermediate claim HA0subU0: A0 ⊆ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (A0 ⊆ U0) HU0left).
Apply andI to the current goal.
An exact proof term for the current goal is HA0subU0.
An exact proof term for the current goal is HU0cl.
We prove the intermediate claim HA0subU0: A0 ⊆ U0.
An exact proof term for the current goal is (andEL (A0 ⊆ U0) (closure_of X Tx U0 ⊆ U) HU0pack).
We prove the intermediate claim HclU0subU: closure_of X Tx U0 ⊆ U.
An exact proof term for the current goal is (andER (A0 ⊆ U0) (closure_of X Tx U0 ⊆ U) HU0pack).
We prove the intermediate claim HAsubV: (A ∖ U0) ⊆ V.
Let x be given.
Assume Hx: x ∈ A ∖ U0.
We will prove x ∈ V.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (setminusE1 A U0 x Hx).
We prove the intermediate claim HxnotU0: x ∉ U0.
An exact proof term for the current goal is (setminusE2 A U0 x Hx).
Apply (xm (x ∈ V)) to the current goal.
Assume HxV: x ∈ V.
An exact proof term for the current goal is HxV.
Assume HxnotV: x ∉ V.
We prove the intermediate claim HxA0: x ∈ A0.
An exact proof term for the current goal is (setminusI A V x HxA HxnotV).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (HA0subU0 x HxA0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotU0 HxU0).
We use U0 to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is HU0Tx.
An exact proof term for the current goal is HA0subU0.
An exact proof term for the current goal is HclU0subU.
An exact proof term for the current goal is HAsubV.
∎