We prove the intermediate claim HconvS: net_pack_converges Hcand Thcand S xprod.

We prove the intermediate claim Hdef: net_pack_converges Hcand Thcand S xprod = ∃J0 le0 net0 : set, S = net_pack J0 le0 net0 ∧ net_converges_on Hcand Thcand net0 J0 le0 xprod.

Use reflexivity.

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

We use K to witness the existential quantifier.

We use leK to witness the existential quantifier.

We use subNet to witness the existential quantifier.

Apply andI to the current goal.

Use reflexivity.

We prove the intermediate claim HNprodDef: Nprod = net_pack J le netP.

Use reflexivity.

We prove the intermediate claim HNidx: net_pack_index Nprod = J.

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

An exact proof term for the current goal is (net_pack_index_eq J le netP).

We prove the intermediate claim HNle: net_pack_le Nprod = le.

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

An exact proof term for the current goal is (net_pack_le_eq J le netP).

We prove the intermediate claim HsubProd: subnet_of_witness (net_pack_fun Nprod) (net_pack_fun Sprod) J le K leK P phi.

We prove the intermediate claim Hsub0: subnet_of_witness (net_pack_fun Nprod) (net_pack_fun Sprod) (net_pack_index Nprod) (net_pack_le Nprod) K leK P phi.

An exact proof term for the current goal is Hphi.

Apply (subnet_of_witness_congr (net_pack_fun Nprod) (net_pack_fun Nprod) (net_pack_fun Sprod) (net_pack_fun Sprod) (net_pack_index Nprod) J (net_pack_le Nprod) le K K leK leK P phi) to the current goal.

Use reflexivity.

An exact proof term for the current goal is HNidx.

An exact proof term for the current goal is HNle.

Use reflexivity.

An exact proof term for the current goal is Hsub0.

We prove the intermediate claim HdirK: directed_set K leK.

An exact proof term for the current goal is (subnet_of_witness_dirK (net_pack_fun Nprod) (net_pack_fun Sprod) J le K leK P phi HsubProd).

We prove the intermediate claim Htotphi: total_function_on phi K J.

An exact proof term for the current goal is (subnet_of_witness_totphi (net_pack_fun Nprod) (net_pack_fun Sprod) J le K leK P phi HsubProd).

We prove the intermediate claim HsubNetDef: subNet = compose_fun K phi net.

Use reflexivity.

We prove the intermediate claim Htotsub: total_function_on subNet K Hcand.

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

An exact proof term for the current goal is (total_function_on_compose_fun K J Hcand phi net (total_function_on_function_on phi K J Htotphi) (total_function_on_function_on net J Hcand Htot)).

We prove the intermediate claim HgraphSub: functional_graph subNet.

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

An exact proof term for the current goal is (functional_graph_compose_fun K phi net).

We prove the intermediate claim HdomSub: graph_domain_subset subNet K.

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

An exact proof term for the current goal is (graph_domain_subset_compose_fun K phi net).

We will prove net_converges_on Hcand Thcand subNet K leK xprod.

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

We prove the intermediate claim HTcc: topology_on CXY Tcc.

An exact proof term for the current goal is (compact_convergence_topology_metric_C_is_topology X Tx Y dY HTx HdY).

Set Dom to be the term function_space X Y.

Set Tpt to be the term pointwise_convergence_topology X Tx Y Ty.

We prove the intermediate claim HxprodInHcand: xprod ∈ Hcand ∧ net_converges_on Dom Tpt subNet K leK xprod.

We prove the intermediate claim HTpt: topology_on Dom Tpt.

An exact proof term for the current goal is (pointwise_convergence_topology_is_topology X Tx Y Ty HTx HTy).

We prove the intermediate claim HFsubDom: F ⊆ Dom.

Let f be given.

Assume HfF: f ∈ F.

We prove the intermediate claim HfC: f ∈ CXY.

An exact proof term for the current goal is (HFcont f HfF).

An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty f HfC).

We prove the intermediate claim Hclosed: closed_in Dom Tpt Hcand.

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

An exact proof term for the current goal is (Ascoli_g_pointwise_closure_closed X Tx Y dY F HTpt HFsubDom).

We prove the intermediate claim Hpkg: Hcand ⊆ Dom ∧ ∃U ∈ Tpt, Hcand = Dom ∖ U.

An exact proof term for the current goal is (closed_in_package Dom Tpt Hcand Hclosed).

We prove the intermediate claim HHcandSubDom: Hcand ⊆ Dom.

An exact proof term for the current goal is (andEL (Hcand ⊆ Dom) (∃U ∈ Tpt, Hcand = Dom ∖ U) Hpkg).

We prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ Tpt ∧ Hcand = Dom ∖ U0.

An exact proof term for the current goal is (andER (Hcand ⊆ Dom) (∃U ∈ Tpt, Hcand = Dom ∖ U) Hpkg).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0pair: U0 ∈ Tpt ∧ Hcand = Dom ∖ U0.

We prove the intermediate claim HU0Tpt: U0 ∈ Tpt.

An exact proof term for the current goal is (andEL (U0 ∈ Tpt) (Hcand = Dom ∖ U0) HU0pair).

We prove the intermediate claim HHcandEq: Hcand = Dom ∖ U0.

An exact proof term for the current goal is (andER (U0 ∈ Tpt) (Hcand = Dom ∖ U0) HU0pair).

We prove the intermediate claim HxprodP: xprod ∈ P.

An exact proof term for the current goal is (net_pack_converges_implies_x_in_space P Tp Sprod xprod HconvProd).

We prove the intermediate claim HunionSubY: space_family_union X XiKa ⊆ Y.

Let y be given.

Assume HyU: y ∈ space_family_union X XiKa.

We will prove y ∈ Y.

We prove the intermediate claim HyU': y ∈ ⋃ {space_family_set XiKa i|i ∈ X}.

We prove the intermediate claim Hdef: space_family_union X XiKa = ⋃ {space_family_set XiKa i|i ∈ X}.

Use reflexivity.

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

An exact proof term for the current goal is HyU.

Apply (UnionE_impred {space_family_set XiKa i|i ∈ X} y HyU') to the current goal.

Let A be given.

Assume HyA: y ∈ A.

Assume HA: A ∈ {space_family_set XiKa i|i ∈ X}.

Apply (ReplE_impred X (λi : set ⇒ space_family_set XiKa i) A HA (y ∈ Y)) to the current goal.

Let a be given.

Assume HaX: a ∈ X.

Assume HAeq: A = space_family_set XiKa a.

We prove the intermediate claim HyA0: y ∈ space_family_set XiKa a.

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

An exact proof term for the current goal is HyA.

We prove the intermediate claim HyA1: y ∈ closure_of Y Ty (Ascoli_F_at X Y a F).

rewrite the current goal using (Ascoli_XiKa_set X Y Ty F a HaX) (from right to left) at position 1.

An exact proof term for the current goal is HyA0.

An exact proof term for the current goal is (closure_in_space Y Ty (Ascoli_F_at X Y a F) HTy y HyA1).

We prove the intermediate claim Hxprop: (total_function_on xprod X (space_family_union X XiKa) ∧ functional_graph xprod) ∧ ∀i : set, i ∈ X → apply_fun xprod i ∈ space_family_set XiKa i.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod X (space_family_union X XiKa))) (λf0 : set ⇒ (total_function_on f0 X (space_family_union X XiKa) ∧ functional_graph f0) ∧ ∀i : set, i ∈ X → apply_fun f0 i ∈ space_family_set XiKa i) xprod HxprodP).

We prove the intermediate claim HtotXU: total_function_on xprod X (space_family_union X XiKa).

We prove the intermediate claim Htf: total_function_on xprod X (space_family_union X XiKa) ∧ functional_graph xprod.

An exact proof term for the current goal is (andEL (total_function_on xprod X (space_family_union X XiKa) ∧ functional_graph xprod) (∀i : set, i ∈ X → apply_fun xprod i ∈ space_family_set XiKa i) Hxprop).

An exact proof term for the current goal is (andEL (total_function_on xprod X (space_family_union X XiKa)) (functional_graph xprod) Htf).

We prove the intermediate claim HtotXY: total_function_on xprod X Y.

An exact proof term for the current goal is (total_function_on_codomain xprod X (space_family_union X XiKa) Y HtotXU HunionSubY).

We prove the intermediate claim HfunXY: function_on xprod X Y.

An exact proof term for the current goal is (total_function_on_function_on xprod X Y HtotXY).

We prove the intermediate claim HxprodInDom: xprod ∈ Dom.

We prove the intermediate claim Hpow0: xprod ∈ 𝒫 (setprod X (space_family_union X XiKa)).

An exact proof term for the current goal is (SepE1 (𝒫 (setprod X (space_family_union X XiKa))) (λf0 : set ⇒ (total_function_on f0 X (space_family_union X XiKa) ∧ functional_graph f0) ∧ ∀i : set, i ∈ X → apply_fun f0 i ∈ space_family_set XiKa i) xprod HxprodP).

We prove the intermediate claim Hsub0: xprod ⊆ setprod X (space_family_union X XiKa).

Let p be given.

Assume Hp: p ∈ xprod.

An exact proof term for the current goal is (PowerE (setprod X (space_family_union X XiKa)) xprod Hpow0 p Hp).

We prove the intermediate claim HsetprodSub: setprod X (space_family_union X XiKa) ⊆ setprod X Y.

An exact proof term for the current goal is (setprod_Subq X (space_family_union X XiKa) X Y (Subq_ref X) HunionSubY).

We prove the intermediate claim Hsub: xprod ⊆ setprod X Y.

Let p be given.

Assume Hp: p ∈ xprod.

An exact proof term for the current goal is (HsetprodSub p (Hsub0 p Hp)).

We prove the intermediate claim Hpow: xprod ∈ 𝒫 (setprod X Y).

An exact proof term for the current goal is (PowerI (setprod X Y) xprod Hsub).

An exact proof term for the current goal is (SepI (𝒫 (setprod X Y)) (λf0 : set ⇒ function_on f0 X Y) xprod Hpow HfunXY).

Set Spt to be the term (pointwise_subbasis X Tx Y Ty) ∪ {Dom}.

We prove the intermediate claim HSpt: subbasis_on Dom Spt.

We will prove Spt ⊆ 𝒫 Dom ∧ ⋃ Spt = Dom.

Apply andI to the current goal.

Let s be given.

Assume Hs: s ∈ Spt.

We will prove s ∈ 𝒫 Dom.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} s (s ∈ 𝒫 Dom)) to the current goal.

Assume Hsp: s ∈ pointwise_subbasis X Tx Y Ty.

An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x U : set, x ∈ X ∧ U ∈ Ty ∧ S0 = {f ∈ Dom|apply_fun f x ∈ U}) s Hsp).

Assume HsDom: s ∈ {Dom}.

We prove the intermediate claim Hseq: s = Dom.

An exact proof term for the current goal is (SingE Dom s HsDom).

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

An exact proof term for the current goal is (PowerI Dom Dom (Subq_ref Dom)).

An exact proof term for the current goal is Hs.

Apply set_ext to the current goal.

Let f be given.

Assume HfU: f ∈ ⋃ Spt.

We will prove f ∈ Dom.

Apply (UnionE_impred Spt f HfU (f ∈ Dom)) to the current goal.

Let U be given.

Assume HfU0: f ∈ U.

Assume HU: U ∈ Spt.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} U (f ∈ Dom)) to the current goal.

Assume HUp: U ∈ pointwise_subbasis X Tx Y Ty.

We prove the intermediate claim HUpow: U ∈ 𝒫 Dom.

An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x U0 : set, x ∈ X ∧ U0 ∈ Ty ∧ S0 = {f0 ∈ Dom|apply_fun f0 x ∈ U0}) U HUp).

An exact proof term for the current goal is (PowerE Dom U HUpow f HfU0).

Assume HUDom: U ∈ {Dom}.

We prove the intermediate claim HUeq: U = Dom.

An exact proof term for the current goal is (SingE Dom U HUDom).

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

An exact proof term for the current goal is HfU0.

An exact proof term for the current goal is HU.

Let f be given.

Assume HfD: f ∈ Dom.

We prove the intermediate claim HDomInS: Dom ∈ Spt.

An exact proof term for the current goal is (binunionI2 (pointwise_subbasis X Tx Y Ty) {Dom} Dom (SingI Dom)).

An exact proof term for the current goal is (UnionI Spt f Dom HfD HDomInS).

We prove the intermediate claim HtotsubDom: total_function_on subNet K Dom.

An exact proof term for the current goal is (total_function_on_codomain subNet K Hcand Dom Htotsub HHcandSubDom).

We prove the intermediate claim HevSpt: ∀s : set, s ∈ Spt → xprod ∈ s → ∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ s.

Let s be given.

Assume HsS: s ∈ Spt.

Assume Hxps: xprod ∈ s.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} s (∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ s)) to the current goal.

Assume Hsp: s ∈ pointwise_subbasis X Tx Y Ty.

We prove the intermediate claim Hex: ∃a U : set, a ∈ X ∧ U ∈ Ty ∧ s = {f ∈ Dom|apply_fun f a ∈ U}.

An exact proof term for the current goal is (SepE2 (𝒫 Dom) (λS0 : set ⇒ ∃x U0 : set, x ∈ X ∧ U0 ∈ Ty ∧ S0 = {f0 ∈ Dom|apply_fun f0 x ∈ U0}) s Hsp).

Apply Hex to the current goal.

Let a be given.

Assume HexU: ∃U : set, a ∈ X ∧ U ∈ Ty ∧ s = {f ∈ Dom|apply_fun f a ∈ U}.

Apply HexU to the current goal.

Let U be given.

Assume Hdef: a ∈ X ∧ U ∈ Ty ∧ s = {f ∈ Dom|apply_fun f a ∈ U}.

We prove the intermediate claim Hab: a ∈ X ∧ U ∈ Ty.

An exact proof term for the current goal is (andEL (a ∈ X ∧ U ∈ Ty) (s = {f ∈ Dom|apply_fun f a ∈ U}) Hdef).

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (andEL (a ∈ X) (U ∈ Ty) Hab).

We prove the intermediate claim HUty: U ∈ Ty.

An exact proof term for the current goal is (andER (a ∈ X) (U ∈ Ty) Hab).

We prove the intermediate claim Hseq: s = {f ∈ Dom|apply_fun f a ∈ U}.

An exact proof term for the current goal is (andER (a ∈ X ∧ U ∈ Ty) (s = {f ∈ Dom|apply_fun f a ∈ U}) Hdef).

We prove the intermediate claim HappU: apply_fun xprod a ∈ U.

We prove the intermediate claim Hxps0: xprod ∈ {f ∈ Dom|apply_fun f a ∈ U}.

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

An exact proof term for the current goal is Hxps.

