Let s be given.

Assume Hs: s ∈ Scc.

We will prove s ∈ Tco.

Apply (binunionE' (compact_convergence_subbasis_metric X Tx Y dY) {CXY} s (s ∈ Tco)) to the current goal.

Assume Hsm: s ∈ compact_convergence_subbasis_metric X Tx Y dY.

We prove the intermediate claim Hex: ∃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 ⇒ ∃C f eps : set, compact_space C (subspace_topology X Tx C) ∧ C ⊆ X ∧ f ∈ CXY ∧ eps ∈ R ∧ Rlt 0 eps ∧ S0 = {g ∈ CXY|∀x : set, x ∈ C → Rlt (apply_fun dY (apply_fun g x,apply_fun f x)) eps}) s Hsm).

Apply Hex to the current goal.

Let C0 be given.

Assume Hcf.

Apply Hcf to the current goal.

Let f0 be given.

Assume Hcfe.

Apply Hcfe to the current goal.

Let eps0 be given.

Assume Hpkg.

We prove the intermediate claim Hcore: ((((compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) ∧ f0 ∈ CXY) ∧ eps0 ∈ R) ∧ Rlt 0 eps0).

An exact proof term for the current goal is (andEL ((((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}) Hpkg).

We prove the intermediate claim Hseq: 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 (andER ((((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}) Hpkg).

We prove the intermediate claim Hpre1: (((compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) ∧ f0 ∈ CXY) ∧ eps0 ∈ R).

An exact proof term for the current goal is (andEL (((compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) ∧ f0 ∈ CXY) ∧ eps0 ∈ R) (Rlt 0 eps0) Hcore).

We prove the intermediate claim Heps0pos: Rlt 0 eps0.

An exact proof term for the current goal is (andER (((compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) ∧ f0 ∈ CXY) ∧ eps0 ∈ R) (Rlt 0 eps0) Hcore).

We prove the intermediate claim Hpre2: ((compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) ∧ f0 ∈ CXY).

An exact proof term for the current goal is (andEL ((compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) ∧ f0 ∈ CXY) (eps0 ∈ R) Hpre1).

We prove the intermediate claim Heps0R: eps0 ∈ R.

An exact proof term for the current goal is (andER ((compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) ∧ f0 ∈ CXY) (eps0 ∈ R) Hpre1).

We prove the intermediate claim Hpre3: compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X.

An exact proof term for the current goal is (andEL (compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) (f0 ∈ CXY) Hpre2).

We prove the intermediate claim Hf0C: f0 ∈ CXY.

An exact proof term for the current goal is (andER (compact_space C0 (subspace_topology X Tx C0) ∧ C0 ⊆ X) (f0 ∈ CXY) Hpre2).

We prove the intermediate claim HC0comp: compact_space C0 (subspace_topology X Tx C0).

An exact proof term for the current goal is (andEL (compact_space C0 (subspace_topology X Tx C0)) (C0 ⊆ X) Hpre3).

We prove the intermediate claim HC0subX: C0 ⊆ X.

An exact proof term for the current goal is (andER (compact_space C0 (subspace_topology X Tx C0)) (C0 ⊆ X) Hpre3).

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

Set S0 to be the term {g ∈ CXY|∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0}.

We prove the intermediate claim HS0open: open_in CXY Tco S0.

Apply (ex13_1_local_open_subset CXY Tco S0 HTco) to the current goal.

Let g be given.

Assume HgS0: g ∈ S0.

We will prove ∃U ∈ Tco, g ∈ U ∧ U ⊆ S0.

We prove the intermediate claim HgC: g ∈ CXY.

An exact proof term for the current goal is (SepE1 CXY (λg0 : set ⇒ ∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) eps0) g HgS0).

We prove the intermediate claim Hgunif: ∀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 (λg0 : set ⇒ ∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) eps0) g HgS0).

We prove the intermediate claim HCsub: CXY ⊆ function_space X Y.

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

We prove the intermediate claim HgFS: g ∈ function_space X Y.

An exact proof term for the current goal is (HCsub g HgC).

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

An exact proof term for the current goal is (HCsub f0 Hf0C).

We prove the intermediate claim Hcontg: continuous_map X Tx Y Ty g.

An exact proof term for the current goal is (SepE2 (function_space X Y) (λh : set ⇒ continuous_map X Tx Y Ty h) g HgC).

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

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

We prove the intermediate claim Hfung: function_on g X Y.

An exact proof term for the current goal is (function_on_of_function_space g X Y HgFS).

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

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

Set dgap to be the term λx : set ⇒ add_SNo eps0 (minus_SNo (apply_fun dY (apply_fun g x,apply_fun f0 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 HxX: x ∈ X.

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

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

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

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

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

We prove the intermediate claim Hdistlt: Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0.

An exact proof term for the current goal is (Hgunif 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 (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps0 Hdistlt).

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).

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

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)).

An exact proof term for the current goal is HNpack.

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

Set Uof to be the term λx : set ⇒ (preimage_of X f0 (open_ball Y dY (apply_fun f0 x) (rsmall x))) ∩ (preimage_of X g (open_ball Y dY (apply_fun g 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 HfxY: apply_fun f0 x ∈ Y.

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

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

An exact proof term for the current goal is (Hfung 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 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 HBgTy: open_ball Y dY (apply_fun g x) (rsmall x) ∈ Ty.

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

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 Hcontf0 (open_ball Y dY (apply_fun f0 x) (rsmall x)) HBfTy).

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

An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty g Hcontg (open_ball Y dY (apply_fun g x) (rsmall x)) HBgTy).

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 f0 (open_ball Y dY (apply_fun f0 x) (rsmall x))) (preimage_of X g (open_ball Y dY (apply_fun g x) (rsmall x))) HTx HpreF HpreG).

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 HfxY: apply_fun f0 x ∈ Y.

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

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

An exact proof term for the current goal is (Hfung 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 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 HxInG: x ∈ preimage_of X g (open_ball Y dY (apply_fun g x) (rsmall x)).

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

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

An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun g u ∈ open_ball Y dY (apply_fun g 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 f0 (open_ball Y dY (apply_fun f0 x) (rsmall x))) (preimage_of X g (open_ball Y dY (apply_fun g x) (rsmall x))) x HxInF HxInG).

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) HC0comp).

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).

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.

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

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)).

