Let X, Tx, F, J, x and y be given.
Assume HTx: topology_on X Tx.
Assume HT1: one_point_sets_closed X Tx.
Assume Hsep: separating_family_of_functions X Tx F J.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume Hxy: x ≠ y.
We will prove ∃j : set, j ∈ J ∧ apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y.
We prove the intermediate claim HyCl: closed_in X Tx {y}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) HT1 y HyX).
Set U to be the term X ∖ {y}.
We prove the intermediate claim HUopen_in: open_in X Tx U.
We prove the intermediate claim HUdef: U = X ∖ {y}.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is (open_of_closed_complement X Tx {y} HyCl).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U HUopen_in).
We prove the intermediate claim HxU: x ∈ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume Hxy0: x ∈ {y}.
We prove the intermediate claim Heq: x = y.
An exact proof term for the current goal is (SingE y x Hxy0).
An exact proof term for the current goal is (Hxy Heq).
We prove the intermediate claim Hneigh: ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x) ∧ ∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0.
We prove the intermediate claim HsepABC: (topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j)).
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀z : set, z ∈ X ∖ U0 → apply_fun (apply_fun F j) z = 0) Hsep).
We prove the intermediate claim HsepD: ∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀z : set, z ∈ X ∖ U0 → apply_fun (apply_fun F j) z = 0.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j : set, j ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j : set, j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x0) ∧ ∀z : set, z ∈ X ∖ U0 → apply_fun (apply_fun F j) z = 0) Hsep).
An exact proof term for the current goal is (HsepD x HxX U HUopen HxU).
Apply Hneigh to the current goal.
Let j be given.
Assume Hj: j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x) ∧ ∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0.
We use j to witness the existential quantifier.
We prove the intermediate claim Hj12: j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (andEL (j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x)) (∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0) Hj).
We prove the intermediate claim Hz0: ∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0.
An exact proof term for the current goal is (andER (j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x)) (∀z : set, z ∈ X ∖ U → apply_fun (apply_fun F j) z = 0) Hj).
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) (Rlt 0 (apply_fun (apply_fun F j) x)) Hj12).
We prove the intermediate claim Hpos: Rlt 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (andER (j ∈ J) (Rlt 0 (apply_fun (apply_fun F j) x)) Hj12).
We prove the intermediate claim HyIn: y ∈ X ∖ U.
We prove the intermediate claim HsingSub: {y} ⊆ X.
An exact proof term for the current goal is (singleton_subset y X HyX).
We prove the intermediate claim HUdef: U = X ∖ {y}.
Use reflexivity.
We prove the intermediate claim Heq: X ∖ U = {y}.
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is (setminus_setminus_eq X {y} HsingSub).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI y).
We prove the intermediate claim Hy0: apply_fun (apply_fun F j) y = 0.
An exact proof term for the current goal is (Hz0 y HyIn).
Apply andI to the current goal.
An exact proof term for the current goal is HjJ.
Assume Heq: apply_fun (apply_fun F j) x = apply_fun (apply_fun F j) y.
We will prove False.
We prove the intermediate claim Hx0: apply_fun (apply_fun F j) x = 0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hy0.
We prove the intermediate claim Hpos0: Rlt 0 0.
rewrite the current goal using Hx0 (from right to left) at position 2.
An exact proof term for the current goal is Hpos.
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hpos0).
∎