Assume Hconv: converges_to X Tx seq x.

We will prove net_converges_on X Tx (sequence_as_net seq) ω (inclusion_rel ω) x.

Set net0 to be the term sequence_as_net seq.

We prove the intermediate claim Hdefnet: net0 = graph ω (λn : set ⇒ apply_fun seq n).

Use reflexivity.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (converges_to_topology X Tx seq x Hconv).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (converges_to_point_in_X X Tx seq x Hconv).

We prove the intermediate claim Hnbhd: ∀U : set, U ∈ Tx → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.

An exact proof term for the current goal is (converges_to_neighborhoods X Tx seq x Hconv).

We prove the intermediate claim Htotnet: total_function_on net0 ω X.

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

We prove the intermediate claim Hg: ∀n : set, n ∈ ω → apply_fun seq n ∈ X.

Let n be given.

Assume Hn: n ∈ ω.

An exact proof term for the current goal is (Hseq n Hn).

An exact proof term for the current goal is (total_function_on_graph ω X (λn : set ⇒ apply_fun seq n) Hg).

We prove the intermediate claim Hgraphnet: functional_graph net0.

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

An exact proof term for the current goal is (functional_graph_graph ω (λn : set ⇒ apply_fun seq n)).

We prove the intermediate claim Hdomnet: graph_domain_subset net0 ω.

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

An exact proof term for the current goal is (graph_domain_subset_graph ω (λn : set ⇒ apply_fun seq n)).

We will prove topology_on X Tx ∧ directed_set ω (inclusion_rel ω) ∧ total_function_on net0 ω X ∧ functional_graph net0 ∧ graph_domain_subset net0 ω ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ ω ∧ ∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun net0 i ∈ U.

Apply and7I to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is omega_directed_by_inclusion_rel.

An exact proof term for the current goal is Htotnet.

An exact proof term for the current goal is Hgraphnet.

An exact proof term for the current goal is Hdomnet.

An exact proof term for the current goal is HxX.

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

Apply (Hnbhd U HU HxU) to the current goal.

Let N be given.

Assume HNpair: N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.

We prove the intermediate claim HNomega: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) HNpair).

We prove the intermediate claim Hevent: ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.

An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) HNpair).

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HNomega.

Let i be given.

Assume Hi: i ∈ ω.

Assume Hle: (N,i) ∈ inclusion_rel ω.

We will prove apply_fun net0 i ∈ U.

We prove the intermediate claim HNsubi: N ⊆ i.

An exact proof term for the current goal is (andER ((N,i) ∈ setprod ω ω) (N ⊆ i) (inclusion_relE ω N i Hle)).

We prove the intermediate claim Hseqi: apply_fun seq i ∈ U.

An exact proof term for the current goal is (Hevent i Hi HNsubi).

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

rewrite the current goal using (apply_fun_graph ω (λn : set ⇒ apply_fun seq n) i Hi) (from left to right).

An exact proof term for the current goal is Hseqi.

Assume Hnet: net_converges_on X Tx (sequence_as_net seq) ω (inclusion_rel ω) x.

We will prove converges_to X Tx seq x.

We prove the intermediate claim Hleft: (((((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)) ∧ graph_domain_subset (sequence_as_net seq) ω) ∧ x ∈ X).

An exact proof term for the current goal is (andEL (((((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)) ∧ graph_domain_subset (sequence_as_net seq) ω) ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ ω ∧ ∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun (sequence_as_net seq) i ∈ U) Hnet).

We prove the intermediate claim Hevent: ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ ω ∧ ∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun (sequence_as_net seq) i ∈ U.

An exact proof term for the current goal is (andER (((((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)) ∧ graph_domain_subset (sequence_as_net seq) ω) ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ ω ∧ ∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun (sequence_as_net seq) i ∈ U) Hnet).

We prove the intermediate claim Hleft5: ((((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)) ∧ graph_domain_subset (sequence_as_net seq) ω).

An exact proof term for the current goal is (andEL ((((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)) ∧ graph_domain_subset (sequence_as_net seq) ω) (x ∈ X) Hleft).

We prove the intermediate claim Hx: x ∈ X.

An exact proof term for the current goal is (andER ((((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)) ∧ graph_domain_subset (sequence_as_net seq) ω) (x ∈ X) Hleft).

We prove the intermediate claim Hleft4: (((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)).

An exact proof term for the current goal is (andEL (((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) ∧ functional_graph (sequence_as_net seq)) (graph_domain_subset (sequence_as_net seq) ω) Hleft5).

We prove the intermediate claim Hleft3: ((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X).

An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) ∧ total_function_on (sequence_as_net seq) ω X) (functional_graph (sequence_as_net seq)) Hleft4).

We prove the intermediate claim Hleft2: topology_on X Tx ∧ directed_set ω (inclusion_rel ω).

An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set ω (inclusion_rel ω)) (total_function_on (sequence_as_net seq) ω X) Hleft3).

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (andEL (topology_on X Tx) (directed_set ω (inclusion_rel ω)) Hleft2).

We will prove topology_on X Tx ∧ sequence_on seq X ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is Hseq.

An exact proof term for the current goal is Hx.

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

Apply (Hevent U HU HxU) to the current goal.

Let i0 be given.

Assume Hi0pair: i0 ∈ ω ∧ ∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun (sequence_as_net seq) i ∈ U.

We prove the intermediate claim Hi0omega: i0 ∈ ω.

An exact proof term for the current goal is (andEL (i0 ∈ ω) (∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun (sequence_as_net seq) i ∈ U) Hi0pair).

We prove the intermediate claim Hevent0: ∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun (sequence_as_net seq) i ∈ U.

An exact proof term for the current goal is (andER (i0 ∈ ω) (∀i : set, i ∈ ω → (i0,i) ∈ inclusion_rel ω → apply_fun (sequence_as_net seq) i ∈ U) Hi0pair).

We use i0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hi0omega.

Let n be given.

Assume Hn: n ∈ ω.

Assume Hi0subn: i0 ⊆ n.

We will prove apply_fun seq n ∈ U.

We prove the intermediate claim Hle: (i0,n) ∈ inclusion_rel ω.

Apply (inclusion_relI ω i0 n) to the current goal.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω ω i0 n Hi0omega Hn).

An exact proof term for the current goal is Hi0subn.

We prove the intermediate claim Hnetn: apply_fun (sequence_as_net seq) n ∈ U.

An exact proof term for the current goal is (Hevent0 n Hn Hle).

We prove the intermediate claim Hdef: sequence_as_net seq = graph ω (λk : set ⇒ apply_fun seq k).

Use reflexivity.

We prove the intermediate claim Happ: apply_fun (sequence_as_net seq) n = apply_fun seq n.

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

An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ apply_fun seq k) n Hn).

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

An exact proof term for the current goal is Hnetn.