Let x1 and x2 be given.

Assume Hx1: x1 ∈ product_space I Xi.

Assume Hx2: x2 ∈ product_space I Xi.

Assume Hneq: x1 ≠ x2.

We will prove ∃U V : set, U ∈ product_topology_full I Xi ∧ V ∈ product_topology_full I Xi ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.

Apply (xm (I = Empty)) to the current goal.

Assume HI0: I = Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HX0: product_space Empty Xi = {Empty}.

An exact proof term for the current goal is (product_space_empty_index Xi).

We prove the intermediate claim Hx1S: x1 ∈ {Empty}.

rewrite the current goal using HX0 (from right to left).

We prove the intermediate claim Hx1Eidx: x1 ∈ product_space Empty Xi.

We will prove x1 ∈ product_space Empty Xi.

rewrite the current goal using HI0 (from right to left).

An exact proof term for the current goal is Hx1.

An exact proof term for the current goal is Hx1Eidx.

We prove the intermediate claim Hx2S: x2 ∈ {Empty}.

rewrite the current goal using HX0 (from right to left).

We prove the intermediate claim Hx2Eidx: x2 ∈ product_space Empty Xi.

We will prove x2 ∈ product_space Empty Xi.

rewrite the current goal using HI0 (from right to left).

An exact proof term for the current goal is Hx2.

An exact proof term for the current goal is Hx2Eidx.

We prove the intermediate claim Hx1E: x1 = Empty.

An exact proof term for the current goal is (SingE Empty x1 Hx1S).

We prove the intermediate claim Hx2E: x2 = Empty.

An exact proof term for the current goal is (SingE Empty x2 Hx2S).

We prove the intermediate claim Heq: x1 = x2.

rewrite the current goal using Hx1E (from left to right).

rewrite the current goal using Hx2E (from left to right).

Use reflexivity.

An exact proof term for the current goal is (Hneq Heq).

Assume HIne: I ≠ Empty.

Set X to be the term product_space I Xi.

We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume HiI: i ∈ I.

An exact proof term for the current goal is (Hausdorff_space_topology (product_component Xi i) (product_component_topology Xi i) (HHfam i HiI)).

We prove the intermediate claim HSsub: subbasis_on X (product_subbasis_full I Xi).

An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIne HcompTop).

We prove the intermediate claim Hexi: ∃i : set, i ∈ I ∧ apply_fun x1 i ≠ apply_fun x2 i.

An exact proof term for the current goal is (product_space_points_differ_coord I Xi x1 x2 Hx1 Hx2 Hneq).

Apply Hexi to the current goal.

Let i be given.

Assume Hiconj.

We prove the intermediate claim HiI: i ∈ I.

An exact proof term for the current goal is (andEL (i ∈ I) (apply_fun x1 i ≠ apply_fun x2 i) Hiconj).

We prove the intermediate claim Hdiff: apply_fun x1 i ≠ apply_fun x2 i.

An exact proof term for the current goal is (andER (i ∈ I) (apply_fun x1 i ≠ apply_fun x2 i) Hiconj).

We prove the intermediate claim HHi: Hausdorff_space (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (HHfam i HiI).

We prove the intermediate claim HTi: topology_on (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (Hausdorff_space_topology (product_component Xi i) (product_component_topology Xi i) HHi).

We prove the intermediate claim HSepi: ∀y1 y2 : set, y1 ∈ product_component Xi i → y2 ∈ product_component Xi i → y1 ≠ y2 → ∃U V : set, U ∈ product_component_topology Xi i ∧ V ∈ product_component_topology Xi i ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (andER (topology_on (product_component Xi i) (product_component_topology Xi i)) (∀y1 y2 : set, y1 ∈ product_component Xi i → y2 ∈ product_component Xi i → y1 ≠ y2 → ∃U V : set, U ∈ product_component_topology Xi i ∧ V ∈ product_component_topology Xi i ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty) HHi).

We prove the intermediate claim Hx1i: apply_fun x1 i ∈ product_component Xi i.

We prove the intermediate claim Hx1prop: total_function_on x1 I (space_family_union I Xi) ∧ functional_graph x1 ∧ ∀j : set, j ∈ I → apply_fun x1 j ∈ space_family_set Xi j.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf : set ⇒ total_function_on f I (space_family_union I Xi) ∧ functional_graph f ∧ ∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j) x1 Hx1).