An exact proof term for the current goal is (SepE2 Dom (λf0 : set ⇒ apply_fun f0 a ∈ U) xprod Hxps0).

Set Ka to be the term closure_of Y Ty (Ascoli_F_at X Y a F).

We prove the intermediate claim HKaTop: topology_on Ka (subspace_topology Y Ty Ka).

An exact proof term for the current goal is (subspace_topology_is_topology Y Ty Ka HTy (closure_in_space Y Ty (Ascoli_F_at X Y a F) HTy)).

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

Let i be given.

Assume HiX: i ∈ X.

rewrite the current goal using (Ascoli_XiKa_set X Y Ty F i HiX) (from left to right).

rewrite the current goal using (Ascoli_XiKa_topology X Y Ty F i HiX) (from left to right).

An exact proof term for the current goal is (subspace_topology_is_topology Y Ty (closure_of Y Ty (Ascoli_F_at X Y i F)) HTy (closure_in_space Y Ty (Ascoli_F_at X Y i F) HTy)).

We prove the intermediate claim HconvProdOn: net_converges_on P Tp (net_pack_fun Sprod) K leK xprod.

Apply HconvProd to the current goal.

Let J0 be given.

Assume Hexle0: ∃le0 net0 : set, Sprod = net_pack J0 le0 net0 ∧ net_converges_on P Tp net0 J0 le0 xprod.

Apply Hexle0 to the current goal.

Let le0 be given.

Assume Hexnet0: ∃net0 : set, Sprod = net_pack J0 le0 net0 ∧ net_converges_on P Tp net0 J0 le0 xprod.

Apply Hexnet0 to the current goal.

Let net0 be given.

Assume Hpair0: Sprod = net_pack J0 le0 net0 ∧ net_converges_on P Tp net0 J0 le0 xprod.

We prove the intermediate claim HSprodEq0: Sprod = net_pack J0 le0 net0.

An exact proof term for the current goal is (andEL (Sprod = net_pack J0 le0 net0) (net_converges_on P Tp net0 J0 le0 xprod) Hpair0).

We prove the intermediate claim Hconv0: net_converges_on P Tp net0 J0 le0 xprod.

An exact proof term for the current goal is (andER (Sprod = net_pack J0 le0 net0) (net_converges_on P Tp net0 J0 le0 xprod) Hpair0).

We prove the intermediate claim HK0: K = J0.

We prove the intermediate claim HKdef: K = net_pack_index Sprod.

Use reflexivity.

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

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

rewrite the current goal using (net_pack_index_eq J0 le0 net0) (from left to right).

Use reflexivity.

We prove the intermediate claim Hle0: leK = le0.

We prove the intermediate claim Hledef: leK = net_pack_le Sprod.

Use reflexivity.

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

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

rewrite the current goal using (net_pack_le_eq J0 le0 net0) (from left to right).

Use reflexivity.

We prove the intermediate claim Hnet0: net_pack_fun Sprod = net0.

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

rewrite the current goal using (net_pack_fun_eq J0 le0 net0) (from left to right).

Use reflexivity.

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

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

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

An exact proof term for the current goal is Hconv0.

We prove the intermediate claim HcoordConv: net_converges_on Ka (subspace_topology Y Ty Ka) (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) K leK (apply_fun xprod a).

rewrite the current goal using (Ascoli_XiKa_set X Y Ty F a HaX) (from right to left) at position 1.

rewrite the current goal using (Ascoli_XiKa_topology X Y Ty F a HaX) (from right to left) at position 1.

An exact proof term for the current goal is (net_converges_on_product_topology_full_implies_coord_converges X XiKa (net_pack_fun Sprod) K leK xprod a HcompTop HaX HconvProdOn).

We prove the intermediate claim HKUopen: (U ∩ Ka) ∈ subspace_topology Y Ty Ka.

An exact proof term for the current goal is (subspace_topologyI Y Ty Ka U HUty).

We prove the intermediate claim HlimIn: apply_fun xprod a ∈ U ∩ Ka.

Apply binintersectI to the current goal.

An exact proof term for the current goal is HappU.

We prove the intermediate claim Hxprop2: (total_function_on xprod X (space_family_union X XiKa) ∧ functional_graph xprod) ∧ ∀i : set, i ∈ X → apply_fun xprod i ∈ space_family_set XiKa i.

We prove the intermediate claim Hcoords: ∀i : set, i ∈ X → apply_fun xprod i ∈ space_family_set XiKa i.

An exact proof term for the current goal is (andER (total_function_on xprod X (space_family_union X XiKa) ∧ functional_graph xprod) (∀i : set, i ∈ X → apply_fun xprod i ∈ space_family_set XiKa i) Hxprop2).

We prove the intermediate claim HxpaXi: apply_fun xprod a ∈ space_family_set XiKa a.

An exact proof term for the current goal is (Hcoords a HaX).

rewrite the current goal using (Ascoli_XiKa_set X Y Ty F a HaX) (from right to left) at position 1.

An exact proof term for the current goal is HxpaXi.

Apply HcoordConv to the current goal.

Assume Hcore Htail.

Apply (Htail (U ∩ Ka) HKUopen HlimIn) to the current goal.

Let k0 be given.

Assume Hk0pair: k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) k ∈ U ∩ Ka.

We use k0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) k ∈ U ∩ Ka) Hk0pair).

Let k be given.

Assume HkK: k ∈ K.

Assume Hk0k: (k0,k) ∈ leK.

We prove the intermediate claim HcoordIn: apply_fun (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) k ∈ U ∩ Ka.

An exact proof term for the current goal is (andER (k0 ∈ K) (∀k1 : set, k1 ∈ K → (k0,k1) ∈ leK → apply_fun (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) k1 ∈ U ∩ Ka) Hk0pair k HkK Hk0k).

We prove the intermediate claim HcoordInU: apply_fun (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) k ∈ U.

An exact proof term for the current goal is (binintersectE1 U Ka (apply_fun (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) k) HcoordIn).

We will prove apply_fun subNet k ∈ s.

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

Apply (SepI Dom (λf0 : set ⇒ apply_fun f0 a ∈ U) (apply_fun subNet k)) to the current goal.

An exact proof term for the current goal is (HHcandSubDom (apply_fun subNet k) (total_function_on_apply_fun_in_Y subNet K Hcand k Htotsub HkK)).

We prove the intermediate claim HvalEq: apply_fun (compose_fun K (net_pack_fun Sprod) (product_eval_map X XiKa a)) k = apply_fun (apply_fun subNet k) a.

Set fS to be the term net_pack_fun Sprod.

Set ev to be the term product_eval_map X XiKa a.

We prove the intermediate claim HfunComp: functional_graph (compose_fun K fS ev).

An exact proof term for the current goal is (functional_graph_compose_fun K fS ev).

We prove the intermediate claim HpairComp: (k,apply_fun ev (apply_fun fS k)) ∈ compose_fun K fS ev.

An exact proof term for the current goal is (ReplI K (λk0 : set ⇒ (k0,apply_fun ev (apply_fun fS k0))) k HkK).

We prove the intermediate claim HappComp: apply_fun (compose_fun K fS ev) k = apply_fun ev (apply_fun fS k).

An exact proof term for the current goal is (functional_graph_apply_fun_eq (compose_fun K fS ev) k (apply_fun ev (apply_fun fS k)) HfunComp HpairComp).

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

We prove the intermediate claim Htotsprod: total_function_on fS K P.

An exact proof term for the current goal is (subnet_of_witness_totsub (net_pack_fun Nprod) fS (net_pack_index Nprod) (net_pack_le Nprod) K leK P phi Hphi).

We prove the intermediate claim HSkP: apply_fun fS k ∈ P.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y fS K P k Htotsprod HkK).

We prove the intermediate claim HevEval: apply_fun ev (apply_fun fS k) = apply_fun (apply_fun fS k) a.

An exact proof term for the current goal is (apply_fun_graph P (λf0 : set ⇒ apply_fun f0 a) (apply_fun fS k) HSkP).

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

We prove the intermediate claim HvalsProd: ∀kk : set, kk ∈ K → apply_fun fS kk = apply_fun (net_pack_fun Nprod) (apply_fun phi kk).

An exact proof term for the current goal is (subnet_of_witness_vals (net_pack_fun Nprod) fS (net_pack_index Nprod) (net_pack_le Nprod) K leK P phi Hphi).

We prove the intermediate claim HSkEq0: apply_fun fS k = apply_fun (net_pack_fun Nprod) (apply_fun phi k).

An exact proof term for the current goal is (HvalsProd k HkK).

We prove the intermediate claim HNprodDef0: Nprod = net_pack J le netP.

Use reflexivity.

We prove the intermediate claim HnetfunNprod: net_pack_fun Nprod = netP.

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

An exact proof term for the current goal is (net_pack_fun_eq J le netP).

We prove the intermediate claim HNprodApp: apply_fun (net_pack_fun Nprod) (apply_fun phi k) = apply_fun netP (apply_fun phi k).

An exact proof term for the current goal is (apply_fun_congr (net_pack_fun Nprod) netP (apply_fun phi k) HnetfunNprod).

We prove the intermediate claim HSkEq: apply_fun fS k = apply_fun netP (apply_fun phi k).

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

An exact proof term for the current goal is HNprodApp.

We prove the intermediate claim HLHS0: apply_fun (apply_fun fS k) a = apply_fun (apply_fun netP (apply_fun phi k)) a.

An exact proof term for the current goal is (apply_fun_congr (apply_fun fS k) (apply_fun netP (apply_fun phi k)) a HSkEq).

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

We prove the intermediate claim HphikJ: apply_fun phi k ∈ J.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K J k Htotphi HkK).

We prove the intermediate claim HnetPDef0: netP = graph J (λj1 : set ⇒ graph X (λa0 : set ⇒ apply_fun (apply_fun net j1) a0)).

Use reflexivity.

We prove the intermediate claim HnetPjEq: apply_fun netP (apply_fun phi k) = apply_fun (graph J (λj1 : set ⇒ graph X (λa0 : set ⇒ apply_fun (apply_fun net j1) a0))) (apply_fun phi k).

An exact proof term for the current goal is (apply_fun_congr netP (graph J (λj1 : set ⇒ graph X (λa0 : set ⇒ apply_fun (apply_fun net j1) a0))) (apply_fun phi k) HnetPDef0).

We prove the intermediate claim HnetPjEq2: apply_fun (apply_fun netP (apply_fun phi k)) a = apply_fun (apply_fun (graph J (λj1 : set ⇒ graph X (λa0 : set ⇒ apply_fun (apply_fun net j1) a0))) (apply_fun phi k)) a.

An exact proof term for the current goal is (apply_fun_congr (apply_fun netP (apply_fun phi k)) (apply_fun (graph J (λj1 : set ⇒ graph X (λa0 : set ⇒ apply_fun (apply_fun net j1) a0))) (apply_fun phi k)) a HnetPjEq).

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

rewrite the current goal using (apply_fun_apply_fun_graph J (λj1 : set ⇒ graph X (λa0 : set ⇒ apply_fun (apply_fun net j1) a0)) (apply_fun phi k) a HphikJ) (from left to right).

rewrite the current goal using (apply_fun_graph X (λa0 : set ⇒ apply_fun (apply_fun net (apply_fun phi k)) a0) a HaX) (from left to right).

We prove the intermediate claim HsubNetDef0: subNet = compose_fun K phi net.

Use reflexivity.

We prove the intermediate claim HfunSub: functional_graph (compose_fun K phi net).

An exact proof term for the current goal is (functional_graph_compose_fun K phi net).

We prove the intermediate claim HpairSub: (k,apply_fun net (apply_fun phi k)) ∈ compose_fun K phi net.

An exact proof term for the current goal is (ReplI K (λk0 : set ⇒ (k0,apply_fun net (apply_fun phi k0))) k HkK).

We prove the intermediate claim HappSub: apply_fun subNet k = apply_fun net (apply_fun phi k).

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

An exact proof term for the current goal is (functional_graph_apply_fun_eq (compose_fun K phi net) k (apply_fun net (apply_fun phi k)) HfunSub HpairSub).

We prove the intermediate claim HRHS: apply_fun (apply_fun subNet k) a = apply_fun (apply_fun net (apply_fun phi k)) a.

An exact proof term for the current goal is (apply_fun_congr (apply_fun subNet k) (apply_fun net (apply_fun phi k)) a HappSub).

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

Use reflexivity.

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

An exact proof term for the current goal is HcoordInU.

Assume HsDom: s ∈ {Dom}.

We prove the intermediate claim Hseq: s = Dom.

An exact proof term for the current goal is (SingE Dom s HsDom).

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

We prove the intermediate claim HKne: K ≠ Empty.

An exact proof term for the current goal is (directed_set_nonempty K leK HdirK).

We prove the intermediate claim Hexk0: ∃k0 : set, k0 ∈ K.

An exact proof term for the current goal is (nonempty_has_element K HKne).

Apply Hexk0 to the current goal.

Let k0 be given.

Assume Hk0K: k0 ∈ K.

We use k0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hk0K.

Let k be given.

Assume HkK: k ∈ K.

Assume Hk0k: (k0,k) ∈ leK.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K Dom k HtotsubDom HkK).

An exact proof term for the current goal is HsS.

We prove the intermediate claim HconvDom: net_converges_on Dom Tpt subNet K leK xprod.

An exact proof term for the current goal is (net_converges_on_generated_topology_from_subbasis_of_subeventual Dom Spt subNet K leK xprod HSpt HdirK HtotsubDom HgraphSub HdomSub HxprodInDom HevSpt).

We prove the intermediate claim Hmem: xprod ∈ Hcand.

Apply (xm (xprod ∈ Hcand)) to the current goal.

Assume Hin: xprod ∈ Hcand.

An exact proof term for the current goal is Hin.

Assume Hnot: xprod ∉ Hcand.

We will prove xprod ∈ Hcand.

Apply FalseE to the current goal.

We will prove False.

We prove the intermediate claim HxU0: xprod ∈ U0.

Apply xm (xprod ∈ U0) to the current goal.

Assume HxU: xprod ∈ U0.

An exact proof term for the current goal is HxU.

Assume HxnotU: xprod ∉ U0.

We will prove xprod ∈ U0.

Apply FalseE to the current goal.

We will prove False.

We prove the intermediate claim HxInDiff: xprod ∈ Dom ∖ U0.

An exact proof term for the current goal is (setminusI Dom U0 xprod HxprodInDom HxnotU).

We prove the intermediate claim HxInHcand: xprod ∈ Hcand.

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

An exact proof term for the current goal is HxInDiff.

An exact proof term for the current goal is (Hnot HxInHcand).

Apply HconvDom to the current goal.

Assume Hcore Htail.

Apply Hcore to the current goal.

Assume Hcore6 HxX.

Apply Hcore6 to the current goal.

Assume Hcore5 Hdom2.