An exact proof term for the current goal is Hpack.

Set rbig to be the term λU : set ⇒ eps_ (ordsucc (pickN (xOf U))).

Set Kof to be the term λU : set ⇒ (closure_of X Tx U) ∩ C0.

Set Sof to be the term λU : set ⇒ {h ∈ function_space X Y|Kof U ⊆ preimage_of X h (open_ball Y dY (apply_fun g (xOf U)) (rbig U))}.

Set F to be the term {Sof U|U ∈ G}.

We prove the intermediate claim HFsub: F ⊆ compact_open_subbasis X Tx Y Ty.

Let S be given.

Assume HS: S ∈ F.

Apply (ReplE_impred G (λU0 : set ⇒ Sof U0) S HS) to the current goal.

Let U be given.

Assume HUG: U ∈ G.

Assume HSeq: S = Sof U.

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

We will prove Sof U ∈ compact_open_subbasis X Tx Y Ty.

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 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 HxX: xOf U ∈ X.

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

We prove the intermediate claim HgxY: apply_fun g (xOf U) ∈ Y.

An exact proof term for the current goal is (Hfung (xOf U) 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) HxC0).

We prove the intermediate claim HrbigR: rbig 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 (rbig U) (SNo_eps_SNoS_omega (ordsucc (pickN (xOf U))) Hn1omega)).

We prove the intermediate claim Hrbigpos: Rlt 0 (rbig 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 (rbig U) real_0 HrbigR Hlt0).

We prove the intermediate claim HBTy: open_ball Y dY (apply_fun g (xOf U)) (rbig U) ∈ Ty.

An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun g (xOf U)) (rbig U) HdY HgxY Hrbigpos).

We prove the intermediate claim HKUcomp: compact_space (Kof U) (subspace_topology X Tx (Kof U)).

Set TxC0 to be the term subspace_topology X Tx C0.

We prove the intermediate claim HTxC0: topology_on C0 TxC0.

An exact proof term for the current goal is (compact_space_topology C0 TxC0 HC0comp).

We prove the intermediate claim HclUclosed: closed_in X Tx (closure_of X Tx U).

An exact proof term for the current goal is (andER (closure_of X Tx (closure_of X Tx U) = closure_of X Tx U) (closed_in X Tx (closure_of X Tx U)) (closure_idempotent_and_closed X Tx U HTx)).

We prove the intermediate claim HKUclosed: closed_in C0 TxC0 (Kof U).

Apply (iffER (closed_in C0 TxC0 (Kof U)) (∃C : set, closed_in X Tx C ∧ (Kof U) = C ∩ C0) (closed_in_subspace_iff_intersection X Tx C0 (Kof U) HTx HC0subX)) to the current goal.

We use (closure_of X Tx U) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HclUclosed.

Use reflexivity.

We prove the intermediate claim HKUcompC0: compact_space (Kof U) (subspace_topology C0 TxC0 (Kof U)).

An exact proof term for the current goal is (closed_subspace_compact C0 TxC0 (Kof U) HC0comp HKUclosed).

We prove the intermediate claim HKUsubC0: (Kof U) ⊆ C0.

An exact proof term for the current goal is (binintersect_Subq_2 (closure_of X Tx U) C0).

We prove the intermediate claim HeqTop: subspace_topology C0 TxC0 (Kof U) = subspace_topology X Tx (Kof U).

An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx C0 (Kof U) HTx HC0subX HKUsubC0).

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

An exact proof term for the current goal is HKUcompC0.

We prove the intermediate claim HKUsubX: Kof U ⊆ X.

Let x be given.

Assume HxK: x ∈ Kof U.

We will prove x ∈ X.

