Let X0 and y0 be given.

Assume HX0fin: finite X0.

Assume Hy0notX0: y0 ∉ X0.

Assume HpX0: p X0.

We will prove p (X0 ∪ {y0}).

Assume HsubX1: X0 ∪ {y0} ⊆ S.

Assume HxIntX1: x ∈ intersection_of_family Xp (X0 ∪ {y0}).

We prove the intermediate claim HsubX0: X0 ⊆ S.

Let s be given.

Assume HsX0: s ∈ X0.

An exact proof term for the current goal is (HsubX1 s (binunionI1 X0 {y0} s HsX0)).

We prove the intermediate claim Hy0S: y0 ∈ S.

An exact proof term for the current goal is (HsubX1 y0 (binunionI2 X0 {y0} y0 (SingI y0))).

We prove the intermediate claim HxXp1: x ∈ Xp.

An exact proof term for the current goal is (intersection_of_familyE1 Xp (X0 ∪ {y0}) x HxIntX1).

We prove the intermediate claim HxIntX0: x ∈ intersection_of_family Xp X0.

Apply (intersection_of_familyI Xp X0 x HxXp1) to the current goal.

Let s be given.

Assume HsX0: s ∈ X0.

We prove the intermediate claim HsX1: s ∈ X0 ∪ {y0}.

An exact proof term for the current goal is (binunionI1 X0 {y0} s HsX0).

An exact proof term for the current goal is (intersection_of_familyE2 Xp (X0 ∪ {y0}) x HxIntX1 s HsX1).

We prove the intermediate claim Hxy0: x ∈ y0.

We prove the intermediate claim Hy0X1: y0 ∈ X0 ∪ {y0}.

An exact proof term for the current goal is (binunionI2 X0 {y0} y0 (SingI y0)).

An exact proof term for the current goal is (intersection_of_familyE2 Xp (X0 ∪ {y0}) x HxIntX1 y0 Hy0X1).

We prove the intermediate claim Hexf0: ∃f0 : set, continuous_map Xp Tp R R_standard_topology f0 ∧ apply_fun f0 x = 0 ∧ ∀y : set, y ∈ Xp → (∃s : set, s ∈ X0 ∧ y ∉ s) → apply_fun f0 y = 1.

An exact proof term for the current goal is (HpX0 HsubX0 HxIntX0).

Apply Hexf0 to the current goal.

Let f0 be given.

Assume Hf0pack.

We prove the intermediate claim Hexg0: ∃g0 : set, continuous_map Xp Tp R R_standard_topology g0 ∧ apply_fun g0 x = 0 ∧ ∀y : set, y ∈ Xp → y ∉ y0 → apply_fun g0 y = 1.

We prove the intermediate claim Hexi: ∃i : set, i ∈ I ∧ ∃U : set, U ∈ space_family_topology Xi i ∧ y0 = product_cylinder I Xi i U.

An exact proof term for the current goal is (product_subbasis_fullE I Xi y0 Hy0S).

Apply Hexi to the current goal.

Let i be given.

Assume Hipack.

We prove the intermediate claim HiI: i ∈ I.

An exact proof term for the current goal is (andEL (i ∈ I) (∃U : set, U ∈ space_family_topology Xi i ∧ y0 = product_cylinder I Xi i U) Hipack).

We prove the intermediate claim HexU: ∃U : set, U ∈ space_family_topology Xi i ∧ y0 = product_cylinder I Xi i U.

An exact proof term for the current goal is (andER (i ∈ I) (∃U : set, U ∈ space_family_topology Xi i ∧ y0 = product_cylinder I Xi i U) Hipack).

Apply HexU to the current goal.

Let U be given.

Assume HUand.

We prove the intermediate claim HUopen: U ∈ space_family_topology Xi i.

An exact proof term for the current goal is (andEL (U ∈ space_family_topology Xi i) (y0 = product_cylinder I Xi i U) HUand).

We prove the intermediate claim Hy0eq: y0 = product_cylinder I Xi i U.

An exact proof term for the current goal is (andER (U ∈ space_family_topology Xi i) (y0 = product_cylinder I Xi i U) HUand).

We prove the intermediate claim HxCyl: x ∈ product_cylinder I Xi i U.

rewrite the current goal using Hy0eq (from right to left) at position 1.

An exact proof term for the current goal is Hxy0.

We prove the intermediate claim HxCylProp: i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun x i ∈ U.

An exact proof term for the current goal is (SepE2 Xp (λf0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) x HxCyl).

We prove the intermediate claim HxiU: apply_fun x i ∈ U.

An exact proof term for the current goal is (andER (i ∈ I ∧ U ∈ space_family_topology Xi i) (apply_fun x i ∈ U) HxCylProp).

Set Xi_i to be the term space_family_set Xi i.

Set Ti_i to be the term space_family_topology Xi i.