Apply Hcore5 to the current goal.

Assume Hcore4 Hgraph2.

Apply Hcore4 to the current goal.

Assume Hcore3 Htot2.

Apply Hcore3 to the current goal.

Assume HTtop2 Hdir2.

Apply (Htail U0 HU0Tpt HxU0) to the current goal.

Let k0 be given.

Assume Hk0pair: k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ U0.

We prove the intermediate claim Hk0K: k0 ∈ K.

An exact proof term for the current goal is (andEL (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ U0) Hk0pair).

We prove the intermediate claim Hk0k0: (k0,k0) ∈ leK.

An exact proof term for the current goal is (directed_set_refl K leK HdirK k0 Hk0K).

We prove the intermediate claim Hsubk0U0: apply_fun subNet k0 ∈ U0.

An exact proof term for the current goal is (andER (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ U0) Hk0pair k0 Hk0K Hk0k0).

We prove the intermediate claim Hsubk0Hcand: apply_fun subNet k0 ∈ Hcand.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K Hcand k0 Htotsub Hk0K).

We prove the intermediate claim Hsubk0NotU0: apply_fun subNet k0 ∉ U0.

We prove the intermediate claim Hsubk0InDiff: apply_fun subNet k0 ∈ Dom ∖ U0.

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

An exact proof term for the current goal is Hsubk0Hcand.

An exact proof term for the current goal is (setminusE2 Dom U0 (apply_fun subNet k0) Hsubk0InDiff).

An exact proof term for the current goal is (Hsubk0NotU0 Hsubk0U0).

Apply andI to the current goal.

An exact proof term for the current goal is Hmem.

An exact proof term for the current goal is HconvDom.

We prove the intermediate claim HxprodInHcandMem: xprod ∈ Hcand.

An exact proof term for the current goal is (andEL (xprod ∈ Hcand) (net_converges_on Dom Tpt subNet K leK xprod) HxprodInHcand).

We prove the intermediate claim HconvDom: net_converges_on Dom Tpt subNet K leK xprod.

An exact proof term for the current goal is (andER (xprod ∈ Hcand) (net_converges_on Dom Tpt subNet K leK xprod) HxprodInHcand).

We prove the intermediate claim HxprodCXY: xprod ∈ CXY.

An exact proof term for the current goal is (HHcandSubCXY xprod HxprodInHcandMem).

We prove the intermediate claim HtotsubCXY: total_function_on subNet K CXY.

An exact proof term for the current goal is (total_function_on_codomain subNet K Hcand CXY Htotsub HHcandSubCXY).

We prove the intermediate claim HconvAmbient: net_converges_on CXY Tcc subNet K leK xprod.

Set Scc to be the term (compact_convergence_subbasis_metric X Tx Y dY) ∪ {CXY}.

We prove the intermediate claim HScc: subbasis_on CXY Scc.

An exact proof term for the current goal is (compact_convergence_metric_subbasis_on X Tx Y dY HTx HdY).

We prove the intermediate claim HevS: ∀s : set, s ∈ Scc → xprod ∈ s → ∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ s.

Let s be given.

Assume HsScc: s ∈ Scc.

Assume Hxps: xprod ∈ s.

Apply (binunionE' (compact_convergence_subbasis_metric X Tx Y dY) {CXY} s (∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ s)) to the current goal.

Assume HsMetric: s ∈ compact_convergence_subbasis_metric X Tx Y dY.

We prove the intermediate claim HexCfe: ∃C0 f0 eps0 : set, compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X ∧ f0 ∈ CXY ∧ eps0 ∈ R ∧ Rlt 0 eps0 ∧ s = {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}.

An exact proof term for the current goal is (SepE2 (𝒫 CXY) (λS0 : set ⇒ ∃C0 f0 eps0 : set, compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X ∧ f0 ∈ CXY ∧ eps0 ∈ R ∧ Rlt 0 eps0 ∧ S0 = {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}) s HsMetric).

Apply HexCfe to the current goal.

Let C0 be given.

Assume Hexfe: ∃f0 eps0 : set, compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X ∧ f0 ∈ CXY ∧ eps0 ∈ R ∧ Rlt 0 eps0 ∧ s = {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}.

Apply Hexfe to the current goal.

Let f0 be given.

Assume Hexeps0: ∃eps0 : set, compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X ∧ f0 ∈ CXY ∧ eps0 ∈ R ∧ Rlt 0 eps0 ∧ s = {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}.

Apply Hexeps0 to the current goal.

Let eps0 be given.

Assume Hpack: compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X ∧ f0 ∈ CXY ∧ eps0 ∈ R ∧ Rlt 0 eps0 ∧ s = {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}.

Apply (and6E (compact_space C0 (subspace_topology X Tx C0)) (C0 ⊆ X) (f0 ∈ CXY) (eps0 ∈ R) (Rlt 0 eps0) (s = {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}) Hpack) to the current goal.

Assume Hcompact HC0subX Hf0CXY Heps0R Heps0Pos HsDef.

We prove the intermediate claim HxprodInS0: xprod ∈ {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}.

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

An exact proof term for the current goal is Hxps.

We prove the intermediate claim HxprodClose: ∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun xprod x,apply_fun f0 x)) eps0.

Let x be given.

Assume HxC0: x ∈ C0.

An exact proof term for the current goal is (SepE2 CXY (λg0 : set ⇒ ∀x0 : set, x0 ∈ C0 → Rlt (apply_fun dY (apply_fun g0 x0,apply_fun f0 x0)) eps0) xprod HxprodInS0 x HxC0).

Set Ty to be the term metric_topology Y dY.

We prove the intermediate claim Hf0cont: continuous_map X Tx Y Ty f0.

An exact proof term for the current goal is (SepE2 (function_space X Y) (λf : set ⇒ continuous_map X Tx Y Ty f) f0 Hf0CXY).

We prove the intermediate claim Hxprodcont: continuous_map X Tx Y Ty xprod.

An exact proof term for the current goal is (SepE2 (function_space X Y) (λf : set ⇒ continuous_map X Tx Y Ty f) xprod HxprodCXY).

We prove the intermediate claim Hf0FS: f0 ∈ function_space X Y.

An exact proof term for the current goal is (SepE1 (function_space X Y) (λf : set ⇒ continuous_map X Tx Y Ty f) f0 Hf0CXY).

We prove the intermediate claim HxprodFS: xprod ∈ function_space X Y.

An exact proof term for the current goal is (SepE1 (function_space X Y) (λf : set ⇒ continuous_map X Tx Y Ty f) xprod HxprodCXY).

We prove the intermediate claim Hf0fun: function_on f0 X Y.

An exact proof term for the current goal is (function_on_of_function_space f0 X Y Hf0FS).

We prove the intermediate claim Hxprodfun: function_on xprod X Y.

An exact proof term for the current goal is (function_on_of_function_space xprod X Y HxprodFS).

We prove the intermediate claim HdYfun: function_on dY (setprod Y Y) R.

An exact proof term for the current goal is (metric_on_function_on Y dY HdY).

Set dist to be the term λx : set ⇒ apply_fun dY (apply_fun xprod x,apply_fun f0 x).

We prove the intermediate claim HdistR: ∀x : set, x ∈ C0 → dist x ∈ R.

Let x be given.

Assume HxC0: x ∈ C0.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HC0subX x HxC0).

We prove the intermediate claim HgxY: apply_fun xprod x ∈ Y.

An exact proof term for the current goal is (Hxprodfun x HxX).

We prove the intermediate claim HfxY: apply_fun f0 x ∈ Y.

An exact proof term for the current goal is (Hf0fun x HxX).

We prove the intermediate claim HpIn: (apply_fun xprod x,apply_fun f0 x) ∈ setprod Y Y.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun xprod x) (apply_fun f0 x) HgxY HfxY).

We prove the intermediate claim HdistDef: dist x = apply_fun dY (apply_fun xprod x,apply_fun f0 x).

Use reflexivity.

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

An exact proof term for the current goal is (HdYfun (apply_fun xprod x,apply_fun f0 x) HpIn).

We prove the intermediate claim HdistClose: ∀x : set, x ∈ C0 → Rlt (dist x) eps0.

Let x be given.

Assume HxC0: x ∈ C0.

We prove the intermediate claim HdistDef: dist x = apply_fun dY (apply_fun xprod x,apply_fun f0 x).

Use reflexivity.

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

An exact proof term for the current goal is (HxprodClose x HxC0).

We prove the intermediate claim HexDeltaM: ∃deltaM : set, deltaM ∈ R ∧ Rlt 0 deltaM ∧ ∀x : set, x ∈ C0 → Rlt (add_SNo (dist x) deltaM) eps0.

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

Assume HC0Empty: C0 = Empty.

We use 1 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is real_1.

An exact proof term for the current goal is (RltI 0 1 real_0 real_1 SNoLt_0_1).

Let x be given.

Assume HxC0: x ∈ C0.

We will prove Rlt (add_SNo (dist x) 1) eps0.

We prove the intermediate claim Hx0: x ∈ Empty.

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

An exact proof term for the current goal is HxC0.

An exact proof term for the current goal is (EmptyE x Hx0 (Rlt (add_SNo (dist x) 1) eps0)).

Assume HC0ne: C0 ≠ Empty.

Set dgap to be the term λx : set ⇒ add_SNo eps0 (minus_SNo (dist x)).

Set pickN to be the term λx : set ⇒ Eps_i (λN : set ⇒ N ∈ ω ∧ eps_ N < dgap x).

We prove the intermediate claim HpickN: ∀x : set, x ∈ C0 → pickN x ∈ ω ∧ eps_ (pickN x) < dgap x.

Let x be given.

Assume HxC0: x ∈ C0.

We prove the intermediate claim HdistxR: dist x ∈ R.

An exact proof term for the current goal is (HdistR x HxC0).

We prove the intermediate claim HdistxLt: Rlt (dist x) eps0.

An exact proof term for the current goal is (HdistClose x HxC0).

We prove the intermediate claim HdgapPos: Rlt 0 (dgap x).

An exact proof term for the current goal is (Rlt_0_diff_of_lt (dist x) eps0 HdistxLt).

We prove the intermediate claim HdgapR: dgap x ∈ R.

An exact proof term for the current goal is (RltE_right 0 (dgap x) HdgapPos).

We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < dgap x.

An exact proof term for the current goal is (exists_eps_lt_pos_Euclid (dgap x) HdgapR HdgapPos).

Apply HexN to the current goal.

Let N be given.

Assume HNpair.

We prove the intermediate claim HNomega: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < dgap x) HNpair).

We prove the intermediate claim HNlt: eps_ N < dgap x.

An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < dgap x) HNpair).

An exact proof term for the current goal is (Eps_i_ax (λM : set ⇒ M ∈ ω ∧ eps_ M < dgap x) N (andI (N ∈ ω) (eps_ N < dgap x) HNomega HNlt)).

Set rsmall to be the term λx : set ⇒ eps_ (ordsucc (ordsucc (pickN x))).

Set delta_of to be the term λx : set ⇒ eps_ (ordsucc (pickN x)).

Set Uof to be the term λx : set ⇒ (preimage_of X xprod (open_ball Y dY (apply_fun xprod x) (rsmall x))) ∩ (preimage_of X f0 (open_ball Y dY (apply_fun f0 x) (rsmall x))).

Set UFam to be the term {Uof x|x ∈ C0}.

We prove the intermediate claim HUFamSubTx: UFam ⊆ Tx.

Let U be given.

Assume HU: U ∈ UFam.

Apply (ReplE_impred C0 (λx0 : set ⇒ Uof x0) U HU) to the current goal.

Let x be given.

Assume HxC0: x ∈ C0.

Assume HUeq: U = Uof x.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HC0subX x HxC0).

We prove the intermediate claim HgxY: apply_fun xprod x ∈ Y.

An exact proof term for the current goal is (Hxprodfun x HxX).

We prove the intermediate claim HfxY: apply_fun f0 x ∈ Y.

An exact proof term for the current goal is (Hf0fun x HxX).

We prove the intermediate claim HNpack: pickN x ∈ ω ∧ eps_ (pickN x) < dgap x.

An exact proof term for the current goal is (HpickN x HxC0).

We prove the intermediate claim Hrpos: Rlt 0 (rsmall x).

We prove the intermediate claim Hn2omega: ordsucc (ordsucc (pickN x)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (ordsucc (pickN x)) (omega_ordsucc (pickN x) (andEL (pickN x ∈ ω) (eps_ (pickN x) < dgap x) HNpack))).

We prove the intermediate claim Hrlt0: 0 < eps_ (ordsucc (ordsucc (pickN x))).

An exact proof term for the current goal is (SNo_eps_pos (ordsucc (ordsucc (pickN x))) Hn2omega).

We prove the intermediate claim HrR: rsmall x ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (rsmall x) (SNo_eps_SNoS_omega (ordsucc (ordsucc (pickN x))) Hn2omega)).

An exact proof term for the current goal is (RltI 0 (rsmall x) real_0 HrR Hrlt0).

We prove the intermediate claim HBxTy: open_ball Y dY (apply_fun xprod x) (rsmall x) ∈ Ty.

An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun xprod x) (rsmall x) HdY HgxY Hrpos).

We prove the intermediate claim HBfTy: open_ball Y dY (apply_fun f0 x) (rsmall x) ∈ Ty.

An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun f0 x) (rsmall x) HdY HfxY Hrpos).

We prove the intermediate claim HpreG: preimage_of X xprod (open_ball Y dY (apply_fun xprod x) (rsmall x)) ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty xprod Hxprodcont (open_ball Y dY (apply_fun xprod x) (rsmall x)) HBxTy).

We prove the intermediate claim HpreF: preimage_of X f0 (open_ball Y dY (apply_fun f0 x) (rsmall x)) ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f0 Hf0cont (open_ball Y dY (apply_fun f0 x) (rsmall x)) HBfTy).

We prove the intermediate claim HUofTx: Uof x ∈ Tx.

An exact proof term for the current goal is (topology_binintersect_closed X Tx (preimage_of X xprod (open_ball Y dY (apply_fun xprod x) (rsmall x))) (preimage_of X f0 (open_ball Y dY (apply_fun f0 x) (rsmall x))) HTx HpreG HpreF).

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

An exact proof term for the current goal is HUofTx.

We prove the intermediate claim HC0cov: C0 ⊆ ⋃ UFam.

Let x be given.

Assume HxC0: x ∈ C0.

We will prove x ∈ ⋃ UFam.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HC0subX x HxC0).

We prove the intermediate claim HgxY: apply_fun xprod x ∈ Y.

An exact proof term for the current goal is (Hxprodfun x HxX).

We prove the intermediate claim HfxY: apply_fun f0 x ∈ Y.

An exact proof term for the current goal is (Hf0fun x HxX).