An exact proof term for the current goal is (HC0subX x (binintersectE2 (closure_of X Tx U) C0 x HxK)).

We prove the intermediate claim HSprop: ∃K0 U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ Sof U = {f ∈ function_space X Y|K0 ⊆ preimage_of X f U0}.

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

We use (open_ball Y dY (apply_fun g (xOf U)) (rbig U)) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HKUcomp.

An exact proof term for the current goal is HKUsubX.

An exact proof term for the current goal is HBTy.

Use reflexivity.

We prove the intermediate claim HSsubPow: Sof U ∈ 𝒫 (function_space X Y).

Apply PowerI to the current goal.

Let h be given.

Assume Hh: h ∈ Sof U.

An exact proof term for the current goal is (SepE1 (function_space X Y) (λh0 : set ⇒ Kof U ⊆ preimage_of X h0 (open_ball Y dY (apply_fun g (xOf U)) (rbig U))) h Hh).

An exact proof term for the current goal is (SepI (𝒫 (function_space X Y)) (λS0 : set ⇒ ∃K0 U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S0 = {f ∈ function_space X Y|K0 ⊆ preimage_of X f U0}) (Sof U) HSsubPow HSprop).

We prove the intermediate claim HFfin: finite F.

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

Set Dom to be the term function_space X Y.

Set Ssub to be the term compact_open_subbasis X Tx Y Ty.

Set Tdom to be the term compact_convergence_topology X Tx Y Ty.

We prove the intermediate claim HSsub: subbasis_on Dom Ssub.

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

We prove the intermediate claim HTdom: topology_on Dom Tdom.

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

We prove the intermediate claim HFsubTdom: F ⊆ Tdom.

Let S be given.

Assume HS: S ∈ F.

We prove the intermediate claim HSsubbasis: S ∈ Ssub.

An exact proof term for the current goal is (HFsub S HS).

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis Dom Ssub S HSsub HSsubbasis).

We prove the intermediate claim HFpow: F ∈ 𝒫 Tdom.

An exact proof term for the current goal is (PowerI Tdom F HFsubTdom).

We prove the intermediate claim HFopen: intersection_of_family Dom F ∈ Tdom.

An exact proof term for the current goal is (finite_intersection_in_topology Dom Tdom F HTdom HFpow HFfin).

Set Vbig to be the term intersection_of_family (function_space X Y) F.

Set Ubig to be the term Vbig ∩ CXY.

We prove the intermediate claim HUbigIn: Ubig ∈ Tco.

An exact proof term for the current goal is (subspace_topologyI Dom Tdom CXY Vbig HFopen).

We use Ubig to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HUbigIn.

Apply andI to the current goal.

We prove the intermediate claim HgVbig: g ∈ Vbig.

We prove the intermediate claim HVeq: Vbig = intersection_of_family Dom F.

Use reflexivity.

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

We prove the intermediate claim Hall: ∀S : set, S ∈ F → g ∈ S.

Let S be given.

Assume HS: S ∈ F.

Apply (ReplE_impred G (λU0 : set ⇒ Sof U0) S HS) to the current goal.

Let U0 be given.

Assume HU0G: U0 ∈ G.

Assume HSeq: S = Sof U0.

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

We will prove g ∈ Sof U0.

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

An exact proof term for the current goal is (HxOf U0 HU0G).

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

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

We prove the intermediate claim HU0eq: U0 = Uof (xOf U0).

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

We prove the intermediate claim HxX: xOf U0 ∈ X.

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

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

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

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

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

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

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

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

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

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

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

We prove the intermediate claim HrbigEq: add_SNo (rsmall (xOf U0)) (rsmall (xOf U0)) = rbig U0.

We prove the intermediate claim Hn0Omega: pickN (xOf U0) ∈ ω.

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

We prove the intermediate claim Hn1Omega: ordsucc (pickN (xOf U0)) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (pickN (xOf U0)) Hn0Omega).

We prove the intermediate claim Hn1Nat: nat_p (ordsucc (pickN (xOf U0))).

An exact proof term for the current goal is (omega_nat_p (ordsucc (pickN (xOf U0))) Hn1Omega).

An exact proof term for the current goal is (eps_ordsucc_half_add (ordsucc (pickN (xOf U0))) Hn1Nat).

We prove the intermediate claim Hrbigpos: Rlt 0 (rbig U0).

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

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

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

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

We prove the intermediate claim HrR: rbig U0 ∈ R.

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

An exact proof term for the current goal is (RltI 0 (rbig U0) real_0 HrR Hlt0).

We prove the intermediate claim HgxY: apply_fun g (xOf U0) ∈ Y.

An exact proof term for the current goal is (Hfung (xOf U0) HxX).

We prove the intermediate claim HBTy: open_ball Y dY (apply_fun g (xOf U0)) (rbig U0) ∈ Ty.

An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun g (xOf U0)) (rbig U0) HdY HgxY Hrbigpos).

We prove the intermediate claim HsubK: Kof U0 ⊆ preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rbig U0)).

Let x be given.