We prove the intermediate claim HTi: topology_on Xi_i Ti_i.

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

We prove the intermediate claim HUsubXi: U ⊆ Xi_i.

An exact proof term for the current goal is (topology_elem_subset Xi_i Ti_i U HTi HUopen).

We prove the intermediate claim HxiXi: apply_fun x i ∈ Xi_i.

An exact proof term for the current goal is (HUsubXi (apply_fun x i) HxiU).

Set C to be the term Xi_i ∖ U.

We prove the intermediate claim HCcl: closed_in Xi_i Ti_i C.

An exact proof term for the current goal is (closed_of_open_complement Xi_i Ti_i U HTi HUopen).

We prove the intermediate claim HxiNotC: apply_fun x i ∉ C.

Assume HxiC: apply_fun x i ∈ C.

We prove the intermediate claim HxiNotU: apply_fun x i ∉ U.

An exact proof term for the current goal is (setminusE2 Xi_i U (apply_fun x i) HxiC).

An exact proof term for the current goal is (HxiNotU HxiU).

We prove the intermediate claim Hcri: completely_regular_space Xi_i Ti_i.

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

We prove the intermediate claim Hsep_i: ∀xi : set, xi ∈ Xi_i → ∀Fcl : set, closed_in Xi_i Ti_i Fcl → xi ∉ Fcl → ∃fi : set, continuous_map Xi_i Ti_i R R_standard_topology fi ∧ apply_fun fi xi = 0 ∧ ∀z : set, z ∈ Fcl → apply_fun fi z = 1.

Let xi be given.

Assume Hxi: xi ∈ Xi_i.

Let Fcl be given.

Assume HFcl: closed_in Xi_i Ti_i Fcl.

Assume HxiNotFcl: xi ∉ Fcl.

An exact proof term for the current goal is (completely_regular_space_separation Xi_i Ti_i xi Fcl Hcri Hxi HFcl HxiNotFcl).

We prove the intermediate claim Hexfi: ∃fi : set, continuous_map Xi_i Ti_i R R_standard_topology fi ∧ apply_fun fi (apply_fun x i) = 0 ∧ ∀z : set, z ∈ C → apply_fun fi z = 1.

An exact proof term for the current goal is (Hsep_i (apply_fun x i) HxiXi C HCcl HxiNotC).

Apply Hexfi to the current goal.

Let fi be given.

Assume Hfipack.

Set ev to be the term product_eval_map I Xi i.

Set g0 to be the term compose_fun Xp ev fi.

We use g0 to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim Hevcont: continuous_map Xp Tp Xi_i Ti_i ev.

An exact proof term for the current goal is (product_eval_map_continuous I Xi i HcompTop HiI).

We prove the intermediate claim HfiLeft: continuous_map Xi_i Ti_i R R_standard_topology fi ∧ apply_fun fi (apply_fun x i) = 0.

An exact proof term for the current goal is (andEL (continuous_map Xi_i Ti_i R R_standard_topology fi ∧ apply_fun fi (apply_fun x i) = 0) (∀z : set, z ∈ C → apply_fun fi z = 1) Hfipack).

We prove the intermediate claim HfiCont: continuous_map Xi_i Ti_i R R_standard_topology fi.

An exact proof term for the current goal is (andEL (continuous_map Xi_i Ti_i R R_standard_topology fi) (apply_fun fi (apply_fun x i) = 0) HfiLeft).

An exact proof term for the current goal is (composition_continuous Xp Tp Xi_i Ti_i R R_standard_topology ev fi Hevcont HfiCont).

We prove the intermediate claim Hg0x: apply_fun g0 x = apply_fun fi (apply_fun ev x).

An exact proof term for the current goal is (compose_fun_apply Xp ev fi x HxXp).

We prove the intermediate claim Hevx: apply_fun ev x = apply_fun x i.

An exact proof term for the current goal is (apply_fun_graph Xp (λu0 : set ⇒ apply_fun u0 i) x HxXp).

We prove the intermediate claim HfiLeft: continuous_map Xi_i Ti_i R R_standard_topology fi ∧ apply_fun fi (apply_fun x i) = 0.

An exact proof term for the current goal is (andEL (continuous_map Xi_i Ti_i R R_standard_topology fi ∧ apply_fun fi (apply_fun x i) = 0) (∀z : set, z ∈ C → apply_fun fi z = 1) Hfipack).

We prove the intermediate claim Hfi0: apply_fun fi (apply_fun x i) = 0.

An exact proof term for the current goal is (andER (continuous_map Xi_i Ti_i R R_standard_topology fi) (apply_fun fi (apply_fun x i) = 0) HfiLeft).

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

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

An exact proof term for the current goal is Hfi0.

Let y be given.

Assume HyXp: y ∈ Xp.

Assume Hynoty0: y ∉ y0.