We prove the intermediate claim HNpack: pickN x ∈ ω ∧ eps_ (pickN x) < dgap x.

An exact proof term for the current goal is (HpickN x HxC0).

We prove the intermediate claim Hrpos: Rlt 0 (rsmall x).

We prove the intermediate claim Hn2omega: ordsucc (ordsucc (pickN x)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (ordsucc (pickN x)) (omega_ordsucc (pickN x) (andEL (pickN x ∈ ω) (eps_ (pickN x) < dgap x) HNpack))).

We prove the intermediate claim Hrlt0: 0 < eps_ (ordsucc (ordsucc (pickN x))).

An exact proof term for the current goal is (SNo_eps_pos (ordsucc (ordsucc (pickN x))) Hn2omega).

We prove the intermediate claim HrR: rsmall x ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (rsmall x) (SNo_eps_SNoS_omega (ordsucc (ordsucc (pickN x))) Hn2omega)).

An exact proof term for the current goal is (RltI 0 (rsmall x) real_0 HrR Hrlt0).

We prove the intermediate claim HxInG: x ∈ preimage_of X xprod (open_ball Y dY (apply_fun xprod x) (rsmall x)).

We prove the intermediate claim Hcenter: apply_fun xprod x ∈ open_ball Y dY (apply_fun xprod x) (rsmall x).

An exact proof term for the current goal is (center_in_open_ball Y dY (apply_fun xprod x) (rsmall x) HdY HgxY Hrpos).

An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun xprod u ∈ open_ball Y dY (apply_fun xprod x) (rsmall x)) x HxX Hcenter).

We prove the intermediate claim HxInF: x ∈ preimage_of X f0 (open_ball Y dY (apply_fun f0 x) (rsmall x)).

We prove the intermediate claim Hcenter: apply_fun f0 x ∈ open_ball Y dY (apply_fun f0 x) (rsmall x).

An exact proof term for the current goal is (center_in_open_ball Y dY (apply_fun f0 x) (rsmall x) HdY HfxY Hrpos).

An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f0 u ∈ open_ball Y dY (apply_fun f0 x) (rsmall x)) x HxX Hcenter).

We prove the intermediate claim HxInU: x ∈ Uof x.

An exact proof term for the current goal is (binintersectI (preimage_of X xprod (open_ball Y dY (apply_fun xprod x) (rsmall x))) (preimage_of X f0 (open_ball Y dY (apply_fun f0 x) (rsmall x))) x HxInG HxInF).

We prove the intermediate claim HUin: Uof x ∈ UFam.

An exact proof term for the current goal is (ReplI C0 (λx0 : set ⇒ Uof x0) x HxC0).

An exact proof term for the current goal is (UnionI UFam x (Uof x) HxInU HUin).

We prove the intermediate claim Hcover_prop: ∀Fam : set, (Fam ⊆ Tx ∧ C0 ⊆ ⋃ Fam) → has_finite_subcover C0 Tx Fam.

An exact proof term for the current goal is (iffEL (compact_space C0 (subspace_topology X Tx C0)) (∀Fam : set, (Fam ⊆ Tx ∧ C0 ⊆ ⋃ Fam) → has_finite_subcover C0 Tx Fam) (compact_subspace_via_ambient_covers X Tx C0 HTx HC0subX) Hcompact).

We prove the intermediate claim Hfin: has_finite_subcover C0 Tx UFam.

An exact proof term for the current goal is (Hcover_prop UFam (andI (UFam ⊆ Tx) (C0 ⊆ ⋃ UFam) HUFamSubTx HC0cov)).

Apply Hfin to the current goal.

Let G be given.

Assume HGtriple: G ⊆ UFam ∧ finite G ∧ C0 ⊆ ⋃ G.

We prove the intermediate claim HGsub: G ⊆ UFam.

An exact proof term for the current goal is (andEL (G ⊆ UFam) (finite G) (andEL (G ⊆ UFam ∧ finite G) (C0 ⊆ ⋃ G) HGtriple)).

We prove the intermediate claim HGfin: finite G.

An exact proof term for the current goal is (andER (G ⊆ UFam) (finite G) (andEL (G ⊆ UFam ∧ finite G) (C0 ⊆ ⋃ G) HGtriple)).

We prove the intermediate claim HC0covG: C0 ⊆ ⋃ G.

An exact proof term for the current goal is (andER (G ⊆ UFam ∧ finite G) (C0 ⊆ ⋃ G) HGtriple).

We prove the intermediate claim HGne: G ≠ Empty.

Assume HG0: G = Empty.

We prove the intermediate claim HC0eq: C0 = Empty.

We prove the intermediate claim HC0covG0: C0 ⊆ ⋃ Empty.

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

An exact proof term for the current goal is HC0covG.

We prove the intermediate claim HUn0: ⋃ Empty = Empty.

An exact proof term for the current goal is Union_Empty_eq.

Apply set_ext to the current goal.

Let x be given.

Assume HxC0: x ∈ C0.

We prove the intermediate claim HxU: x ∈ ⋃ Empty.

An exact proof term for the current goal is (HC0covG0 x HxC0).

We prove the intermediate claim Hx0: x ∈ Empty.

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

An exact proof term for the current goal is HxU.

An exact proof term for the current goal is Hx0.

Let x be given.

Assume Hx0: x ∈ Empty.

An exact proof term for the current goal is (EmptyE x Hx0 (x ∈ C0)).

An exact proof term for the current goal is (HC0ne HC0eq).

Set xOf to be the term λU : set ⇒ Eps_i (λx : set ⇒ x ∈ C0 ∧ U = Uof x).

We prove the intermediate claim HxOf: ∀U : set, U ∈ G → xOf U ∈ C0 ∧ U = Uof (xOf U).

Let U be given.

Assume HUG: U ∈ G.

We prove the intermediate claim HUFam: U ∈ UFam.

An exact proof term for the current goal is (HGsub U HUG).

Apply (ReplE_impred C0 (λx0 : set ⇒ Uof x0) U HUFam) to the current goal.

Let x be given.

Assume HxC0: x ∈ C0.

Assume HUeq: U = Uof x.

An exact proof term for the current goal is (Eps_i_ax (λz : set ⇒ z ∈ C0 ∧ U = Uof z) x (andI (x ∈ C0) (U = Uof x) HxC0 HUeq)).

Set V to be the term Repl G (λU0 : set ⇒ delta_of (xOf U0)).

We prove the intermediate claim HVfin: finite V.

An exact proof term for the current goal is (Repl_finite (λU0 : set ⇒ delta_of (xOf U0)) G HGfin).

We prove the intermediate claim HVne0: V ≠ 0.

Assume HV0: V = 0.

We prove the intermediate claim HexU: ∃U : set, U ∈ G.

An exact proof term for the current goal is (nonempty_has_element G HGne).

Apply HexU to the current goal.

Let U be given.

Assume HUG: U ∈ G.

We prove the intermediate claim HvU: delta_of (xOf U) ∈ V.

An exact proof term for the current goal is (ReplI G (λU0 : set ⇒ delta_of (xOf U0)) U HUG).

We prove the intermediate claim HVsub0: V ⊆ 0.

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

An exact proof term for the current goal is (Subq_ref 0).

We prove the intermediate claim Hv0: delta_of (xOf U) ∈ 0.

An exact proof term for the current goal is (HVsub0 (delta_of (xOf U)) HvU).

An exact proof term for the current goal is (EmptyE (delta_of (xOf U)) Hv0).

We prove the intermediate claim HallS: ∀y : set, y ∈ V → SNo y.

Let y be given.

Assume HyV: y ∈ V.

Apply (ReplE_impred G (λU0 : set ⇒ delta_of (xOf U0)) y HyV) to the current goal.

Let U be given.

Assume HUG: U ∈ G.

Assume Hyeq: y = delta_of (xOf U).

We prove the intermediate claim HxPack: xOf U ∈ C0 ∧ U = Uof (xOf U).

An exact proof term for the current goal is (HxOf U HUG).

We prove the intermediate claim HxC0: xOf U ∈ C0.

An exact proof term for the current goal is (andEL (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim HNpack: pickN (xOf U) ∈ ω ∧ eps_ (pickN (xOf U)) < dgap (xOf U).

An exact proof term for the current goal is (HpickN (xOf U) HxC0).

We prove the intermediate claim Hn1omega: ordsucc (pickN (xOf U)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack)).

We prove the intermediate claim HyR: y ∈ R.

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

An exact proof term for the current goal is (SNoS_omega_real (delta_of (xOf U)) (SNo_eps_SNoS_omega (ordsucc (pickN (xOf U))) Hn1omega)).

An exact proof term for the current goal is (real_SNo y HyR).

We prove the intermediate claim Hexm: ∃m : set, SNo_min_of V m.

An exact proof term for the current goal is (finite_min_exists V HallS HVfin HVne0).

Apply Hexm to the current goal.

Let deltaM be given.

Assume Hmin: SNo_min_of V deltaM.

We use deltaM to witness the existential quantifier.

We prove the intermediate claim HdeltaMInV: deltaM ∈ V.

An exact proof term for the current goal is (andEL (deltaM ∈ V) (SNo deltaM) (andEL (deltaM ∈ V ∧ SNo deltaM) (∀y ∈ V, SNo y → deltaM ≤ y) Hmin)).

We prove the intermediate claim HdeltaMS: SNo deltaM.

An exact proof term for the current goal is (andER (deltaM ∈ V) (SNo deltaM) (andEL (deltaM ∈ V ∧ SNo deltaM) (∀y ∈ V, SNo y → deltaM ≤ y) Hmin)).

We prove the intermediate claim HdeltaMLe: ∀y : set, y ∈ V → SNo y → deltaM ≤ y.

An exact proof term for the current goal is (andER (deltaM ∈ V ∧ SNo deltaM) (∀y ∈ V, SNo y → deltaM ≤ y) Hmin).

We prove the intermediate claim HdeltaMR: deltaM ∈ R.

Apply (ReplE_impred G (λU0 : set ⇒ delta_of (xOf U0)) deltaM HdeltaMInV) to the current goal.

Let U be given.

Assume HUG: U ∈ G.

Assume Hdeq: deltaM = delta_of (xOf U).

We prove the intermediate claim HxPack: xOf U ∈ C0 ∧ U = Uof (xOf U).

An exact proof term for the current goal is (HxOf U HUG).

We prove the intermediate claim HxC0: xOf U ∈ C0.

An exact proof term for the current goal is (andEL (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim HNpack: pickN (xOf U) ∈ ω ∧ eps_ (pickN (xOf U)) < dgap (xOf U).

An exact proof term for the current goal is (HpickN (xOf U) HxC0).

We prove the intermediate claim Hn1omega: ordsucc (pickN (xOf U)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack)).

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

An exact proof term for the current goal is (SNoS_omega_real (delta_of (xOf U)) (SNo_eps_SNoS_omega (ordsucc (pickN (xOf U))) Hn1omega)).

We prove the intermediate claim HdeltaMpos: Rlt 0 deltaM.

Apply (ReplE_impred G (λU0 : set ⇒ delta_of (xOf U0)) deltaM HdeltaMInV) to the current goal.

Let U be given.

Assume HUG: U ∈ G.

Assume Hdeq: deltaM = delta_of (xOf U).

We prove the intermediate claim HxPack: xOf U ∈ C0 ∧ U = Uof (xOf U).

An exact proof term for the current goal is (HxOf U HUG).

We prove the intermediate claim HxC0: xOf U ∈ C0.

An exact proof term for the current goal is (andEL (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim HNpack: pickN (xOf U) ∈ ω ∧ eps_ (pickN (xOf U)) < dgap (xOf U).

An exact proof term for the current goal is (HpickN (xOf U) HxC0).

We prove the intermediate claim Hn1omega: ordsucc (pickN (xOf U)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack)).

We prove the intermediate claim HdR: delta_of (xOf U) ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (delta_of (xOf U)) (SNo_eps_SNoS_omega (ordsucc (pickN (xOf U))) Hn1omega)).

We prove the intermediate claim Hdlt0: 0 < eps_ (ordsucc (pickN (xOf U))).

An exact proof term for the current goal is (SNo_eps_pos (ordsucc (pickN (xOf U))) Hn1omega).

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

An exact proof term for the current goal is (RltI 0 (delta_of (xOf U)) real_0 HdR Hdlt0).

Apply andI to the current goal.

An exact proof term for the current goal is HdeltaMR.

An exact proof term for the current goal is HdeltaMpos.

Let x be given.

Assume HxC0: x ∈ C0.

We prove the intermediate claim HxUnion: x ∈ ⋃ G.

An exact proof term for the current goal is (HC0covG x HxC0).

Apply UnionE_impred G x HxUnion to the current goal.

Let U be given.

Assume HxU: x ∈ U.

Assume HUG: U ∈ G.

We prove the intermediate claim HxPack: xOf U ∈ C0 ∧ U = Uof (xOf U).

An exact proof term for the current goal is (HxOf U HUG).

We prove the intermediate claim Hx0C0: xOf U ∈ C0.

An exact proof term for the current goal is (andEL (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim HUeq: U = Uof (xOf U).

An exact proof term for the current goal is (andER (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim HxUof: x ∈ Uof (xOf U).

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

An exact proof term for the current goal is HxU.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HC0subX x HxC0).

We prove the intermediate claim Hx0X: xOf U ∈ X.

An exact proof term for the current goal is (HC0subX (xOf U) Hx0C0).

We prove the intermediate claim Hx0yY: apply_fun xprod (xOf U) ∈ Y.

An exact proof term for the current goal is (Hxprodfun (xOf U) Hx0X).

We prove the intermediate claim Hx0fY: apply_fun f0 (xOf U) ∈ Y.

An exact proof term for the current goal is (Hf0fun (xOf U) Hx0X).

We prove the intermediate claim HxgY: apply_fun xprod x ∈ Y.

An exact proof term for the current goal is (Hxprodfun x HxX).

We prove the intermediate claim HxfY: apply_fun f0 x ∈ Y.

An exact proof term for the current goal is (Hf0fun x HxX).

We prove the intermediate claim HNpack: pickN (xOf U) ∈ ω ∧ eps_ (pickN (xOf U)) < dgap (xOf U).

An exact proof term for the current goal is (HpickN (xOf U) Hx0C0).

We prove the intermediate claim Hrpos: Rlt 0 (rsmall (xOf U)).

We prove the intermediate claim Hn2omega: ordsucc (ordsucc (pickN (xOf U))) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (ordsucc (pickN (xOf U))) (omega_ordsucc (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack))).

We prove the intermediate claim Hrlt0: 0 < eps_ (ordsucc (ordsucc (pickN (xOf U)))).

An exact proof term for the current goal is (SNo_eps_pos (ordsucc (ordsucc (pickN (xOf U)))) Hn2omega).

We prove the intermediate claim HrR: rsmall (xOf U) ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (rsmall (xOf U)) (SNo_eps_SNoS_omega (ordsucc (ordsucc (pickN (xOf U)))) Hn2omega)).

An exact proof term for the current goal is (RltI 0 (rsmall (xOf U)) real_0 HrR Hrlt0).

We prove the intermediate claim HdeltaU_R: delta_of (xOf U) ∈ R.

We prove the intermediate claim Hn1omega: ordsucc (pickN (xOf U)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack)).

An exact proof term for the current goal is (SNoS_omega_real (delta_of (xOf U)) (SNo_eps_SNoS_omega (ordsucc (pickN (xOf U))) Hn1omega)).

We prove the intermediate claim HdeltaU_pos: Rlt 0 (delta_of (xOf U)).

We prove the intermediate claim Hn1omega: ordsucc (pickN (xOf U)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack)).

We prove the intermediate claim Hlt0: 0 < eps_ (ordsucc (pickN (xOf U))).

An exact proof term for the current goal is (SNo_eps_pos (ordsucc (pickN (xOf U))) Hn1omega).

An exact proof term for the current goal is (RltI 0 (delta_of (xOf U)) real_0 HdeltaU_R Hlt0).

We prove the intermediate claim HxPreG: x ∈ preimage_of X xprod (open_ball Y dY (apply_fun xprod (xOf U)) (rsmall (xOf U))).

An exact proof term for the current goal is (binintersectE1 (preimage_of X xprod (open_ball Y dY (apply_fun xprod (xOf U)) (rsmall (xOf U)))) (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U)) (rsmall (xOf U)))) x HxUof).