Assume HxK: x ∈ Kof U0.

We will prove x ∈ preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rbig U0)).

We prove the intermediate claim HxCl: x ∈ closure_of X Tx U0.

An exact proof term for the current goal is (binintersectE1 (closure_of X Tx U0) C0 x HxK).

We prove the intermediate claim HUgSub: U0 ⊆ preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0))).

Let t be given.

Assume HtU0: t ∈ U0.

We will prove t ∈ preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0))).

We prove the intermediate claim HtUof: t ∈ Uof (xOf U0).

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

An exact proof term for the current goal is HtU0.

We prove the intermediate claim HUofdef: Uof (xOf U0) = (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U0)) (rsmall (xOf U0)))) ∩ (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))).

Use reflexivity.

We prove the intermediate claim HtInter: t ∈ (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U0)) (rsmall (xOf U0)))) ∩ (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))).

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

An exact proof term for the current goal is HtUof.

An exact proof term for the current goal is (binintersectE2 (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U0)) (rsmall (xOf U0)))) (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))) t HtInter).

We prove the intermediate claim HBTySmall: open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)) ∈ Ty.

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

We prove the intermediate claim HpreInTx: preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0))) ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty g Hcontg (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0))) HBTySmall).

We prove the intermediate claim HpreSubX: preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0))) ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))) HTx HpreInTx).

We prove the intermediate claim HclMon: closure_of X Tx U0 ⊆ closure_of X Tx (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))).

An exact proof term for the current goal is (closure_monotone X Tx U0 (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))) HTx HUgSub HpreSubX).

We prove the intermediate claim HxCl2: x ∈ closure_of X Tx (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))).

An exact proof term for the current goal is (HclMon x HxCl).

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

An exact proof term for the current goal is (closure_preimage_open_ball_sub_preimage_open_ball_add_radius X Tx Y dY g (apply_fun g (xOf U0)) (rsmall (xOf U0)) HTx HdY Hcontg HgxY (SNoS_omega_real (rsmall (xOf U0)) (SNo_eps_SNoS_omega (ordsucc (ordsucc (pickN (xOf U0)))) (omega_ordsucc (ordsucc (pickN (xOf U0))) (omega_ordsucc (pickN (xOf U0)) (andEL (pickN (xOf U0) ∈ ω) (eps_ (pickN (xOf U0)) < dgap (xOf U0)) HNpack)))))) Hrpos x HxCl2.

An exact proof term for the current goal is (SepI (function_space X Y) (λh : set ⇒ Kof U0 ⊆ preimage_of X h (open_ball Y dY (apply_fun g (xOf U0)) (rbig U0))) g HgFS HsubK).

An exact proof term for the current goal is (intersection_of_familyI Dom F g HgFS Hall).

An exact proof term for the current goal is (binintersectI Vbig CXY g HgVbig HgC).

Let h be given.

Assume Hh: h ∈ Ubig.

We will prove h ∈ S0.

We prove the intermediate claim HhC: h ∈ CXY.

An exact proof term for the current goal is (binintersectE2 Vbig CXY h Hh).

We prove the intermediate claim HhV: h ∈ Vbig.

An exact proof term for the current goal is (binintersectE1 Vbig CXY h Hh).

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

Let x be given.

Assume HxC0: x ∈ C0.

We will prove Rlt (apply_fun dY (apply_fun h x,apply_fun f0 x)) eps0.

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

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

Apply (UnionE_impred G x HxUG) to the current goal.

Let U0 be given.

Assume HxU0: x ∈ U0.

Assume HU0G: U0 ∈ G.

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

An exact proof term for the current goal is (HxOf U0 HU0G).

We prove the intermediate claim HU0eq: U0 = Uof (xOf U0).

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

We prove the intermediate claim HSofInF: Sof U0 ∈ F.

An exact proof term for the current goal is (ReplI G (λU1 : set ⇒ Sof U1) U0 HU0G).

We prove the intermediate claim HVeq: Vbig = intersection_of_family (function_space X Y) F.

Use reflexivity.

We prove the intermediate claim HhInt: h ∈ intersection_of_family (function_space X Y) F.

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

An exact proof term for the current goal is HhV.

We prove the intermediate claim HhSof: h ∈ Sof U0.

An exact proof term for the current goal is (intersection_of_familyE2 (function_space X Y) F h HhInt (Sof U0) HSofInF).

We prove the intermediate claim HKofSubh: Kof U0 ⊆ preimage_of X h (open_ball Y dY (apply_fun g (xOf U0)) (rbig U0)).

An exact proof term for the current goal is (SepE2 (function_space X Y) (λh0 : set ⇒ Kof U0 ⊆ preimage_of X h0 (open_ball Y dY (apply_fun g (xOf U0)) (rbig U0))) h HhSof).

We prove the intermediate claim HU0UFam: U0 ∈ UFam.

An exact proof term for the current goal is (HGsub U0 HU0G).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (HUFamSubTx U0 HU0UFam).

We prove the intermediate claim HU0subX: U0 ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0Tx).

