Let X and Tx be given.
Assume Hcr: completely_regular_space X Tx.
We will prove regular_space X Tx.
We will prove one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is (completely_regular_space_one_point_sets_closed X Tx Hcr).
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X Tx F.
Assume HxnotF: x ∉ F.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Set b to be the term inv_nat 2.
We prove the intermediate claim H2omega: 2 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 2 nat_2).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (inv_nat_real 2 H2omega).
We prove the intermediate claim H2Zp: 2 ∈ ω ∖ {0}.
An exact proof term for the current goal is two_in_Zplus.
We prove the intermediate claim H0ltb: Rlt 0 b.
An exact proof term for the current goal is (inv_nat_pos 2 H2Zp).
We prove the intermediate claim Hblt1: Rlt b 1.
An exact proof term for the current goal is inv_nat_2_lt_1.
We prove the intermediate claim HopenLower: open_ray_lower R b ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_lower R b ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R b HbR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_lower R b) HsRay).
We prove the intermediate claim HopenUpper: open_ray_upper R b ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R b ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R b HbR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R b) HsRay).
Apply (completely_regular_space_separation X Tx x F Hcr HxX HFcl HxnotF) to the current goal.
Let f be given.
Assume Hfpack.
We prove the intermediate claim Hfleft: continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀y : set, y ∈ F → apply_fun f y = 1) Hfpack).
We prove the intermediate claim Hfcont: continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f) (apply_fun f x = 0) Hfleft).
We prove the intermediate claim Hfx0: apply_fun f x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f) (apply_fun f x = 0) Hfleft).
We prove the intermediate claim HfF: ∀y : set, y ∈ F → apply_fun f y = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀y : set, y ∈ F → apply_fun f y = 1) Hfpack).
Set U to be the term preimage_of X f (open_ray_lower R b).
Set V to be the term preimage_of X f (open_ray_upper R b).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology f Hfcont (open_ray_lower R b) HopenLower).
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology f Hfcont (open_ray_upper R b) HopenUpper).
We prove the intermediate claim H0ray: 0 ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepI R (λt : set ⇒ order_rel R t b) 0 real_0 (Rlt_implies_order_rel_R 0 b H0ltb)).
We prove the intermediate claim Hfxray: apply_fun f x ∈ open_ray_lower R b.
rewrite the current goal using Hfx0 (from left to right) at position 1.
An exact proof term for the current goal is H0ray.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepI X (λt : set ⇒ apply_fun f t ∈ open_ray_lower R b) x HxX Hfxray).
We prove the intermediate claim H1ray: 1 ∈ open_ray_upper R b.
An exact proof term for the current goal is (SepI R (λt : set ⇒ order_rel R b t) 1 real_1 (Rlt_implies_order_rel_R b 1 Hblt1)).
We prove the intermediate claim HFsub: F ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx F HFcl).
We prove the intermediate claim HFsubV: F ⊆ V.
Let y be given.
Assume HyF: y ∈ F.
We will prove y ∈ V.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HFsub y HyF).
We prove the intermediate claim Hfy1: apply_fun f y = 1.
An exact proof term for the current goal is (HfF y HyF).
We prove the intermediate claim Hfyray: apply_fun f y ∈ open_ray_upper R b.
rewrite the current goal using Hfy1 (from left to right) at position 1.
An exact proof term for the current goal is H1ray.
An exact proof term for the current goal is (SepI X (λt : set ⇒ apply_fun f t ∈ open_ray_upper R b) y HyX Hfyray).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
Apply FalseE to the current goal.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U V z Hz).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE2 U V z Hz).
We prove the intermediate claim HzUray: apply_fun f z ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ apply_fun f t ∈ open_ray_lower R b) z HzU).
We prove the intermediate claim HzVray: apply_fun f z ∈ open_ray_upper R b.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ apply_fun f t ∈ open_ray_upper R b) z HzV).
We prove the intermediate claim Hzltb: Rlt (apply_fun f z) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun f z) b (SepE2 R (λt : set ⇒ order_rel R t b) (apply_fun f z) HzUray)).
We prove the intermediate claim Hbltz: Rlt b (apply_fun f z).
An exact proof term for the current goal is (order_rel_R_implies_Rlt b (apply_fun f z) (SepE2 R (λt : set ⇒ order_rel R b t) (apply_fun f z) HzVray)).
An exact proof term for the current goal is ((not_Rlt_sym (apply_fun f z) b Hzltb) Hbltz).
Let z be given.
Assume Hz: z ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE z Hz).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We will prove U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
We will prove (((U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U) ∧ F ⊆ V) ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove ((U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U) ∧ F ⊆ V.
Apply andI to the current goal.
We will prove (U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U.
Apply andI to the current goal.
We will prove U ∈ Tx ∧ V ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HUinTx.
An exact proof term for the current goal is HVinTx.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HFsubV.
An exact proof term for the current goal is Hdisj.
∎