We prove the intermediate claim HxPreF: x ∈ preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U)) (rsmall (xOf U))).

An exact proof term for the current goal is (binintersectE2 (preimage_of X xprod (open_ball Y dY (apply_fun xprod (xOf U)) (rsmall (xOf U)))) (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U)) (rsmall (xOf U)))) x HxUof).

We prove the intermediate claim HxBallG: apply_fun xprod x ∈ open_ball Y dY (apply_fun xprod (xOf U)) (rsmall (xOf U)).

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun xprod u ∈ open_ball Y dY (apply_fun xprod (xOf U)) (rsmall (xOf U))) x HxPreG).

We prove the intermediate claim HxBallF: apply_fun f0 x ∈ open_ball Y dY (apply_fun f0 (xOf U)) (rsmall (xOf U)).

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f0 u ∈ open_ball Y dY (apply_fun f0 (xOf U)) (rsmall (xOf U))) x HxPreF).

We prove the intermediate claim Hdxg0: Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x)) (rsmall (xOf U)).

An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun xprod (xOf U)) (rsmall (xOf U)) (apply_fun xprod x) HxBallG).

We prove the intermediate claim Hsymxprod: apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U)) = apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x).

An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun xprod x) (apply_fun xprod (xOf U)) HdY HxgY Hx0yY).

We prove the intermediate claim Hdxg: Rlt (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (rsmall (xOf U)).

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

An exact proof term for the current goal is Hdxg0.

We prove the intermediate claim Hdf0: Rlt (apply_fun dY (apply_fun f0 x,apply_fun f0 (xOf U))) (rsmall (xOf U)).

We prove the intermediate claim Hdf00: Rlt (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) (rsmall (xOf U)).

An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun f0 (xOf U)) (rsmall (xOf U)) (apply_fun f0 x) HxBallF).

We prove the intermediate claim Hsymf0': apply_fun dY (apply_fun f0 x,apply_fun f0 (xOf U)) = apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x).

An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f0 x) (apply_fun f0 (xOf U)) HdY HxfY Hx0fY).

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

An exact proof term for the current goal is Hdf00.

We prove the intermediate claim Hsymf0: apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x) = apply_fun dY (apply_fun f0 x,apply_fun f0 (xOf U)).

An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f0 (xOf U)) (apply_fun f0 x) HdY Hx0fY HxfY).

We prove the intermediate claim Hdfflt: Rlt (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) (rsmall (xOf U)).

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

An exact proof term for the current goal is Hdf0.

We prove the intermediate claim Hdist0Def: dist (xOf U) = apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U)).

Use reflexivity.

We prove the intermediate claim HdistxDef: dist x = apply_fun dY (apply_fun xprod x,apply_fun f0 x).

Use reflexivity.

We prove the intermediate claim Htri1: Rle (apply_fun dY (apply_fun xprod x,apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x))).

An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun xprod x) (apply_fun xprod (xOf U)) (apply_fun f0 x) HdY HxgY Hx0yY HxfY).

We prove the intermediate claim Htri2: Rle (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x))).

An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun xprod (xOf U)) (apply_fun f0 (xOf U)) (apply_fun f0 x) HdY Hx0yY Hx0fY HxfY).

We prove the intermediate claim HNnat: nat_p (pickN (xOf U)).

An exact proof term for the current goal is (omega_nat_p (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack)).

We prove the intermediate claim Hhalf: add_SNo (rsmall (xOf U)) (rsmall (xOf U)) = delta_of (xOf U).

We prove the intermediate claim Hrdef: rsmall (xOf U) = eps_ (ordsucc (ordsucc (pickN (xOf U)))).

Use reflexivity.

We prove the intermediate claim Hddef: delta_of (xOf U) = eps_ (ordsucc (pickN (xOf U))).

Use reflexivity.

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

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

An exact proof term for the current goal is (eps_ordsucc_half_add (ordsucc (pickN (xOf U))) (omega_nat_p (ordsucc (pickN (xOf U))) (omega_ordsucc (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack)))).

We prove the intermediate claim HdeltaMLeU: Rle deltaM (delta_of (xOf U)).

We prove the intermediate claim HdUin: delta_of (xOf U) ∈ V.

An exact proof term for the current goal is (ReplI G (λU0 : set ⇒ delta_of (xOf U0)) U HUG).

We prove the intermediate claim HdUS: SNo (delta_of (xOf U)).

An exact proof term for the current goal is (HallS (delta_of (xOf U)) HdUin).

We prove the intermediate claim HleS: deltaM ≤ delta_of (xOf U).

An exact proof term for the current goal is (HdeltaMLe (delta_of (xOf U)) HdUin HdUS).

An exact proof term for the current goal is (Rle_of_SNoLe deltaM (delta_of (xOf U)) HdeltaMR HdeltaU_R HleS).

We prove the intermediate claim HdistxR: dist x ∈ R.

An exact proof term for the current goal is (HdistR x HxC0).

We prove the intermediate claim HleAdd: Rle (add_SNo (dist x) deltaM) (add_SNo (dist x) (delta_of (xOf U))).

An exact proof term for the current goal is (Rle_add_SNo_2 (dist x) deltaM (delta_of (xOf U)) HdistxR HdeltaMR HdeltaU_R HdeltaMLeU).

We prove the intermediate claim HdistLe: Rle (dist x) (add_SNo (dist (xOf U)) (delta_of (xOf U))).

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

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

We prove the intermediate claim HdxxLe: Rle (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (rsmall (xOf U)).

An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (rsmall (xOf U)) Hdxg).

We prove the intermediate claim HdffLe: Rle (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) (rsmall (xOf U)).

An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) (rsmall (xOf U)) Hdfflt).

We prove the intermediate claim HabR: apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U)) ∈ R.

An exact proof term for the current goal is (RltE_left (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (rsmall (xOf U)) Hdxg).

We prove the intermediate claim HbR: apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x) ∈ R.

An exact proof term for the current goal is (RleE_left (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x))) Htri2).

We prove the intermediate claim HcR: apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U)) ∈ R.

An exact proof term for the current goal is (RltE_left (dist (xOf U)) eps0 (HxprodClose (xOf U) Hx0C0)).

We prove the intermediate claim HdR: apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x) ∈ R.

An exact proof term for the current goal is (RltE_left (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) (rsmall (xOf U)) Hdfflt).

We prove the intermediate claim HrR: rsmall (xOf U) ∈ R.

An exact proof term for the current goal is (RltE_right 0 (rsmall (xOf U)) Hrpos).

We prove the intermediate claim HcdR: add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) HcR (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) HdR).

We prove the intermediate claim HcrR: add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)) ∈ R.

An exact proof term for the current goal is (real_add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) HcR (rsmall (xOf U)) HrR).

We prove the intermediate claim HsumLe1: Rle (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x))) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)))).

An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x))) HabR HbR HcdR Htri2).

We prove the intermediate claim HsumLe2: Rle (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)))) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)))).

An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U))) HabR HcdR HcrR (Rle_add_SNo_2 (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)) (rsmall (xOf U)) HcR HdR HrR HdffLe)).

We prove the intermediate claim HsumLe3: Rle (apply_fun dY (apply_fun xprod x,apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)))).

An exact proof term for the current goal is (Rle_tra (apply_fun dY (apply_fun xprod x,apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x))) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)))) Htri1 (Rle_tra (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 x))) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (apply_fun dY (apply_fun f0 (xOf U),apply_fun f0 x)))) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)))) HsumLe1 HsumLe2)).

We prove the intermediate claim HsumLe4: Rle (apply_fun dY (apply_fun xprod x,apply_fun f0 x)) (add_SNo (rsmall (xOf U)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)))).

An exact proof term for the current goal is (Rle_tra (apply_fun dY (apply_fun xprod x,apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)))) (add_SNo (rsmall (xOf U)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)))) HsumLe3 (Rle_add_SNo_1 (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) (rsmall (xOf U)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U))) HabR HrR (real_add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) HcR (rsmall (xOf U)) HrR) HdxxLe)).

We prove the intermediate claim HcS: SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))).

An exact proof term for the current goal is (real_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) HcR).

We prove the intermediate claim HrS: SNo (rsmall (xOf U)).

An exact proof term for the current goal is (real_SNo (rsmall (xOf U)) HrR).

We prove the intermediate claim HrhsEq: add_SNo (rsmall (xOf U)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U))) = add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (delta_of (xOf U)).

We prove the intermediate claim Hswap: add_SNo (rsmall (xOf U)) (add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U))) = add_SNo (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (add_SNo (rsmall (xOf U)) (rsmall (xOf U))).

An exact proof term for the current goal is (add_SNo_com_3_0_1 (rsmall (xOf U)) (apply_fun dY (apply_fun xprod (xOf U),apply_fun f0 (xOf U))) (rsmall (xOf U)) HrS HcS HrS).

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

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

Use reflexivity.

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

An exact proof term for the current goal is HsumLe4.

We prove the intermediate claim HgapLt: eps_ (pickN (xOf U)) < dgap (xOf U).

An exact proof term for the current goal is (andER (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack).

We prove the intermediate claim HgapR: eps_ (pickN (xOf U)) ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ (pickN (xOf U))) (SNo_eps_SNoS_omega (pickN (xOf U)) (andEL (pickN (xOf U) ∈ ω) (eps_ (pickN (xOf U)) < dgap (xOf U)) HNpack))).

We prove the intermediate claim HdgapR0: dgap (xOf U) ∈ R.

We prove the intermediate claim HdgapPos0: Rlt 0 (dgap (xOf U)).

An exact proof term for the current goal is (Rlt_0_diff_of_lt (dist (xOf U)) eps0 (HdistClose (xOf U) Hx0C0)).

An exact proof term for the current goal is (RltE_right 0 (dgap (xOf U)) HdgapPos0).

We prove the intermediate claim HgapRlt: Rlt (eps_ (pickN (xOf U))) (dgap (xOf U)).

An exact proof term for the current goal is (RltI (eps_ (pickN (xOf U))) (dgap (xOf U)) HgapR HdgapR0 HgapLt).

We prove the intermediate claim Hsum2eq: add_SNo (delta_of (xOf U)) (delta_of (xOf U)) = eps_ (pickN (xOf U)).

We prove the intermediate claim Hddef: delta_of (xOf U) = eps_ (ordsucc (pickN (xOf U))).

Use reflexivity.

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

An exact proof term for the current goal is (eps_ordsucc_half_add (pickN (xOf U)) HNnat).

We prove the intermediate claim Hsum2Rlt: Rlt (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) (dgap (xOf U)).

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

An exact proof term for the current goal is HgapRlt.

We prove the intermediate claim Hdist0R: dist (xOf U) ∈ R.

An exact proof term for the current goal is (HdistR (xOf U) Hx0C0).

We prove the intermediate claim HlhsR: add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) ∈ R.

An exact proof term for the current goal is (real_add_SNo (dist (xOf U)) Hdist0R (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) (real_add_SNo (delta_of (xOf U)) HdeltaU_R (delta_of (xOf U)) HdeltaU_R)).

We prove the intermediate claim HrhsR: add_SNo (dist (xOf U)) (dgap (xOf U)) ∈ R.

An exact proof term for the current goal is (real_add_SNo (dist (xOf U)) Hdist0R (dgap (xOf U)) HdgapR0).

We prove the intermediate claim Hsum2Lt: Rlt (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))) (add_SNo (dist (xOf U)) (dgap (xOf U))).

We prove the intermediate claim H2dS: SNo (add_SNo (delta_of (xOf U)) (delta_of (xOf U))).

An exact proof term for the current goal is (real_SNo (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) (real_add_SNo (delta_of (xOf U)) HdeltaU_R (delta_of (xOf U)) HdeltaU_R)).

We prove the intermediate claim HdgapS: SNo (dgap (xOf U)).

An exact proof term for the current goal is (real_SNo (dgap (xOf U)) HdgapR0).

We prove the intermediate claim Hdist0S: SNo (dist (xOf U)).

An exact proof term for the current goal is (real_SNo (dist (xOf U)) Hdist0R).

We prove the intermediate claim H2dLt: add_SNo (delta_of (xOf U)) (delta_of (xOf U)) < dgap (xOf U).

An exact proof term for the current goal is (RltE_lt (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) (dgap (xOf U)) Hsum2Rlt).

We prove the intermediate claim HsumLt: add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) < add_SNo (dist (xOf U)) (dgap (xOf U)).

An exact proof term for the current goal is (add_SNo_Lt2 (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) (dgap (xOf U)) Hdist0S H2dS HdgapS H2dLt).

An exact proof term for the current goal is (RltI (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))) (add_SNo (dist (xOf U)) (dgap (xOf U))) HlhsR HrhsR HsumLt).

We prove the intermediate claim Heps0S: SNo eps0.

An exact proof term for the current goal is (real_SNo eps0 Heps0R).

We prove the intermediate claim Hdist0S: SNo (dist (xOf U)).

An exact proof term for the current goal is (real_SNo (dist (xOf U)) Hdist0R).

We prove the intermediate claim HeqCanc: add_SNo (dist (xOf U)) (dgap (xOf U)) = eps0.

We prove the intermediate claim HdgapDef: dgap (xOf U) = add_SNo eps0 (minus_SNo (dist (xOf U))).