We prove the intermediate claim HxClU0: x ∈ closure_of X Tx U0.

An exact proof term for the current goal is ((closure_contains_set X Tx U0 HTx HU0subX) x HxU0).

We prove the intermediate claim HxKof: x ∈ Kof U0.

We prove the intermediate claim HKdef: Kof U0 = (closure_of X Tx U0) ∩ C0.

Use reflexivity.

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

An exact proof term for the current goal is (binintersectI (closure_of X Tx U0) C0 x HxClU0 HxC0).

We prove the intermediate claim HxPre: x ∈ preimage_of X h (open_ball Y dY (apply_fun g (xOf U0)) (rbig U0)).

An exact proof term for the current goal is (HKofSubh x HxKof).

We prove the intermediate claim HhxBall: apply_fun h x ∈ open_ball Y dY (apply_fun g (xOf U0)) (rbig U0).

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun h u ∈ open_ball Y dY (apply_fun g (xOf U0)) (rbig U0)) x HxPre).

We prove the intermediate claim Hdist_h_gxOf: Rlt (apply_fun dY (apply_fun g (xOf U0),apply_fun h x)) (rbig U0).

An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun g (xOf U0)) (rbig U0) (apply_fun h x) HhxBall).

We prove the intermediate claim HxOfC0: xOf U0 ∈ C0.

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

We prove the intermediate claim HxOfX: xOf U0 ∈ X.

An exact proof term for the current goal is (HC0subX (xOf U0) HxOfC0).

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 HfxOfY: apply_fun f0 (xOf U0) ∈ Y.

An exact proof term for the current goal is (Hfunf0 (xOf U0) HxOfX).

We prove the intermediate claim HgxOfY: apply_fun g (xOf U0) ∈ Y.

An exact proof term for the current goal is (Hfung (xOf U0) HxOfX).

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

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

We prove the intermediate claim Hdist_gxOf_fxOf: Rlt (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 (xOf U0))) eps0.

An exact proof term for the current goal is (Hgunif (xOf U0) HxOfC0).

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

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

An exact proof term for the current goal is HxU0.

We prove the intermediate claim HUofdef2: Uof (xOf U0) = (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U0)) (rsmall (xOf U0)))) ∩ (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))).

Use reflexivity.

We prove the intermediate claim HxInter2: x ∈ (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U0)) (rsmall (xOf U0)))) ∩ (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))).

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

An exact proof term for the current goal is HxUof.

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

An exact proof term for the current goal is (binintersectE1 (preimage_of X f0 (open_ball Y dY (apply_fun f0 (xOf U0)) (rsmall (xOf U0)))) (preimage_of X g (open_ball Y dY (apply_fun g (xOf U0)) (rsmall (xOf U0)))) x HxInter2).

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

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 U0)) (rsmall (xOf U0))) x HxFPre).

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

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

Set d1 to be the term apply_fun dY (apply_fun g (xOf U0),apply_fun h x).

Set d2 to be the term apply_fun dY (apply_fun g (xOf U0),apply_fun f0 (xOf U0)).

Set d3 to be the term apply_fun dY (apply_fun f0 (xOf U0),apply_fun f0 x).

We prove the intermediate claim HhFS: h ∈ function_space X Y.

An exact proof term for the current goal is (HCsub h HhC).

We prove the intermediate claim Hfunh: function_on h X Y.

An exact proof term for the current goal is (function_on_of_function_space h X Y HhFS).

We prove the intermediate claim HhxY: apply_fun h x ∈ Y.

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

We prove the intermediate claim Hd1Rlt: Rlt d1 (rbig U0).

We prove the intermediate claim Hd1def: d1 = apply_fun dY (apply_fun g (xOf U0),apply_fun h x).

Use reflexivity.

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

An exact proof term for the current goal is Hdist_h_gxOf.

We prove the intermediate claim Hd1Slt: d1 < rbig U0.

An exact proof term for the current goal is (RltE_lt d1 (rbig U0) Hd1Rlt).

We prove the intermediate claim Hd2Slt: d2 < eps0.

We prove the intermediate claim Hd2def: d2 = apply_fun dY (apply_fun g (xOf U0),apply_fun f0 (xOf U0)).

Use reflexivity.

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

An exact proof term for the current goal is (RltE_lt d2 eps0 Hdist_gxOf_fxOf).

We prove the intermediate claim Hd3Rlt: Rlt d3 (rsmall (xOf U0)).

We prove the intermediate claim Hd3def: d3 = apply_fun dY (apply_fun f0 (xOf U0),apply_fun f0 x).

Use reflexivity.

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

An exact proof term for the current goal is Hdist_fxOf_fx.

We prove the intermediate claim Hd3Slt: d3 < rsmall (xOf U0).

An exact proof term for the current goal is (RltE_lt d3 (rsmall (xOf U0)) Hd3Rlt).

We prove the intermediate claim Hd1R: d1 ∈ R.

An exact proof term for the current goal is (RltE_left d1 (rbig U0) Hd1Rlt).