We prove the intermediate claim Hx1all: ∀j : set, j ∈ I → apply_fun x1 j ∈ space_family_set Xi j.

An exact proof term for the current goal is (andER (total_function_on x1 I (space_family_union I Xi) ∧ functional_graph x1) (∀j : set, j ∈ I → apply_fun x1 j ∈ space_family_set Xi j) Hx1prop).

An exact proof term for the current goal is (Hx1all i HiI).

We prove the intermediate claim Hx2i: apply_fun x2 i ∈ product_component Xi i.

We prove the intermediate claim Hx2prop: total_function_on x2 I (space_family_union I Xi) ∧ functional_graph x2 ∧ ∀j : set, j ∈ I → apply_fun x2 j ∈ space_family_set Xi j.

We prove the intermediate claim Hx2all: ∀j : set, j ∈ I → apply_fun x2 j ∈ space_family_set Xi j.

An exact proof term for the current goal is (andER (total_function_on x2 I (space_family_union I Xi) ∧ functional_graph x2) (∀j : set, j ∈ I → apply_fun x2 j ∈ space_family_set Xi j) Hx2prop).

An exact proof term for the current goal is (Hx2all i HiI).

We prove the intermediate claim HexUV: ∃U0 V0 : set, U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i ∧ apply_fun x1 i ∈ U0 ∧ apply_fun x2 i ∈ V0 ∧ U0 ∩ V0 = Empty.

An exact proof term for the current goal is (HSepi (apply_fun x1 i) (apply_fun x2 i) Hx1i Hx2i Hdiff).

Apply HexUV to the current goal.

Let U0 be given.

Assume HU0conj.

Apply HU0conj to the current goal.

Let V0 be given.

Assume HV0conj.

We prove the intermediate claim H4: (((U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) ∧ apply_fun x1 i ∈ U0) ∧ apply_fun x2 i ∈ V0).

An exact proof term for the current goal is (andEL ((((U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) ∧ apply_fun x1 i ∈ U0) ∧ apply_fun x2 i ∈ V0)) (U0 ∩ V0 = Empty) HV0conj).

We prove the intermediate claim Hdisj: U0 ∩ V0 = Empty.

An exact proof term for the current goal is (andER ((((U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) ∧ apply_fun x1 i ∈ U0) ∧ apply_fun x2 i ∈ V0)) (U0 ∩ V0 = Empty) HV0conj).

We prove the intermediate claim H3: ((U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) ∧ apply_fun x1 i ∈ U0).

An exact proof term for the current goal is (andEL (((U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) ∧ apply_fun x1 i ∈ U0)) (apply_fun x2 i ∈ V0) H4).

We prove the intermediate claim Hx2V0: apply_fun x2 i ∈ V0.

An exact proof term for the current goal is (andER (((U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) ∧ apply_fun x1 i ∈ U0)) (apply_fun x2 i ∈ V0) H4).

We prove the intermediate claim HUV: U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i.

An exact proof term for the current goal is (andEL (U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) (apply_fun x1 i ∈ U0) H3).

We prove the intermediate claim Hx1U0: apply_fun x1 i ∈ U0.

An exact proof term for the current goal is (andER (U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i) (apply_fun x1 i ∈ U0) H3).

We prove the intermediate claim HU0top: U0 ∈ product_component_topology Xi i.

An exact proof term for the current goal is (andEL (U0 ∈ product_component_topology Xi i) (V0 ∈ product_component_topology Xi i) HUV).

We prove the intermediate claim HV0top: V0 ∈ product_component_topology Xi i.

An exact proof term for the current goal is (andER (U0 ∈ product_component_topology Xi i) (V0 ∈ product_component_topology Xi i) HUV).

Set U to be the term product_cylinder I Xi i U0.

