Let X, Tx, net and x be given.
Assume H: net_converges X Tx net x.
Apply H to the current goal.
Let J be given.
Assume Hexle: ∃le : set, topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
Apply Hexle to the current goal.
Let le be given.
Assume Hdata: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
We will prove net_in_space X net.
We will prove ∃J0 le0 : set, directed_set J0 le0 ∧ total_function_on net J0 X ∧ functional_graph net ∧ graph_domain_subset net J0.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
Apply Hdata to the current goal.
Assume Hcore Hevent.
Apply Hcore to the current goal.
Assume Hcore5 HxX.
Apply Hcore5 to the current goal.
Assume Hcore4 Hdom.
Apply Hcore4 to the current goal.
Assume Hcore3 Hgraph.
Apply Hcore3 to the current goal.
Assume Hcore2 Htot.
Apply Hcore2 to the current goal.
Assume HTx Hdir.
An exact proof term for the current goal is (and4I (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) Hdir Htot Hgraph Hdom).
∎