We prove the intermediate claim Hd2R: d2 ∈ R.

An exact proof term for the current goal is (RltE_left d2 eps0 Hdist_gxOf_fxOf).

We prove the intermediate claim Hd3R: d3 ∈ R.

An exact proof term for the current goal is (RltE_left d3 (rsmall (xOf U0)) Hd3Rlt).

We prove the intermediate claim Hd1S: SNo d1.

An exact proof term for the current goal is (real_SNo d1 Hd1R).

We prove the intermediate claim Hd2S: SNo d2.

An exact proof term for the current goal is (real_SNo d2 Hd2R).

We prove the intermediate claim Hd3S: SNo d3.

An exact proof term for the current goal is (real_SNo d3 Hd3R).

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

An exact proof term for the current goal is (HpickN (xOf U0) HxOfC0).

We prove the intermediate claim HN0O: pickN (xOf U0) ∈ ω.

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

We prove the intermediate claim HepsN0LtGap: eps_ (pickN (xOf U0)) < dgap (xOf U0).

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

We prove the intermediate claim HN0Nat: nat_p (pickN (xOf U0)).

An exact proof term for the current goal is (omega_nat_p (pickN (xOf U0)) HN0O).

We prove the intermediate claim HrbigR: rbig U0 ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (rbig U0) (SNo_eps_SNoS_omega (ordsucc (pickN (xOf U0))) (omega_ordsucc (pickN (xOf U0)) HN0O))).

We prove the intermediate claim HrsmallR: rsmall (xOf U0) ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (rsmall (xOf U0)) (SNo_eps_SNoS_omega (ordsucc (ordsucc (pickN (xOf U0)))) (omega_ordsucc (ordsucc (pickN (xOf U0))) (omega_ordsucc (pickN (xOf U0)) HN0O)))).

We prove the intermediate claim HrbigS: SNo (rbig U0).

An exact proof term for the current goal is (real_SNo (rbig U0) HrbigR).

We prove the intermediate claim HrsmallS: SNo (rsmall (xOf U0)).

An exact proof term for the current goal is (real_SNo (rsmall (xOf U0)) HrsmallR).

We prove the intermediate claim HrsmallLtRbig: rsmall (xOf U0) < rbig U0.

An exact proof term for the current goal is (SNo_eps_decr (ordsucc (ordsucc (pickN (xOf U0)))) (omega_ordsucc (ordsucc (pickN (xOf U0))) (omega_ordsucc (pickN (xOf U0)) HN0O)) (ordsucc (pickN (xOf U0))) (ordsuccI2 (ordsucc (pickN (xOf U0))))).

Set sum13 to be the term add_SNo d1 d3.

We prove the intermediate claim Hsum13S: SNo sum13.

An exact proof term for the current goal is (SNo_add_SNo d1 d3 Hd1S Hd3S).

We prove the intermediate claim Hsum13LtRad: sum13 < add_SNo (rbig U0) (rsmall (xOf U0)).

An exact proof term for the current goal is (add_SNo_Lt3 d1 d3 (rbig U0) (rsmall (xOf U0)) Hd1S Hd3S HrbigS HrsmallS Hd1Slt Hd3Slt).

We prove the intermediate claim HrbigEq: add_SNo (rsmall (xOf U0)) (rsmall (xOf U0)) = rbig U0.

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

An exact proof term for the current goal is (omega_ordsucc (pickN (xOf U0)) HN0O).

We prove the intermediate claim Hn1Nat: nat_p (ordsucc (pickN (xOf U0))).

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

An exact proof term for the current goal is (eps_ordsucc_half_add (ordsucc (pickN (xOf U0))) Hn1Nat).

We prove the intermediate claim HradLtEpsN0: add_SNo (rbig U0) (rsmall (xOf U0)) < eps_ (pickN (xOf U0)).

We prove the intermediate claim HrsmallLt: rsmall (xOf U0) < rbig U0.

An exact proof term for the current goal is HrsmallLtRbig.

We prove the intermediate claim Hstep1: add_SNo (rbig U0) (rsmall (xOf U0)) < add_SNo (rbig U0) (rbig U0).

An exact proof term for the current goal is (add_SNo_Lt2 (rbig U0) (rsmall (xOf U0)) (rbig U0) HrbigS HrsmallS HrbigS HrsmallLt).

We prove the intermediate claim HepsHalf: add_SNo (rbig U0) (rbig U0) = eps_ (pickN (xOf U0)).

We prove the intermediate claim HrbigDef: rbig U0 = eps_ (ordsucc (pickN (xOf U0))).

Use reflexivity.

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

An exact proof term for the current goal is (eps_ordsucc_half_add (pickN (xOf U0)) HN0Nat).

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

An exact proof term for the current goal is Hstep1.

We prove the intermediate claim Hsum13LtEpsN0: sum13 < eps_ (pickN (xOf U0)).

We prove the intermediate claim HradLeEpsN0: add_SNo (rbig U0) (rsmall (xOf U0)) ≤ eps_ (pickN (xOf U0)).