We will prove apply_fun g0 y = 1.

We prove the intermediate claim HynotCyl: y ∉ product_cylinder I Xi i U.

rewrite the current goal using Hy0eq (from right to left) at position 1.

An exact proof term for the current goal is Hynoty0.

We prove the intermediate claim HyNotU: apply_fun y i ∉ U.

Assume HyiU: apply_fun y i ∈ U.

We prove the intermediate claim HyCyl: y ∈ product_cylinder I Xi i U.

We prove the intermediate claim HXpeq: Xp = product_space I Xi.

Use reflexivity.

We prove the intermediate claim HyPS: y ∈ product_space I Xi.

rewrite the current goal using HXpeq (from right to left) at position 1.

An exact proof term for the current goal is HyXp.

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

Use reflexivity.

rewrite the current goal using Hcyldef (from left to right) at position 1.

Apply (SepI (product_space I Xi) (λf0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) y HyPS) to the current goal.

An exact proof term for the current goal is (andI (i ∈ I ∧ U ∈ space_family_topology Xi i) (apply_fun y i ∈ U) (andI (i ∈ I) (U ∈ space_family_topology Xi i) HiI HUopen) HyiU).

An exact proof term for the current goal is (HynotCyl HyCyl).

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

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

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

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

We prove the intermediate claim HyiXi: apply_fun y i ∈ Xi_i.

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

We prove the intermediate claim HyC: apply_fun y i ∈ C.

An exact proof term for the current goal is (setminusI Xi_i U (apply_fun y i) HyiXi HyNotU).

We prove the intermediate claim HfiRight: ∀z : set, z ∈ C → apply_fun fi z = 1.

An exact proof term for the current goal is (andER (continuous_map Xi_i Ti_i R R_standard_topology fi ∧ apply_fun fi (apply_fun x i) = 0) (∀z : set, z ∈ C → apply_fun fi z = 1) Hfipack).

We prove the intermediate claim Hfiy: apply_fun fi (apply_fun y i) = 1.

An exact proof term for the current goal is (HfiRight (apply_fun y i) HyC).

We prove the intermediate claim Hg0y: apply_fun g0 y = apply_fun fi (apply_fun ev y).

An exact proof term for the current goal is (compose_fun_apply Xp ev fi y HyXp).

We prove the intermediate claim Hevy: apply_fun ev y = apply_fun y i.

An exact proof term for the current goal is (apply_fun_graph Xp (λu0 : set ⇒ apply_fun u0 i) y HyXp).

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

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

An exact proof term for the current goal is Hfiy.

Apply Hexg0 to the current goal.

Let g0 be given.

Assume Hg0pack.

We prove the intermediate claim Hf0cont: continuous_map Xp Tp R R_standard_topology f0.

An exact proof term for the current goal is (andEL (continuous_map Xp Tp R R_standard_topology f0) (apply_fun f0 x = 0) (andEL (continuous_map Xp Tp R R_standard_topology f0 ∧ apply_fun f0 x = 0) (∀y : set, y ∈ Xp → (∃s : set, s ∈ X0 ∧ y ∉ s) → apply_fun f0 y = 1) Hf0pack)).

We prove the intermediate claim Hf0x0: apply_fun f0 x = 0.

An exact proof term for the current goal is (andER (continuous_map Xp Tp R R_standard_topology f0) (apply_fun f0 x = 0) (andEL (continuous_map Xp Tp R R_standard_topology f0 ∧ apply_fun f0 x = 0) (∀y : set, y ∈ Xp → (∃s : set, s ∈ X0 ∧ y ∉ s) → apply_fun f0 y = 1) Hf0pack)).

We prove the intermediate claim Hf0sep: ∀y : set, y ∈ Xp → (∃s : set, s ∈ X0 ∧ y ∉ s) → apply_fun f0 y = 1.

An exact proof term for the current goal is (andER (continuous_map Xp Tp R R_standard_topology f0 ∧ apply_fun f0 x = 0) (∀y : set, y ∈ Xp → (∃s : set, s ∈ X0 ∧ y ∉ s) → apply_fun f0 y = 1) Hf0pack).

We prove the intermediate claim Hg0cont: continuous_map Xp Tp R R_standard_topology g0.

An exact proof term for the current goal is (andEL (continuous_map Xp Tp R R_standard_topology g0) (apply_fun g0 x = 0) (andEL (continuous_map Xp Tp R R_standard_topology g0 ∧ apply_fun g0 x = 0) (∀y : set, y ∈ Xp → y ∉ y0 → apply_fun g0 y = 1) Hg0pack)).

We prove the intermediate claim Hg0x0: apply_fun g0 x = 0.