Set V to be the term product_cylinder I Xi i V0.

We use U to witness the existential quantifier.

We use V to witness the existential quantifier.

Apply and5I to the current goal.

We prove the intermediate claim HUsub: U ∈ product_subbasis_full I Xi.

We will prove U ∈ product_subbasis_full I Xi.

We will prove U ∈ (⋃_{j ∈ I}{product_cylinder I Xi j W|W ∈ space_family_topology Xi j}).

Apply (famunionI I (λj : set ⇒ {product_cylinder I Xi j W|W ∈ space_family_topology Xi j}) i U HiI) to the current goal.

An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λW : set ⇒ product_cylinder I Xi i W) U0 HU0top).

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (product_subbasis_full I Xi) U HSsub HUsub).

We prove the intermediate claim HVsub: V ∈ product_subbasis_full I Xi.

We will prove V ∈ product_subbasis_full I Xi.

We will prove V ∈ (⋃_{j ∈ I}{product_cylinder I Xi j W|W ∈ space_family_topology Xi j}).

Apply (famunionI I (λj : set ⇒ {product_cylinder I Xi j W|W ∈ space_family_topology Xi j}) i V HiI) to the current goal.

An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λW : set ⇒ product_cylinder I Xi i W) V0 HV0top).

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (product_subbasis_full I Xi) V HSsub HVsub).

We will prove x1 ∈ U.

We prove the intermediate claim HdefU: U = {f ∈ product_space I Xi|i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0}.

Use reflexivity.

rewrite the current goal using HdefU (from left to right).

Apply (SepI (product_space I Xi) (λf : set ⇒ i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0) x1 Hx1) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is HiI.

An exact proof term for the current goal is HU0top.

An exact proof term for the current goal is Hx1U0.

We will prove x2 ∈ V.

We prove the intermediate claim HdefV: V = {f ∈ product_space I Xi|i ∈ I ∧ V0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ V0}.

Use reflexivity.

rewrite the current goal using HdefV (from left to right).

Apply (SepI (product_space I Xi) (λf : set ⇒ i ∈ I ∧ V0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ V0) x2 Hx2) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is HiI.

An exact proof term for the current goal is HV0top.

An exact proof term for the current goal is Hx2V0.

We will prove U ∩ V = Empty.

Apply set_ext to the current goal.

Let f be given.

Assume Hf: f ∈ U ∩ V.

Apply FalseE to the current goal.

We prove the intermediate claim HfU: f ∈ U.

An exact proof term for the current goal is (binintersectE1 U V f Hf).

We prove the intermediate claim HfV: f ∈ V.

An exact proof term for the current goal is (binintersectE2 U V f Hf).

We prove the intermediate claim HfUprop: i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0.

An exact proof term for the current goal is (SepE2 X (λf0 : set ⇒ i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U0) f HfU).

We prove the intermediate claim HfVprop: i ∈ I ∧ V0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ V0.

An exact proof term for the current goal is (SepE2 X (λf0 : set ⇒ i ∈ I ∧ V0 ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ V0) f HfV).

We prove the intermediate claim HfiU0: apply_fun f i ∈ U0.

An exact proof term for the current goal is (andER (i ∈ I ∧ U0 ∈ space_family_topology Xi i) (apply_fun f i ∈ U0) HfUprop).

We prove the intermediate claim HfiV0: apply_fun f i ∈ V0.

An exact proof term for the current goal is (andER (i ∈ I ∧ V0 ∈ space_family_topology Xi i) (apply_fun f i ∈ V0) HfVprop).

We prove the intermediate claim HfiInt: apply_fun f i ∈ U0 ∩ V0.

Apply binintersectI to the current goal.

An exact proof term for the current goal is HfiU0.

An exact proof term for the current goal is HfiV0.

We prove the intermediate claim HfiE: apply_fun f i ∈ Empty.

rewrite the current goal using Hdisj (from right to left).

An exact proof term for the current goal is HfiInt.

An exact proof term for the current goal is (EmptyE (apply_fun f i) HfiE).

Let f be given.

Assume Hf: f ∈ Empty.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE f Hf).