An exact proof term for the current goal is (SNoLtLe (add_SNo (rbig U0) (rsmall (xOf U0))) (eps_ (pickN (xOf U0))) HradLtEpsN0).

An exact proof term for the current goal is (SNoLtLe_tra sum13 (add_SNo (rbig U0) (rsmall (xOf U0))) (eps_ (pickN (xOf U0))) Hsum13S (SNo_add_SNo (rbig U0) (rsmall (xOf U0)) HrbigS HrsmallS) (real_SNo (eps_ (pickN (xOf U0))) (SNoS_omega_real (eps_ (pickN (xOf U0))) (SNo_eps_SNoS_omega (pickN (xOf U0)) HN0O))) Hsum13LtRad HradLeEpsN0).

We prove the intermediate claim HdgapR: dgap (xOf U0) ∈ R.

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

Use reflexivity.

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

An exact proof term for the current goal is (real_add_SNo eps0 Heps0R (minus_SNo d2) (real_minus_SNo d2 Hd2R)).

We prove the intermediate claim HepsN0LeGap: eps_ (pickN (xOf U0)) ≤ dgap (xOf U0).

An exact proof term for the current goal is (SNoLtLe (eps_ (pickN (xOf U0))) (dgap (xOf U0)) HepsN0LtGap).

We prove the intermediate claim Hsum13LtGap: sum13 < dgap (xOf U0).

An exact proof term for the current goal is (SNoLtLe_tra sum13 (eps_ (pickN (xOf U0))) (dgap (xOf U0)) Hsum13S (real_SNo (eps_ (pickN (xOf U0))) (SNoS_omega_real (eps_ (pickN (xOf U0))) (SNo_eps_SNoS_omega (pickN (xOf U0)) HN0O))) (real_SNo (dgap (xOf U0)) HdgapR) Hsum13LtEpsN0 HepsN0LeGap).

We prove the intermediate claim HsumFinalLt: add_SNo sum13 d2 < eps0.

We prove the intermediate claim Hsum13d2Lt: add_SNo sum13 d2 < add_SNo (dgap (xOf U0)) d2.

An exact proof term for the current goal is (add_SNo_Lt1 sum13 d2 (dgap (xOf U0)) Hsum13S Hd2S (real_SNo (dgap (xOf U0)) HdgapR) Hsum13LtGap).

We prove the intermediate claim Hd2S2: SNo d2.

An exact proof term for the current goal is Hd2S.

We prove the intermediate claim Hd2inv: add_SNo (minus_SNo d2) d2 = 0.

An exact proof term for the current goal is (add_SNo_minus_SNo_linv d2 Hd2S2).

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 HdEq: dgap (xOf U0) = add_SNo eps0 (minus_SNo d2).

Use reflexivity.

We prove the intermediate claim HgapPlus: add_SNo (dgap (xOf U0)) d2 = eps0.

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

We prove the intermediate claim Hassoc: add_SNo eps0 (add_SNo (minus_SNo d2) d2) = add_SNo (add_SNo eps0 (minus_SNo d2)) d2.

An exact proof term for the current goal is (add_SNo_assoc eps0 (minus_SNo d2) d2 Heps0S (SNo_minus_SNo d2 Hd2S2) Hd2S2).

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

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

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

We prove the intermediate claim HgapLe: add_SNo (dgap (xOf U0)) d2 ≤ eps0.

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

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

An exact proof term for the current goal is (SNoLtLe_tra (add_SNo sum13 d2) (add_SNo (dgap (xOf U0)) d2) eps0 (SNo_add_SNo sum13 d2 Hsum13S Hd2S) (SNo_add_SNo (dgap (xOf U0)) d2 (real_SNo (dgap (xOf U0)) HdgapR) Hd2S) Heps0S Hsum13d2Lt HgapLe).

We prove the intermediate claim Hsum13R: sum13 ∈ R.

An exact proof term for the current goal is (real_add_SNo d1 Hd1R d3 Hd3R).

We prove the intermediate claim HsumFinalR: add_SNo sum13 d2 ∈ R.

An exact proof term for the current goal is (real_add_SNo sum13 Hsum13R d2 Hd2R).

We prove the intermediate claim HsumFinalRlt: Rlt (add_SNo sum13 d2) eps0.

An exact proof term for the current goal is (RltI (add_SNo sum13 d2) eps0 HsumFinalR Heps0R HsumFinalLt).

We prove the intermediate claim Htri2: Rle (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)) (add_SNo d2 d3).

An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun g (xOf U0)) (apply_fun f0 (xOf U0)) (apply_fun f0 x) HdY HgxOfY HfxOfY HfxY).

We prove the intermediate claim Htri1: Rle (apply_fun dY (apply_fun h x,apply_fun f0 x)) (add_SNo (apply_fun dY (apply_fun h x,apply_fun g (xOf U0))) (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x))).

An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun h x) (apply_fun g (xOf U0)) (apply_fun f0 x) HdY HhxY HgxOfY HfxY).