Use reflexivity.

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

We prove the intermediate claim HmdistS: SNo (minus_SNo (dist (xOf U))).

An exact proof term for the current goal is (SNo_minus_SNo (dist (xOf U)) Hdist0S).

We prove the intermediate claim Hrot: add_SNo (dist (xOf U)) (add_SNo eps0 (minus_SNo (dist (xOf U)))) = add_SNo (minus_SNo (dist (xOf U))) (add_SNo (dist (xOf U)) eps0).

An exact proof term for the current goal is (add_SNo_rotate_3_1 (dist (xOf U)) eps0 (minus_SNo (dist (xOf U))) Hdist0S Heps0S HmdistS).

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

We prove the intermediate claim Hassoc: add_SNo (minus_SNo (dist (xOf U))) (add_SNo (dist (xOf U)) eps0) = add_SNo (add_SNo (minus_SNo (dist (xOf U))) (dist (xOf U))) eps0.

An exact proof term for the current goal is (add_SNo_assoc (minus_SNo (dist (xOf U))) (dist (xOf U)) eps0 HmdistS Hdist0S Heps0S).

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

We prove the intermediate claim Hlinv: add_SNo (minus_SNo (dist (xOf U))) (dist (xOf U)) = 0.

An exact proof term for the current goal is (add_SNo_minus_SNo_linv (dist (xOf U)) Hdist0S).

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

An exact proof term for the current goal is (add_SNo_0L eps0 Heps0S).

We prove the intermediate claim Hsum2LtEps: Rlt (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))) eps0.

We prove the intermediate claim Hle: Rle (add_SNo (dist (xOf U)) (dgap (xOf U))) eps0.

Apply (RleI (add_SNo (dist (xOf U)) (dgap (xOf U))) eps0 HrhsR Heps0R) to the current goal.

Assume Hlt: Rlt eps0 (add_SNo (dist (xOf U)) (dgap (xOf U))).

We prove the intermediate claim Hrr: Rlt (add_SNo (dist (xOf U)) (dgap (xOf U))) (add_SNo (dist (xOf U)) (dgap (xOf U))).

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

An exact proof term for the current goal is Hlt.

An exact proof term for the current goal is (not_Rlt_refl (add_SNo (dist (xOf U)) (dgap (xOf U))) HrhsR Hrr).

An exact proof term for the current goal is (Rlt_Rle_tra (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))) (add_SNo (dist (xOf U)) (dgap (xOf U))) eps0 Hsum2Lt Hle).

We prove the intermediate claim Hassoc: add_SNo (add_SNo (dist (xOf U)) (delta_of (xOf U))) (delta_of (xOf U)) = add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U))).

Use symmetry.

An exact proof term for the current goal is (add_SNo_assoc (dist (xOf U)) (delta_of (xOf U)) (delta_of (xOf U)) (real_SNo (dist (xOf U)) Hdist0R) (real_SNo (delta_of (xOf U)) HdeltaU_R) (real_SNo (delta_of (xOf U)) HdeltaU_R)).

We prove the intermediate claim HdistAddU: Rlt (add_SNo (dist x) (delta_of (xOf U))) eps0.

We prove the intermediate claim HrhsR: add_SNo (dist (xOf U)) (delta_of (xOf U)) ∈ R.

An exact proof term for the current goal is (real_add_SNo (dist (xOf U)) Hdist0R (delta_of (xOf U)) HdeltaU_R).

We prove the intermediate claim Hle1: Rle (add_SNo (dist x) (delta_of (xOf U))) (add_SNo (add_SNo (dist (xOf U)) (delta_of (xOf U))) (delta_of (xOf U))).

An exact proof term for the current goal is (Rle_add_SNo_1 (dist x) (add_SNo (dist (xOf U)) (delta_of (xOf U))) (delta_of (xOf U)) HdistxR HrhsR HdeltaU_R HdistLe).

We prove the intermediate claim Ht2R: add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U))) ∈ R.

We prove the intermediate claim HleEq: Rle (add_SNo (add_SNo (dist (xOf U)) (delta_of (xOf U))) (delta_of (xOf U))) (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))).

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

An exact proof term for the current goal is (Rle_refl (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))) Ht2R).

We prove the intermediate claim Hle1': Rle (add_SNo (dist x) (delta_of (xOf U))) (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))).

An exact proof term for the current goal is (Rle_tra (add_SNo (dist x) (delta_of (xOf U))) (add_SNo (add_SNo (dist (xOf U)) (delta_of (xOf U))) (delta_of (xOf U))) (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))) Hle1 HleEq).

An exact proof term for the current goal is (Rle_Rlt_tra (add_SNo (dist x) (delta_of (xOf U))) (add_SNo (dist (xOf U)) (add_SNo (delta_of (xOf U)) (delta_of (xOf U)))) eps0 Hle1' Hsum2LtEps).

An exact proof term for the current goal is (Rle_Rlt_tra (add_SNo (dist x) deltaM) (add_SNo (dist x) (delta_of (xOf U))) eps0 HleAdd HdistAddU).

Apply HexDeltaM to the current goal.

Let deltaM be given.

Assume HdeltaMpack: deltaM ∈ R ∧ Rlt 0 deltaM ∧ ∀x : set, x ∈ C0 → Rlt (add_SNo (dist x) deltaM) eps0.

We prove the intermediate claim HdeltaMR: deltaM ∈ R.

Apply (and3E (deltaM ∈ R) (Rlt 0 deltaM) (∀x : set, x ∈ C0 → Rlt (add_SNo (dist x) deltaM) eps0) HdeltaMpack (deltaM ∈ R)) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H1.

We prove the intermediate claim HdeltaMpos: Rlt 0 deltaM.

Apply (and3E (deltaM ∈ R) (Rlt 0 deltaM) (∀x : set, x ∈ C0 → Rlt (add_SNo (dist x) deltaM) eps0) HdeltaMpack (Rlt 0 deltaM)) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H2.

We prove the intermediate claim Hmargin: ∀x : set, x ∈ C0 → Rlt (add_SNo (dist x) deltaM) eps0.

Apply (and3E (deltaM ∈ R) (Rlt 0 deltaM) (∀x : set, x ∈ C0 → Rlt (add_SNo (dist x) deltaM) eps0) HdeltaMpack (∀x : set, x ∈ C0 → Rlt (add_SNo (dist x) deltaM) eps0)) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H3.

We prove the intermediate claim Hexk0: ∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → ∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM.

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

Assume HC0Empty: C0 = Empty.

We prove the intermediate claim HKne: K ≠ Empty.

An exact proof term for the current goal is (directed_set_nonempty K leK HdirK).

We prove the intermediate claim Hexk: ∃k0 : set, k0 ∈ K.

An exact proof term for the current goal is (nonempty_has_element K HKne).

Apply Hexk to the current goal.

Let k0 be given.

Assume Hk0K: k0 ∈ K.

We use k0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hk0K.

Let k be given.

Assume HkK: k ∈ K.

Assume Hk0k: (k0,k) ∈ leK.

Let x be given.

Assume HxC0: x ∈ C0.

We will prove Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM.

We prove the intermediate claim Hx0: x ∈ Empty.

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

An exact proof term for the current goal is HxC0.

An exact proof term for the current goal is (EmptyE x Hx0 (Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM)).

Assume HC0ne: C0 ≠ Empty.

Set Dom to be the term function_space X Y.

We prove the intermediate claim HHcandSubDom3: Hcand ⊆ Dom.

Let f be given.

Assume HfHcand: f ∈ Hcand.

We prove the intermediate claim HfCXY: f ∈ CXY.

An exact proof term for the current goal is (HHcandSubCXY f HfHcand).

An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty f HfCXY).

We prove the intermediate claim HtotsubDom: total_function_on subNet K Dom.

An exact proof term for the current goal is (total_function_on_codomain subNet K Hcand Dom Htotsub HHcandSubDom3).

Set delta to be the term mul_SNo deltaM one_third.

We prove the intermediate claim H13R: one_third ∈ R.

An exact proof term for the current goal is one_third_in_R.

We prove the intermediate claim HdeltaR: delta ∈ R.

An exact proof term for the current goal is (real_mul_SNo deltaM HdeltaMR one_third H13R).

We prove the intermediate claim H13pos: Rlt 0 one_third.

An exact proof term for the current goal is (RltI 0 one_third real_0 H13R one_third_pos).

We prove the intermediate claim HdeltaPos: Rlt 0 delta.

We prove the intermediate claim HdeltaMS: SNo deltaM.

An exact proof term for the current goal is (real_SNo deltaM HdeltaMR).

We prove the intermediate claim H13S: SNo one_third.

An exact proof term for the current goal is (real_SNo one_third H13R).

We prove the intermediate claim H0lt_deltaM: 0 < deltaM.

An exact proof term for the current goal is (RltE_lt 0 deltaM HdeltaMpos).

We prove the intermediate claim H0lt_13: 0 < one_third.

An exact proof term for the current goal is (RltE_lt 0 one_third H13pos).

We prove the intermediate claim H0lt_mul: 0 < mul_SNo deltaM one_third.

An exact proof term for the current goal is (mul_SNo_pos_pos deltaM one_third HdeltaMS H13S H0lt_deltaM H0lt_13).

An exact proof term for the current goal is (RltI 0 delta real_0 HdeltaR H0lt_mul).

We prove the intermediate claim HdeltaPack: delta ∈ R ∧ Rlt 0 delta.

Apply andI to the current goal.

An exact proof term for the current goal is HdeltaR.

An exact proof term for the current goal is HdeltaPos.

Set Gcl to be the term Ascoli_g_pointwise_closure X Tx Y dY F.

Set PU to be the term λx0 U : set ⇒ U ∈ Tx ∧ x0 ∈ U ∧ ∀g : set, g ∈ Gcl → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun g x,apply_fun g x0)) delta.

Set Uof to be the term λx0 : set ⇒ Eps_i (λU : set ⇒ PU x0 U).

We prove the intermediate claim HUof: ∀x0 : set, x0 ∈ C0 → PU x0 (Uof x0).

Let x0 be given.

Assume Hx0C0: x0 ∈ C0.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (HC0subX x0 Hx0C0).

We prove the intermediate claim HexU: ∃U : set, PU x0 U.

An exact proof term for the current goal is (Ascoli_g_pointwise_closure_equicontinuous_bound X Tx Y dY F x0 delta HTx HdY HFcont Hequi Hx0X HdeltaPack).

Apply HexU to the current goal.

Let U be given.

Assume HU: PU x0 U.

An exact proof term for the current goal is (Eps_i_ax (λU0 : set ⇒ PU x0 U0) U HU).

We prove the intermediate claim HUofTx: ∀x0 : set, x0 ∈ C0 → (Uof x0) ∈ Tx.

Let x0 be given.

Assume Hx0C0: x0 ∈ C0.

We prove the intermediate claim Hpack: PU x0 (Uof x0).

An exact proof term for the current goal is (HUof x0 Hx0C0).

Apply (and3E ((Uof x0) ∈ Tx) (x0 ∈ (Uof x0)) (∀g : set, g ∈ Gcl → ∀x : set, x ∈ X → x ∈ (Uof x0) → Rlt (apply_fun dY (apply_fun g x,apply_fun g x0)) delta) Hpack ((Uof x0) ∈ Tx)) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H1.

We prove the intermediate claim HUofMem: ∀x0 : set, x0 ∈ C0 → x0 ∈ (Uof x0).

Let x0 be given.

Assume Hx0C0: x0 ∈ C0.

We prove the intermediate claim Hpack: PU x0 (Uof x0).

An exact proof term for the current goal is (HUof x0 Hx0C0).

Apply (and3E ((Uof x0) ∈ Tx) (x0 ∈ (Uof x0)) (∀g : set, g ∈ Gcl → ∀x : set, x ∈ X → x ∈ (Uof x0) → Rlt (apply_fun dY (apply_fun g x,apply_fun g x0)) delta) Hpack (x0 ∈ (Uof x0))) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H2.

Set Fam to be the term Repl C0 (λx0 : set ⇒ Uof x0).

We prove the intermediate claim HFamSubTx: Fam ⊆ Tx.

Let U be given.

Assume HUfam: U ∈ Fam.

Apply (ReplE_impred C0 (λx0 : set ⇒ Uof x0) U HUfam) to the current goal.

Let x0 be given.

Assume Hx0C0: x0 ∈ C0.

Assume HUeq: U = Uof x0.

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

An exact proof term for the current goal is (HUofTx x0 Hx0C0).

We prove the intermediate claim HC0covFam: C0 ⊆ ⋃ Fam.

Let x0 be given.

Assume Hx0C0: x0 ∈ C0.

We will prove x0 ∈ ⋃ Fam.

We prove the intermediate claim HUin: Uof x0 ∈ Fam.

An exact proof term for the current goal is (ReplI C0 (λx1 : set ⇒ Uof x1) x0 Hx0C0).

We prove the intermediate claim Hx0U: x0 ∈ Uof x0.

An exact proof term for the current goal is (HUofMem x0 Hx0C0).

An exact proof term for the current goal is (UnionI Fam x0 (Uof x0) Hx0U HUin).

We prove the intermediate claim HcovProp: ∀Fam0 : set, (Fam0 ⊆ Tx ∧ C0 ⊆ ⋃ Fam0) → has_finite_subcover C0 Tx Fam0.

An exact proof term for the current goal is (iffEL (compact_space C0 (subspace_topology X Tx C0)) (∀Fam0 : set, (Fam0 ⊆ Tx ∧ C0 ⊆ ⋃ Fam0) → has_finite_subcover C0 Tx Fam0) (compact_subspace_via_ambient_covers X Tx C0 HTx HC0subX) Hcompact).

We prove the intermediate claim HfinSub: has_finite_subcover C0 Tx Fam.

Apply (HcovProp Fam) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is HFamSubTx.

An exact proof term for the current goal is HC0covFam.

Apply HfinSub to the current goal.

Let G be given.

Assume HGpack: G ⊆ Fam ∧ finite G ∧ C0 ⊆ ⋃ G.

We prove the intermediate claim HGsubFam: G ⊆ Fam.

Apply (and3E (G ⊆ Fam) (finite G) (C0 ⊆ ⋃ G) HGpack (G ⊆ Fam)) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H1.

We prove the intermediate claim HGfin: finite G.

Apply (and3E (G ⊆ Fam) (finite G) (C0 ⊆ ⋃ G) HGpack (finite G)) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H2.

We prove the intermediate claim HC0covG: C0 ⊆ ⋃ G.

Apply (and3E (G ⊆ Fam) (finite G) (C0 ⊆ ⋃ G) HGpack (C0 ⊆ ⋃ G)) to the current goal.

Assume H1 H2 H3.

An exact proof term for the current goal is H3.

Set PxOf to be the term λU x0 : set ⇒ x0 ∈ C0 ∧ U = Uof x0.