An exact proof term for the current goal is (andER (continuous_map Xp Tp R R_standard_topology g0) (apply_fun g0 x = 0) (andEL (continuous_map Xp Tp R R_standard_topology g0 ∧ apply_fun g0 x = 0) (∀y : set, y ∈ Xp → y ∉ y0 → apply_fun g0 y = 1) Hg0pack)).

We prove the intermediate claim Hg0sep: ∀y : set, y ∈ Xp → y ∉ y0 → apply_fun g0 y = 1.

An exact proof term for the current goal is (andER (continuous_map Xp Tp R R_standard_topology g0 ∧ apply_fun g0 x = 0) (∀y : set, y ∈ Xp → y ∉ y0 → apply_fun g0 y = 1) Hg0pack).

We prove the intermediate claim Hexh: ∃h : set, continuous_map Xp Tp R R_standard_topology h ∧ apply_fun h x = 0 ∧ ∀y : set, y ∈ Xp → (apply_fun f0 y = 1 ∨ apply_fun g0 y = 1) → apply_fun h y = 1.

An exact proof term for the current goal is (continuous_combine_or_01 Xp Tp f0 g0 x HTp Hf0cont Hg0cont HxXp Hf0x0 Hg0x0).

Apply Hexh to the current goal.

Let h be given.

Assume Hhpack.

We use h to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (continuous_map Xp Tp R R_standard_topology h ∧ apply_fun h x = 0) (∀y : set, y ∈ Xp → (apply_fun f0 y = 1 ∨ apply_fun g0 y = 1) → apply_fun h y = 1) Hhpack).

Let y be given.

Assume HyXp: y ∈ Xp.

Assume Hexs: ∃s : set, s ∈ X0 ∪ {y0} ∧ y ∉ s.

We will prove apply_fun h y = 1.

We prove the intermediate claim HhOr: ∀y0 : set, y0 ∈ Xp → (apply_fun f0 y0 = 1 ∨ apply_fun g0 y0 = 1) → apply_fun h y0 = 1.

An exact proof term for the current goal is (andER (continuous_map Xp Tp R R_standard_topology h ∧ apply_fun h x = 0) (∀y0 : set, y0 ∈ Xp → (apply_fun f0 y0 = 1 ∨ apply_fun g0 y0 = 1) → apply_fun h y0 = 1) Hhpack).

Apply Hexs to the current goal.

Let s be given.

Assume Hsand.

We prove the intermediate claim HsX1: s ∈ X0 ∪ {y0}.

An exact proof term for the current goal is (andEL (s ∈ X0 ∪ {y0}) (y ∉ s) Hsand).

We prove the intermediate claim HynotS: y ∉ s.

An exact proof term for the current goal is (andER (s ∈ X0 ∪ {y0}) (y ∉ s) Hsand).

We prove the intermediate claim Hcases: s ∈ X0 ∨ s ∈ {y0}.

An exact proof term for the current goal is (binunionE X0 {y0} s HsX1).

We prove the intermediate claim Hcases3: s ∈ X0 ∨ s ∈ {y0} ∨ False.

An exact proof term for the current goal is (orIL (s ∈ X0 ∨ s ∈ {y0}) False Hcases).

Apply (or3E (s ∈ X0) (s ∈ {y0}) False Hcases3 (apply_fun h y = 1)) to the current goal.

Assume HsX0: s ∈ X0.

We prove the intermediate claim Hdisj: ∃s0 : set, s0 ∈ X0 ∧ y ∉ s0.

We use s to witness the existential quantifier.

An exact proof term for the current goal is (andI (s ∈ X0) (y ∉ s) HsX0 HynotS).

We prove the intermediate claim Hf0y: apply_fun f0 y = 1.

An exact proof term for the current goal is (Hf0sep y HyXp Hdisj).

We prove the intermediate claim Hor: apply_fun f0 y = 1 ∨ apply_fun g0 y = 1.

An exact proof term for the current goal is (orIL (apply_fun f0 y = 1) (apply_fun g0 y = 1) Hf0y).

An exact proof term for the current goal is (HhOr y HyXp Hor).

Assume HsSing: s ∈ {y0}.

We prove the intermediate claim Hseq: s = y0.

An exact proof term for the current goal is (SingE y0 s HsSing).

We prove the intermediate claim Hynoty0: y ∉ y0.

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

An exact proof term for the current goal is HynotS.

We prove the intermediate claim Hg0y: apply_fun g0 y = 1.

An exact proof term for the current goal is (Hg0sep y HyXp Hynoty0).

We prove the intermediate claim Hor: apply_fun f0 y = 1 ∨ apply_fun g0 y = 1.

An exact proof term for the current goal is (orIR (apply_fun f0 y = 1) (apply_fun g0 y = 1) Hg0y).

An exact proof term for the current goal is (HhOr y HyXp Hor).

Assume Hbad: False.

An exact proof term for the current goal is (FalseE Hbad (apply_fun h y = 1)).