We prove the intermediate claim Hsymhg: apply_fun dY (apply_fun h x,apply_fun g (xOf U0)) = d1.

An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun h x) (apply_fun g (xOf U0)) HdY HhxY HgxOfY).

We prove the intermediate claim Htri1': Rle (apply_fun dY (apply_fun h x,apply_fun f0 x)) (add_SNo d1 (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x))).

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

An exact proof term for the current goal is Htri1.

We prove the intermediate claim Htri2Le: d1 ≤ d1.

An exact proof term for the current goal is (SNoLe_ref d1).

We prove the intermediate claim Htri2LeR: (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)) ≤ add_SNo d2 d3.

An exact proof term for the current goal is (SNoLe_of_Rle (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)) (add_SNo d2 d3) Htri2).

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).

We prove the intermediate claim Hpair_gx_fx: (apply_fun g (xOf U0),apply_fun f0 x) ∈ setprod Y Y.

An exact proof term for the current goal is (tuple_2_setprod Y Y (apply_fun g (xOf U0)) HgxOfY (apply_fun f0 x) HfxY).

We prove the intermediate claim Hbd1R: apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x) ∈ R.

An exact proof term for the current goal is (HdYfun (apply_fun g (xOf U0),apply_fun f0 x) Hpair_gx_fx).

We prove the intermediate claim Hbd1S: SNo (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)).

An exact proof term for the current goal is (real_SNo (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)) Hbd1R).

We prove the intermediate claim HsumLe: add_SNo d1 (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)) ≤ add_SNo d1 (add_SNo d2 d3).

An exact proof term for the current goal is (add_SNo_Le2 d1 (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)) (add_SNo d2 d3) Hd1S Hbd1S (SNo_add_SNo d2 d3 Hd2S Hd3S) Htri2LeR).

We prove the intermediate claim HtriR: Rle (add_SNo d1 (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x))) (add_SNo d1 (add_SNo d2 d3)).

An exact proof term for the current goal is (Rle_of_SNoLe (add_SNo d1 (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x))) (add_SNo d1 (add_SNo d2 d3)) (real_add_SNo d1 Hd1R (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x)) Hbd1R) (real_add_SNo d1 Hd1R (add_SNo d2 d3) (real_add_SNo d2 Hd2R d3 Hd3R)) HsumLe).

We prove the intermediate claim HtriAll: Rle (apply_fun dY (apply_fun h x,apply_fun f0 x)) (add_SNo d1 (add_SNo d2 d3)).

An exact proof term for the current goal is (Rle_tra (apply_fun dY (apply_fun h x,apply_fun f0 x)) (add_SNo d1 (apply_fun dY (apply_fun g (xOf U0),apply_fun f0 x))) (add_SNo d1 (add_SNo d2 d3)) Htri1' HtriR).

We prove the intermediate claim HeqSum: add_SNo d1 (add_SNo d2 d3) = add_SNo sum13 d2.

We prove the intermediate claim Hassoc1: add_SNo d1 (add_SNo d2 d3) = add_SNo (add_SNo d1 d2) d3.

An exact proof term for the current goal is (add_SNo_assoc d1 d2 d3 Hd1S Hd2S Hd3S).

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

We prove the intermediate claim Hcom12: add_SNo d1 d2 = add_SNo d2 d1.

An exact proof term for the current goal is (add_SNo_com d1 d2 Hd1S Hd2S).

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

We prove the intermediate claim Hassoc2: add_SNo d2 (add_SNo d1 d3) = add_SNo (add_SNo d2 d1) d3.

An exact proof term for the current goal is (add_SNo_assoc d2 d1 d3 Hd2S Hd1S Hd3S).

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

We prove the intermediate claim Hcom2: add_SNo d2 (add_SNo d1 d3) = add_SNo (add_SNo d1 d3) d2.

An exact proof term for the current goal is (add_SNo_com d2 (add_SNo d1 d3) Hd2S (SNo_add_SNo d1 d3 Hd1S Hd3S)).

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

Use reflexivity.

We prove the intermediate claim HtriAll2: Rle (apply_fun dY (apply_fun h x,apply_fun f0 x)) (add_SNo sum13 d2).

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

An exact proof term for the current goal is HtriAll.

An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun dY (apply_fun h x,apply_fun f0 x)) (add_SNo sum13 d2) eps0 HtriAll2 HsumFinalRlt).

An exact proof term for the current goal is (SepI CXY (λg0 : set ⇒ ∀x : set, x ∈ C0 → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) eps0) h HhC HhProp).

An exact proof term for the current goal is (open_in_elem CXY Tco S0 HS0open).

Assume HsC: s ∈ {CXY}.

We prove the intermediate claim Hseq: s = CXY.

An exact proof term for the current goal is (SingE CXY s HsC).

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

We prove the intermediate claim HCopen: CXY ∈ Tco.

An exact proof term for the current goal is (topology_has_X CXY Tco HTco).

An exact proof term for the current goal is HCopen.

An exact proof term for the current goal is Hs.