Set xOf to be the term λU : set ⇒ Eps_i (λx0 : set ⇒ PxOf U x0).

We prove the intermediate claim HxOf: ∀U : set, U ∈ G → PxOf U (xOf U).

Let U be given.

Assume HUG: U ∈ G.

We prove the intermediate claim HUFam: U ∈ Fam.

An exact proof term for the current goal is (HGsubFam U HUG).

Apply (ReplE_impred C0 (λx0 : set ⇒ Uof x0) U HUFam) to the current goal.

Let x0 be given.

Assume Hx0C0: x0 ∈ C0.

Assume HUeq: U = Uof x0.

We prove the intermediate claim Hexx0: ∃x1 : set, PxOf U x1.

We use x0 to witness the existential quantifier.

An exact proof term for the current goal is (andI (x0 ∈ C0) (U = Uof x0) Hx0C0 HUeq).

Apply Hexx0 to the current goal.

Let x1 be given.

Assume Hx1: PxOf U x1.

An exact proof term for the current goal is (Eps_i_ax (λx2 : set ⇒ PxOf U x2) x1 Hx1).

Set PkOf to be the term λU k0 : set ⇒ k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k) (xOf U))) delta.

Set kOf to be the term λU : set ⇒ Eps_i (λk0 : set ⇒ PkOf U k0).

We prove the intermediate claim HkOf: ∀U : set, U ∈ G → PkOf U (kOf U).

Let U be given.

Assume HUG: U ∈ G.

We prove the intermediate claim HxPack: xOf U ∈ C0 ∧ U = Uof (xOf U).

An exact proof term for the current goal is (HxOf U HUG).

We prove the intermediate claim Hx0C0: xOf U ∈ C0.

An exact proof term for the current goal is (andEL (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim Hx0X: xOf U ∈ X.

An exact proof term for the current goal is (HC0subX (xOf U) Hx0C0).

Set Dom to be the term function_space X Y.

We prove the intermediate claim HHcandSubDom2: Hcand ⊆ Dom.

Let f be given.

Assume HfHcand: f ∈ Hcand.

We prove the intermediate claim HfCXY: f ∈ CXY.

An exact proof term for the current goal is (HHcandSubCXY f HfHcand).

An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty f HfCXY).

We prove the intermediate claim HtotsubDom: total_function_on subNet K Dom.

An exact proof term for the current goal is (total_function_on_codomain subNet K Hcand Dom Htotsub HHcandSubDom2).

We prove the intermediate claim HxprodInDom: xprod ∈ Dom.

We prove the intermediate claim HxprodInCXY: xprod ∈ CXY.

An exact proof term for the current goal is (HHcandSubCXY xprod HxprodInHcandMem).

An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty xprod HxprodInCXY).

We prove the intermediate claim HxprodY0: apply_fun xprod (xOf U) ∈ Y.

An exact proof term for the current goal is ((function_on_of_function_space xprod X Y HxprodInDom) (xOf U) Hx0X).

Set Ball to be the term open_ball Y dY (apply_fun xprod (xOf U)) delta.

We prove the intermediate claim HBallTy: Ball ∈ Ty.

An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun xprod (xOf U)) delta HdY HxprodY0 HdeltaPos).

Set Sx to be the term {f ∈ Dom|apply_fun f (xOf U) ∈ Ball}.

Set Spt to be the term (pointwise_subbasis X Tx Y Ty) ∪ {Dom}.

Set Tpt to be the term pointwise_convergence_topology X Tx Y Ty.

We prove the intermediate claim HSxSub: Sx ⊆ Dom.

Let f be given.

Assume Hf: f ∈ Sx.

An exact proof term for the current goal is (SepE1 Dom (λf0 : set ⇒ apply_fun f0 (xOf U) ∈ Ball) f Hf).

We prove the intermediate claim HSxPow: Sx ∈ 𝒫 Dom.

An exact proof term for the current goal is (PowerI Dom Sx HSxSub).

We prove the intermediate claim HSxSubb: Sx ∈ pointwise_subbasis X Tx Y Ty.

We will prove Sx ∈ {S ∈ 𝒫 Dom|∃x1 U1 : set, x1 ∈ X ∧ U1 ∈ Ty ∧ S = {f ∈ Dom|apply_fun f x1 ∈ U1}}.

Apply (SepI (𝒫 Dom) (λS : set ⇒ ∃x1 U1 : set, x1 ∈ X ∧ U1 ∈ Ty ∧ S = {f ∈ Dom|apply_fun f x1 ∈ U1}) Sx) to the current goal.

An exact proof term for the current goal is HSxPow.

We use (xOf U) to witness the existential quantifier.

We use Ball to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0X.

An exact proof term for the current goal is HBallTy.

Use reflexivity.

We prove the intermediate claim HSxSpt: Sx ∈ Spt.

An exact proof term for the current goal is (binunionI1 (pointwise_subbasis X Tx Y Ty) {Dom} Sx HSxSubb).

We prove the intermediate claim HSpt: subbasis_on Dom Spt.

We will prove Spt ⊆ 𝒫 Dom ∧ ⋃ Spt = Dom.

Apply andI to the current goal.

Let s be given.

Assume Hs: s ∈ Spt.

We will prove s ∈ 𝒫 Dom.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} s (s ∈ 𝒫 Dom)) to the current goal.

Assume Hsp: s ∈ pointwise_subbasis X Tx Y Ty.

An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x2 U2 : set, x2 ∈ X ∧ U2 ∈ Ty ∧ S0 = {f0 ∈ Dom|apply_fun f0 x2 ∈ U2}) s Hsp).

Assume HsDom: s ∈ {Dom}.

We prove the intermediate claim Hseq: s = Dom.

An exact proof term for the current goal is (SingE Dom s HsDom).

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

An exact proof term for the current goal is (PowerI Dom Dom (Subq_ref Dom)).

An exact proof term for the current goal is Hs.

Apply set_ext to the current goal.

Let f be given.

Assume HfU: f ∈ ⋃ Spt.

We will prove f ∈ Dom.

Apply (UnionE_impred Spt f HfU (f ∈ Dom)) to the current goal.

Let U0 be given.

Assume HfU0: f ∈ U0.

Assume HU0: U0 ∈ Spt.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} U0 (f ∈ Dom)) to the current goal.

Assume HUp: U0 ∈ pointwise_subbasis X Tx Y Ty.

We prove the intermediate claim HUpow: U0 ∈ 𝒫 Dom.

An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x2 U2 : set, x2 ∈ X ∧ U2 ∈ Ty ∧ S0 = {f0 ∈ Dom|apply_fun f0 x2 ∈ U2}) U0 HUp).

An exact proof term for the current goal is (PowerE Dom U0 HUpow f HfU0).

Assume HUDom: U0 ∈ {Dom}.

We prove the intermediate claim HUeq: U0 = Dom.

An exact proof term for the current goal is (SingE Dom U0 HUDom).

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

An exact proof term for the current goal is HfU0.

An exact proof term for the current goal is HU0.

Let f be given.

Assume HfD: f ∈ Dom.

We prove the intermediate claim HDomInS: Dom ∈ Spt.

An exact proof term for the current goal is (binunionI2 (pointwise_subbasis X Tx Y Ty) {Dom} Dom (SingI Dom)).

An exact proof term for the current goal is (UnionI Spt f Dom HfD HDomInS).

We prove the intermediate claim HTpt: topology_on Dom Tpt.

An exact proof term for the current goal is (pointwise_convergence_topology_is_topology X Tx Y Ty HTx HTy).

We prove the intermediate claim HSxOpen: Sx ∈ Tpt.

An exact proof term for the current goal is (generated_topology_from_subbasis_contains_subbasis_elem Dom Spt Sx HSpt HSxSpt).

We prove the intermediate claim HxprodInSx: xprod ∈ Sx.

We prove the intermediate claim Hcenter: apply_fun xprod (xOf U) ∈ Ball.

An exact proof term for the current goal is (center_in_open_ball Y dY (apply_fun xprod (xOf U)) delta HdY HxprodY0 HdeltaPos).

An exact proof term for the current goal is (SepI Dom (λf0 : set ⇒ apply_fun f0 (xOf U) ∈ Ball) xprod HxprodInDom Hcenter).

We prove the intermediate claim HtailProp: ∀U0 : set, U0 ∈ Tpt → xprod ∈ U0 → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun subNet i ∈ U0.

Apply (and7E (topology_on Dom Tpt) (directed_set K leK) (total_function_on subNet K Dom) (functional_graph subNet) (graph_domain_subset subNet K) (xprod ∈ Dom) (∀U0 : set, U0 ∈ Tpt → xprod ∈ U0 → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun subNet i ∈ U0) HconvDom (∀U0 : set, U0 ∈ Tpt → xprod ∈ U0 → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun subNet i ∈ U0)) to the current goal.

Assume H1 H2 H3 H4 H5 H6 H7.

An exact proof term for the current goal is H7.

We prove the intermediate claim Hexk: ∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ Sx.

An exact proof term for the current goal is (HtailProp Sx HSxOpen HxprodInSx).

Apply Hexk to the current goal.

Let k0 be given.

Assume Hk0pair: k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ Sx.

We prove the intermediate claim Hk0K: k0 ∈ K.

An exact proof term for the current goal is (andEL (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun subNet k ∈ Sx) Hk0pair).

We prove the intermediate claim Htail: ∀k : set, k ∈ K → (k0,k) ∈ leK → Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k) (xOf U))) delta.

Let k be given.

Assume HkK: k ∈ K.

Assume Hk0k: (k0,k) ∈ leK.

We prove the intermediate claim HsubkSx: apply_fun subNet k ∈ Sx.

An exact proof term for the current goal is (andER (k0 ∈ K) (∀k1 : set, k1 ∈ K → (k0,k1) ∈ leK → apply_fun subNet k1 ∈ Sx) Hk0pair k HkK Hk0k).

We prove the intermediate claim HsubkFS: apply_fun subNet k ∈ Dom.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K Dom k HtotsubDom HkK).

We prove the intermediate claim HsubkVal: apply_fun (apply_fun subNet k) (xOf U) ∈ Ball.

An exact proof term for the current goal is (SepE2 Dom (λf0 : set ⇒ apply_fun f0 (xOf U) ∈ Ball) (apply_fun subNet k) HsubkSx).

An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun xprod (xOf U)) delta (apply_fun (apply_fun subNet k) (xOf U)) HsubkVal).

We prove the intermediate claim Hexk0: ∃k1 : set, PkOf U k1.

We use k0 to witness the existential quantifier.

An exact proof term for the current goal is (andI (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k) (xOf U))) delta) Hk0K Htail).

Apply Hexk0 to the current goal.

Let k1 be given.

Assume Hk1: PkOf U k1.

An exact proof term for the current goal is (Eps_i_ax (λk2 : set ⇒ PkOf U k2) k1 Hk1).

Set F0 to be the term Repl G (λU0 : set ⇒ kOf U0).

We prove the intermediate claim HF0fin: finite F0.

An exact proof term for the current goal is (Repl_finite (λU0 : set ⇒ kOf U0) G HGfin).

We prove the intermediate claim HF0subK: F0 ⊆ K.

Let i be given.

Assume Hi: i ∈ F0.

Apply (ReplE_impred G (λU0 : set ⇒ kOf U0) i Hi) to the current goal.

Let U be given.

Assume HUG: U ∈ G.

Assume Hieq: i = kOf U.

We prove the intermediate claim Hk0: kOf U ∈ K.

An exact proof term for the current goal is (andEL (kOf U ∈ K) (∀k : set, k ∈ K → (kOf U,k) ∈ leK → Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k) (xOf U))) delta) (HkOf U HUG)).

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

An exact proof term for the current goal is Hk0.

We prove the intermediate claim HexK0: ∃k0 : set, k0 ∈ K ∧ ∀i : set, i ∈ F0 → (i,k0) ∈ leK.

An exact proof term for the current goal is (directed_set_finite_upper_bound K leK F0 HdirK HF0fin HF0subK).

Apply HexK0 to the current goal.

Let k0 be given.

Assume Hk0ub.

We use k0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (k0 ∈ K) (∀i : set, i ∈ F0 → (i,k0) ∈ leK) Hk0ub).

Let k be given.

Assume HkK: k ∈ K.

Assume Hk0k: (k0,k) ∈ leK.

Let x be given.

Assume HxC0: x ∈ C0.

We will prove Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM.

We prove the intermediate claim HxUnion: x ∈ ⋃ G.

An exact proof term for the current goal is (HC0covG x HxC0).

Apply (UnionE_impred G x HxUnion (Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM)) to the current goal.

Let U be given.

Assume HxU: x ∈ U.

Assume HUG: U ∈ G.

We prove the intermediate claim HxPack: xOf U ∈ C0 ∧ U = Uof (xOf U).

An exact proof term for the current goal is (HxOf U HUG).

We prove the intermediate claim Hx0C0: xOf U ∈ C0.

An exact proof term for the current goal is (andEL (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim HUeq: U = Uof (xOf U).

An exact proof term for the current goal is (andER (xOf U ∈ C0) (U = Uof (xOf U)) HxPack).

We prove the intermediate claim Hx0X: xOf U ∈ X.

An exact proof term for the current goal is (HC0subX (xOf U) Hx0C0).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HC0subX x HxC0).

We prove the intermediate claim HUofProp: ∀g : set, g ∈ Hcand → ∀x1 : set, x1 ∈ X → x1 ∈ U → Rlt (apply_fun dY (apply_fun g x1,apply_fun g (xOf U))) delta.

Let g be given.

Assume HgHcand: g ∈ Hcand.

Let x1 be given.

Assume Hx1X: x1 ∈ X.

Assume Hx1U: x1 ∈ U.

We prove the intermediate claim HUofPU: PU (xOf U) (Uof (xOf U)).

An exact proof term for the current goal is (HUof (xOf U) Hx0C0).

We prove the intermediate claim Hforall: ∀g0 : set, g0 ∈ Gcl → ∀x2 : set, x2 ∈ X → x2 ∈ (Uof (xOf U)) → Rlt (apply_fun dY (apply_fun g0 x2,apply_fun g0 (xOf U))) delta.

An exact proof term for the current goal is (andER (((Uof (xOf U)) ∈ Tx) ∧ ((xOf U) ∈ (Uof (xOf U)))) (∀g0 : set, g0 ∈ Gcl → ∀x2 : set, x2 ∈ X → x2 ∈ (Uof (xOf U)) → Rlt (apply_fun dY (apply_fun g0 x2,apply_fun g0 (xOf U))) delta) HUofPU).

We prove the intermediate claim HgGcl: g ∈ Gcl.

We will prove g ∈ Gcl.

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

An exact proof term for the current goal is HgHcand.

We prove the intermediate claim Hx1Uof: x1 ∈ (Uof (xOf U)).

We will prove x1 ∈ (Uof (xOf U)).

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

An exact proof term for the current goal is Hx1U.

An exact proof term for the current goal is (Hforall g HgGcl x1 Hx1X Hx1Uof).

We prove the intermediate claim HsubkH: apply_fun subNet k ∈ Hcand.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K Hcand k Htotsub HkK).

