Let X, Tx, Y, Ty and f be given.
Assume Hhom: homeomorphism X Tx Y Ty f.
Assume HcrY: completely_regular_space Y Ty.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (homeomorphism_topology_left X Tx Y Ty f Hhom).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (homeomorphism_topology_right X Tx Y Ty f Hhom).
We prove the intermediate claim Hcontf: continuous_map X Tx Y Ty f.
An exact proof term for the current goal is (homeomorphism_continuous X Tx Y Ty f Hhom).
We prove the intermediate claim Hfunf: function_on f X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty f Hcontf).
We prove the intermediate claim HsepY: ∀y : set, y ∈ Y → ∀F : set, closed_in Y Ty F → y ∉ F → ∃h : set, continuous_map Y Ty R R_standard_topology h ∧ apply_fun h y = 0 ∧ ∀z : set, z ∈ F → apply_fun h z = 1.
Let y be given.
Assume HyY: y ∈ Y.
Let F be given.
Assume HFcl: closed_in Y Ty F.
Assume HynotF: y ∉ F.
An exact proof term for the current goal is (completely_regular_space_separation Y Ty y F HcrY HyY HFcl HynotF).
We prove the intermediate claim HexInv: ∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y).
An exact proof term for the current goal is (homeomorphism_inverse_package X Tx Y Ty f Hhom).
We will prove completely_regular_space X Tx.
We will prove topology_on X Tx ∧ (one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃h : set, continuous_map X Tx R R_standard_topology h ∧ apply_fun h x = 0 ∧ ∀z : set, z ∈ F → apply_fun h z = 1).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Apply andI to the current goal.
We will prove one_point_sets_closed X Tx.
We will prove topology_on X Tx ∧ ∀x0 : set, x0 ∈ X → closed_in X Tx {x0}.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove closed_in X Tx {x0}.
Set y0 to be the term apply_fun f x0.
We prove the intermediate claim Hy0Y: y0 ∈ Y.
An exact proof term for the current goal is (Hfunf x0 Hx0X).
We prove the intermediate claim HoneY: one_point_sets_closed Y Ty.
An exact proof term for the current goal is (completely_regular_space_one_point_sets_closed Y Ty HcrY).
We prove the intermediate claim HsingClosedY: ∀y : set, y ∈ Y → closed_in Y Ty {y}.
An exact proof term for the current goal is (andER (topology_on Y Ty) (∀y : set, y ∈ Y → closed_in Y Ty {y}) HoneY).
We prove the intermediate claim Hy0Closed: closed_in Y Ty {y0}.
An exact proof term for the current goal is (HsingClosedY y0 Hy0Y).
We prove the intermediate claim HpreClosed: closed_in X Tx (preimage_of X f {y0}).
An exact proof term for the current goal is (continuous_map_preimage_closed X Tx Y Ty f {y0} Hcontf Hy0Closed).
We prove the intermediate claim HpreEq: preimage_of X f {y0} = {x0}.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ preimage_of X f {y0}.
We will prove u ∈ {x0}.
We prove the intermediate claim HuX: u ∈ X.
An exact proof term for the current goal is (SepE1 X (λt : set ⇒ apply_fun f t ∈ {y0}) u Hu).
We prove the intermediate claim Hfu: apply_fun f u ∈ {y0}.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ apply_fun f t ∈ {y0}) u Hu).
We prove the intermediate claim HfuEq: apply_fun f u = y0.
An exact proof term for the current goal is (SingE y0 (apply_fun f u) Hfu).
We prove the intermediate claim Hfx0Eq: apply_fun f x0 = y0.
Use reflexivity.
We prove the intermediate claim HffEq: apply_fun f u = apply_fun f x0.
rewrite the current goal using HfuEq (from left to right).
rewrite the current goal using Hfx0Eq (from right to left).
Use reflexivity.
We prove the intermediate claim HuEq: u = x0.
An exact proof term for the current goal is (homeomorphism_injective X Tx Y Ty f Hhom u x0 HuX Hx0X HffEq).
rewrite the current goal using HuEq (from left to right).
An exact proof term for the current goal is (SingI x0).
Let u be given.
Assume Hu: u ∈ {x0}.
We will prove u ∈ preimage_of X f {y0}.
We prove the intermediate claim HuEq: u = x0.
An exact proof term for the current goal is (SingE x0 u Hu).
rewrite the current goal using HuEq (from left to right).
We will prove x0 ∈ preimage_of X f {y0}.
We prove the intermediate claim Hfy0: apply_fun f x0 ∈ {y0}.
We prove the intermediate claim Hfx0Eq: apply_fun f x0 = y0.
Use reflexivity.
rewrite the current goal using Hfx0Eq (from left to right) at position 1.
An exact proof term for the current goal is (SingI y0).
An exact proof term for the current goal is (SepI X (λt : set ⇒ apply_fun f t ∈ {y0}) x0 Hx0X Hfy0).
rewrite the current goal using HpreEq (from right to left).
An exact proof term for the current goal is HpreClosed.
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 ∃h : set, continuous_map X Tx R R_standard_topology h ∧ apply_fun h x = 0 ∧ ∀z : set, z ∈ F → apply_fun h z = 1.
Apply HexInv to the current goal.
Let g be given.
Assume Hgpack.
We prove the intermediate claim Hleft: continuous_map Y Ty X Tx g ∧ (∀x0 : set, x0 ∈ X → apply_fun g (apply_fun f x0) = x0).
An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g ∧ (∀x0 : set, x0 ∈ X → apply_fun g (apply_fun f x0) = x0)) (∀y0 : set, y0 ∈ Y → apply_fun f (apply_fun g y0) = y0) Hgpack).
We prove the intermediate claim Hgcont: continuous_map Y Ty X Tx g.
An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g) (∀x0 : set, x0 ∈ X → apply_fun g (apply_fun f x0) = x0) Hleft).
We prove the intermediate claim Hgf: ∀x0 : set, x0 ∈ X → apply_fun g (apply_fun f x0) = x0.
An exact proof term for the current goal is (andER (continuous_map Y Ty X Tx g) (∀x0 : set, x0 ∈ X → apply_fun g (apply_fun f x0) = x0) Hleft).
We prove the intermediate claim Hfg: ∀y0 : set, y0 ∈ Y → apply_fun f (apply_fun g y0) = y0.
An exact proof term for the current goal is (andER (continuous_map Y Ty X Tx g ∧ (∀x0 : set, x0 ∈ X → apply_fun g (apply_fun f x0) = x0)) (∀y0 : set, y0 ∈ Y → apply_fun f (apply_fun g y0) = y0) Hgpack).
We prove the intermediate claim Hgfun: function_on g Y X.
An exact proof term for the current goal is (continuous_map_function_on Y Ty X Tx g Hgcont).
Set y to be the term apply_fun f x.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
Set Fy to be the term preimage_of Y g F.
We prove the intermediate claim HFyClosed: closed_in Y Ty Fy.
An exact proof term for the current goal is (continuous_map_preimage_closed Y Ty X Tx g F Hgcont HFcl).
We prove the intermediate claim HynotFy: y ∉ Fy.
Assume HyFy: y ∈ Fy.
We prove the intermediate claim HgyF: apply_fun g y ∈ F.
An exact proof term for the current goal is (SepE2 Y (λu : set ⇒ apply_fun g u ∈ F) y HyFy).
We prove the intermediate claim HgyEq: apply_fun g y = x.
An exact proof term for the current goal is (Hgf x HxX).
We prove the intermediate claim HxF: x ∈ F.
rewrite the current goal using HgyEq (from right to left).
An exact proof term for the current goal is HgyF.
An exact proof term for the current goal is (HxnotF HxF).
Apply (HsepY y HyY Fy HFyClosed HynotFy) to the current goal.
Let h be given.
Assume Hhpack.
We use (compose_fun X f h) to witness the existential quantifier.
We prove the intermediate claim Hhleft: continuous_map Y Ty R R_standard_topology h ∧ apply_fun h y = 0.
An exact proof term for the current goal is (andEL (continuous_map Y Ty R R_standard_topology h ∧ apply_fun h y = 0) (∀z : set, z ∈ Fy → apply_fun h z = 1) Hhpack).
We prove the intermediate claim Hhcont: continuous_map Y Ty R R_standard_topology h.
An exact proof term for the current goal is (andEL (continuous_map Y Ty R R_standard_topology h) (apply_fun h y = 0) Hhleft).
We prove the intermediate claim Hhy0: apply_fun h y = 0.
An exact proof term for the current goal is (andER (continuous_map Y Ty R R_standard_topology h) (apply_fun h y = 0) Hhleft).
We prove the intermediate claim HhFy: ∀z : set, z ∈ Fy → apply_fun h z = 1.
An exact proof term for the current goal is (andER (continuous_map Y Ty R R_standard_topology h ∧ apply_fun h y = 0) (∀z : set, z ∈ Fy → apply_fun h z = 1) Hhpack).
Apply andI to the current goal.
We will prove continuous_map X Tx R R_standard_topology (compose_fun X f h) ∧ apply_fun (compose_fun X f h) x = 0.
Apply andI to the current goal.
An exact proof term for the current goal is (composition_continuous X Tx Y Ty R R_standard_topology f h Hcontf Hhcont).
rewrite the current goal using (compose_fun_apply X f h x HxX) (from left to right).
rewrite the current goal using Hhy0 (from right to left).
Use reflexivity.
Let z be given.
Assume HzF: z ∈ F.
We will prove apply_fun (compose_fun X f h) z = 1.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (closed_in_subset X Tx F HFcl z HzF).
We prove the intermediate claim HfzY: apply_fun f z ∈ Y.
An exact proof term for the current goal is (Hfunf z HzX).
We prove the intermediate claim Hgfz: apply_fun g (apply_fun f z) = z.
An exact proof term for the current goal is (Hgf z HzX).
We prove the intermediate claim HfzFy: apply_fun f z ∈ Fy.
We prove the intermediate claim HFyDef: Fy = preimage_of Y g F.
Use reflexivity.
rewrite the current goal using HFyDef (from left to right).
We prove the intermediate claim HpreDef: preimage_of Y g F = {u ∈ Y|apply_fun g u ∈ F}.
Use reflexivity.
rewrite the current goal using HpreDef (from left to right).
Apply (SepI Y (λu : set ⇒ apply_fun g u ∈ F) (apply_fun f z) HfzY) to the current goal.
rewrite the current goal using Hgfz (from left to right).
An exact proof term for the current goal is HzF.
rewrite the current goal using (compose_fun_apply X f h z HzX) (from left to right).
An exact proof term for the current goal is (HhFy (apply_fun f z) HfzFy).
∎