We prove the intermediate claim Hd1: Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) delta.

An exact proof term for the current goal is (HUofProp (apply_fun subNet k) HsubkH x HxX HxU).

We prove the intermediate claim Hd3: Rlt (apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U))) delta.

An exact proof term for the current goal is (HUofProp xprod HxprodInHcandMem x HxX HxU).

We prove the intermediate claim HkOfU: PkOf U (kOf U).

An exact proof term for the current goal is (HkOf U HUG).

We prove the intermediate claim HkOfK: kOf U ∈ K.

An exact proof term for the current goal is (andEL (kOf U ∈ K) (∀k1 : set, k1 ∈ K → (kOf U,k1) ∈ leK → Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k1) (xOf U))) delta) HkOfU).

We prove the intermediate claim HkOfInF0: kOf U ∈ F0.

An exact proof term for the current goal is (ReplI G (λU0 : set ⇒ kOf U0) U HUG).

We prove the intermediate claim HkOf_le_k0: (kOf U,k0) ∈ leK.

An exact proof term for the current goal is (andER (k0 ∈ K) (∀i : set, i ∈ F0 → (i,k0) ∈ leK) Hk0ub (kOf U) HkOfInF0).

We prove the intermediate claim HkOf_le_k: (kOf U,k) ∈ leK.

An exact proof term for the current goal is (directed_set_trans K leK HdirK (kOf U) k0 k HkOfK (andEL (k0 ∈ K) (∀i : set, i ∈ F0 → (i,k0) ∈ leK) Hk0ub) HkK HkOf_le_k0 Hk0k).

We prove the intermediate claim Hd2: Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k) (xOf U))) delta.

An exact proof term for the current goal is (andER (kOf U ∈ K) (∀k1 : set, k1 ∈ K → (kOf U,k1) ∈ leK → Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k1) (xOf U))) delta) HkOfU k HkK HkOf_le_k).

We prove the intermediate claim HsubkDom: apply_fun subNet k ∈ Dom.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K Dom k HtotsubDom HkK).

We prove the intermediate claim HsubkFun: ∀z : set, z ∈ X → apply_fun (apply_fun subNet k) z ∈ Y.

Let z be given.

Assume HzX: z ∈ X.

An exact proof term for the current goal is ((function_on_of_function_space (apply_fun subNet k) X Y HsubkDom) z HzX).

We prove the intermediate claim Htri1: Rle (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod x))).

An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun (apply_fun subNet k) x) (apply_fun (apply_fun subNet k) (xOf U)) (apply_fun xprod x) HdY (HsubkFun x HxX) (HsubkFun (xOf U) Hx0X) (Hxprodfun x HxX)).

We prove the intermediate claim Htri2: Rle (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod x)) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x))).

An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun (apply_fun subNet k) (xOf U)) (apply_fun xprod (xOf U)) (apply_fun xprod x) HdY (HsubkFun (xOf U) Hx0X) (Hxprodfun (xOf U) Hx0X) (Hxprodfun x HxX)).

We prove the intermediate claim Hd2': Rlt (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) delta.

We prove the intermediate claim HsymEq: apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U)) = apply_fun dY (apply_fun xprod (xOf U),apply_fun (apply_fun subNet k) (xOf U)).

An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun (apply_fun subNet k) (xOf U)) (apply_fun xprod (xOf U)) HdY (HsubkFun (xOf U) Hx0X) (Hxprodfun (xOf U) Hx0X)).

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

An exact proof term for the current goal is Hd2.

We prove the intermediate claim Hd3': Rlt (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x)) delta.

We prove the intermediate claim HsymEq3: apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x) = apply_fun dY (apply_fun xprod x,apply_fun xprod (xOf U)).

An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun xprod (xOf U)) (apply_fun xprod x) HdY (Hxprodfun (xOf U) Hx0X) (Hxprodfun x HxX)).

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

An exact proof term for the current goal is Hd3.

We prove the intermediate claim Hlt23: Rlt (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x))) (add_SNo delta delta).

An exact proof term for the current goal is (Rlt_add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) delta (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x)) delta Hd2' Hd3').

We prove the intermediate claim Hsumlt: Rlt (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x)))) (add_SNo delta (add_SNo delta delta)).

An exact proof term for the current goal is (Rlt_add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) delta (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x))) (add_SNo delta delta) Hd1 Hlt23).

We prove the intermediate claim HdeltaMS: SNo deltaM.

An exact proof term for the current goal is (real_SNo deltaM HdeltaMR).

We prove the intermediate claim HdeltaS: SNo delta.

An exact proof term for the current goal is (real_SNo delta HdeltaR).

We prove the intermediate claim HsumEq: add_SNo delta (add_SNo delta delta) = deltaM.

rewrite the current goal using (add_SNo_assoc delta delta delta HdeltaS HdeltaS HdeltaS) (from left to right) at position 1.

We prove the intermediate claim Hdef23: two_thirds = add_SNo one_third one_third.

Use reflexivity.

We prove the intermediate claim H23R: two_thirds ∈ R.

An exact proof term for the current goal is two_thirds_in_R.

We prove the intermediate claim H23S: SNo two_thirds.

An exact proof term for the current goal is (real_SNo two_thirds H23R).

We prove the intermediate claim H13S: SNo one_third.

An exact proof term for the current goal is (real_SNo one_third H13R).

rewrite the current goal using (mul_SNo_distrL deltaM one_third one_third HdeltaMS H13S H13S) (from right to left) at position 1.

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

rewrite the current goal using (mul_SNo_distrL deltaM two_thirds one_third HdeltaMS H23S H13S) (from right to left) at position 1.

rewrite the current goal using (add_SNo_com two_thirds one_third H23S H13S) (from left to right) at position 1.

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

An exact proof term for the current goal is (mul_SNo_oneR deltaM HdeltaMS).

We prove the intermediate claim HsumEq': deltaM = add_SNo delta (add_SNo delta delta).

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

Use reflexivity.

We prove the intermediate claim HsumltDM: Rlt (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x)))) deltaM.

Set sumTerm to be the term (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x)))).

We prove the intermediate claim HsumR: sumTerm ∈ R.

An exact proof term for the current goal is (RltE_left sumTerm (add_SNo delta (add_SNo delta delta)) Hsumlt).

We prove the intermediate claim Hsumlt': sumTerm < add_SNo delta (add_SNo delta delta).

An exact proof term for the current goal is (RltE_lt sumTerm (add_SNo delta (add_SNo delta delta)) Hsumlt).

We prove the intermediate claim HsumltDM': sumTerm < deltaM.

We prove the intermediate claim HsumS: SNo sumTerm.

An exact proof term for the current goal is (real_SNo sumTerm HsumR).

We prove the intermediate claim HddS: SNo (add_SNo delta delta).

An exact proof term for the current goal is (SNo_add_SNo delta delta HdeltaS HdeltaS).

We prove the intermediate claim HboundS: SNo (add_SNo delta (add_SNo delta delta)).

An exact proof term for the current goal is (SNo_add_SNo delta (add_SNo delta delta) HdeltaS HddS).

We prove the intermediate claim HboundLe: add_SNo delta (add_SNo delta delta) ≤ deltaM.

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

An exact proof term for the current goal is (SNoLe_ref deltaM).

An exact proof term for the current goal is (SNoLtLe_tra sumTerm (add_SNo delta (add_SNo delta delta)) deltaM HsumS HboundS HdeltaMS Hsumlt' HboundLe).

An exact proof term for the current goal is (RltI sumTerm deltaM HsumR HdeltaMR HsumltDM').

Set termA to be the term (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)).

Set termB to be the term (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod x))).

Set termSum to be the term (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x)))).

We prove the intermediate claim HleAB: Rle termA termB.

An exact proof term for the current goal is Htri1.

We prove the intermediate claim HleBS: Rle termB termSum.

An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod x)) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x))) (RltE_left (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun (apply_fun subNet k) (xOf U))) delta Hd1) ((metric_on_function_on Y dY HdY) (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod x) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun (apply_fun subNet k) (xOf U)) (apply_fun xprod x) (HsubkFun (xOf U) Hx0X) (Hxprodfun x HxX))) (RltE_left (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) (xOf U),apply_fun xprod (xOf U))) (apply_fun dY (apply_fun xprod (xOf U),apply_fun xprod x))) (add_SNo delta delta) Hlt23) Htri2).

We prove the intermediate claim HleAS: Rle termA termSum.

An exact proof term for the current goal is (Rle_tra termA termB termSum HleAB HleBS).

An exact proof term for the current goal is (Rle_Rlt_tra termA termSum deltaM HleAS HsumltDM).

Apply Hexk0 to the current goal.

Let k0 be given.

Assume Hk0pack: k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → ∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM.

We use k0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → ∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM) Hk0pack).

Let k be given.

Assume HkK: k ∈ K.

Assume Hk0k: (k0,k) ∈ leK.

We will prove apply_fun subNet k ∈ s.

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

Apply SepI to the current goal.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K CXY k HtotsubCXY HkK).

Let x be given.

Assume HxC0: x ∈ C0.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HC0subX x HxC0).

We prove the intermediate claim HsubkCXY: apply_fun subNet k ∈ CXY.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K CXY k HtotsubCXY HkK).

We prove the intermediate claim HsubkFS: apply_fun subNet k ∈ function_space X Y.

An exact proof term for the current goal is (SepE1 (function_space X Y) (λf : set ⇒ continuous_map X Tx Y Ty f) (apply_fun subNet k) HsubkCXY).

We prove the intermediate claim HsubkFun: function_on (apply_fun subNet k) X Y.

An exact proof term for the current goal is (function_on_of_function_space (apply_fun subNet k) X Y HsubkFS).

We prove the intermediate claim HsubkY: apply_fun (apply_fun subNet k) x ∈ Y.

An exact proof term for the current goal is (HsubkFun x HxX).

We prove the intermediate claim HxprodY: apply_fun xprod x ∈ Y.

An exact proof term for the current goal is (Hxprodfun x HxX).

We prove the intermediate claim Hf0Y: apply_fun f0 x ∈ Y.

An exact proof term for the current goal is (Hf0fun x HxX).

We prove the intermediate claim Hk0tail: ∀k1 : set, k1 ∈ K → (k0,k1) ∈ leK → ∀x1 : set, x1 ∈ C0 → Rlt (apply_fun dY (apply_fun (apply_fun subNet k1) x1,apply_fun xprod x1)) deltaM.

An exact proof term for the current goal is (andER (k0 ∈ K) (∀k1 : set, k1 ∈ K → (k0,k1) ∈ leK → ∀x1 : set, x1 ∈ C0 → Rlt (apply_fun dY (apply_fun (apply_fun subNet k1) x1,apply_fun xprod x1)) deltaM) Hk0pack).

We prove the intermediate claim HdsubLt: Rlt (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM.

An exact proof term for the current goal is (Hk0tail k HkK Hk0k x HxC0).

We prove the intermediate claim HdsubR: apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x) ∈ R.

We prove the intermediate claim HpIn: (apply_fun (apply_fun subNet k) x,apply_fun xprod x) ∈ setprod Y Y.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun (apply_fun subNet k) x) (apply_fun xprod x) HsubkY HxprodY).

An exact proof term for the current goal is (HdYfun (apply_fun (apply_fun subNet k) x,apply_fun xprod x) HpIn).

We prove the intermediate claim HdistxR: dist x ∈ R.

An exact proof term for the current goal is (HdistR x HxC0).

We prove the intermediate claim HdsubLe: Rle (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM.

An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM HdsubLt).

We prove the intermediate claim HsumLe: Rle (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) (dist x)) (add_SNo deltaM (dist x)).

An exact proof term for the current goal is (Rle_add_SNo_1 (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) deltaM (dist x) HdsubR HdeltaMR HdistxR HdsubLe).

We prove the intermediate claim HdistxS: SNo (dist x).

An exact proof term for the current goal is (real_SNo (dist x) HdistxR).

We prove the intermediate claim HdeltaMS: SNo deltaM.

An exact proof term for the current goal is (real_SNo deltaM HdeltaMR).

We prove the intermediate claim Hcomm: add_SNo (dist x) deltaM = add_SNo deltaM (dist x).

An exact proof term for the current goal is (add_SNo_com (dist x) deltaM HdistxS HdeltaMS).

We prove the intermediate claim HsumLt2: Rlt (add_SNo deltaM (dist x)) eps0.

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

An exact proof term for the current goal is (Hmargin x HxC0).

We prove the intermediate claim HsumLt: Rlt (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) (dist x)) eps0.

An exact proof term for the current goal is (Rle_Rlt_tra (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) (dist x)) (add_SNo deltaM (dist x)) eps0 HsumLe HsumLt2).

We prove the intermediate claim Htri: Rle (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) (apply_fun dY (apply_fun xprod x,apply_fun f0 x))).

An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun (apply_fun subNet k) x) (apply_fun xprod x) (apply_fun f0 x) HdY HsubkY HxprodY Hf0Y).

An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun (apply_fun subNet k) x,apply_fun xprod x)) (apply_fun dY (apply_fun xprod x,apply_fun f0 x))) eps0 Htri HsumLt).

Assume HsCXY: s ∈ {CXY}.

We prove the intermediate claim Hseq: s = CXY.

An exact proof term for the current goal is (SingE CXY s HsCXY).

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

We prove the intermediate claim HKne: K ≠ Empty.

An exact proof term for the current goal is (directed_set_nonempty K leK HdirK).

We prove the intermediate claim Hexk0: ∃k0 : set, k0 ∈ K.

An exact proof term for the current goal is (nonempty_has_element K HKne).

Apply Hexk0 to the current goal.

Let k0 be given.

Assume Hk0K: k0 ∈ K.

We use k0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hk0K.

Let k be given.

Assume HkK: k ∈ K.

Assume _: (k0,k) ∈ leK.

An exact proof term for the current goal is (total_function_on_apply_fun_in_Y subNet K CXY k HtotsubCXY HkK).

An exact proof term for the current goal is HsScc.

An exact proof term for the current goal is (net_converges_on_generated_topology_from_subbasis_of_subeventual CXY Scc subNet K leK xprod HScc HdirK HtotsubCXY HgraphSub HdomSub HxprodCXY HevS).

An exact proof term for the current goal is (net_converges_on_in_subspace_topology CXY Tcc Hcand subNet K leK xprod HTcc HHcandSubCXY HdirK Htotsub HgraphSub HdomSub HxprodInHcandMem HconvAmbient).

An exact proof term for the current goal is HconvS.