Let X, Tx, Y, dY, K and U be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Assume HK: compact_space K (subspace_topology X Tx K).
Assume HKsubX: K ⊆ X.
Assume HU: U ∈ metric_topology Y dY.
Set Ty to be the term metric_topology Y dY.
Set CXY to be the term continuous_function_space X Tx Y Ty.
Set Tcc to be the term compact_convergence_topology_metric_C X Tx Y dY.
Set Sset to be the term {f ∈ CXY|K ⊆ preimage_of X f U}.
We will prove Sset ∈ Tcc.
Set Scc to be the term (compact_convergence_subbasis_metric X Tx Y dY) ∪ {CXY}.
Set Bcc to be the term basis_of_subbasis CXY Scc.
We prove the intermediate claim HScc: subbasis_on CXY Scc.
We will prove Scc ⊆ 𝒫 CXY ∧ ⋃ Scc = CXY.
Apply andI to the current goal.
Let s be given.
Assume Hs: s ∈ Scc.
We will prove s ∈ 𝒫 CXY.
Apply (binunionE' (compact_convergence_subbasis_metric X Tx Y dY) {CXY} s (s ∈ 𝒫 CXY)) to the current goal.
Assume Hsm: s ∈ compact_convergence_subbasis_metric X Tx Y dY.
An exact proof term for the current goal is (SepE1 (𝒫 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).
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).
An exact proof term for the current goal is (PowerI CXY CXY (Subq_ref CXY)).
An exact proof term for the current goal is Hs.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ Scc.
We will prove f ∈ CXY.
Apply (UnionE_impred Scc f Hf (f ∈ CXY)) to the current goal.
Let V be given.
Assume HfV: f ∈ V.
Assume HV: V ∈ Scc.
Apply (binunionE' (compact_convergence_subbasis_metric X Tx Y dY) {CXY} V (f ∈ CXY)) to the current goal.
Assume HVm: V ∈ compact_convergence_subbasis_metric X Tx Y dY.
We prove the intermediate claim HVpow: V ∈ 𝒫 CXY.
An exact proof term for the current goal is (SepE1 (𝒫 CXY) (λS0 : set ⇒ ∃C f0 eps : set, compact_space C (subspace_topology X Tx C) ∧ C ⊆ X ∧ f0 ∈ CXY ∧ eps ∈ R ∧ Rlt 0 eps ∧ S0 = {g ∈ CXY|∀x : set, x ∈ C → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps}) V HVm).
An exact proof term for the current goal is (PowerE CXY V HVpow f HfV).
Assume HVC: V ∈ {CXY}.
We prove the intermediate claim HVeq: V = CXY.
An exact proof term for the current goal is (SingE CXY V HVC).
rewrite the current goal using HVeq (from right to left).
An exact proof term for the current goal is HfV.
An exact proof term for the current goal is HV.
Let f be given.
Assume Hf: f ∈ CXY.
We prove the intermediate claim HCinS: CXY ∈ Scc.
An exact proof term for the current goal is (binunionI2 (compact_convergence_subbasis_metric X Tx Y dY) {CXY} CXY (SingI CXY)).
An exact proof term for the current goal is (UnionI Scc f CXY Hf HCinS).
We prove the intermediate claim HBasis: basis_on CXY Bcc.
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis CXY Scc HScc).
We prove the intermediate claim HTccdef: Tcc = generated_topology_from_subbasis CXY Scc.
Use reflexivity.
We prove the intermediate claim HTccB: Tcc = generated_topology CXY Bcc.
rewrite the current goal using HTccdef (from left to right).
Use reflexivity.
rewrite the current goal using HTccB (from left to right).
rewrite the current goal using (lemma_generated_topology_characterization CXY Bcc HBasis) (from left to right).
We will prove Sset ∈ {U0 ∈ 𝒫 CXY|∀f0 ∈ U0, ∃b ∈ Bcc, f0 ∈ b ∧ b ⊆ U0}.
Apply SepI to the current goal.
Apply PowerI to the current goal.
Let f0 be given.
Assume Hf0: f0 ∈ Sset.
An exact proof term for the current goal is (SepE1 CXY (λf1 : set ⇒ K ⊆ preimage_of X f1 U) f0 Hf0).
Let f0 be given.
Assume Hf0: f0 ∈ Sset.
We will prove ∃b ∈ Bcc, f0 ∈ b ∧ b ⊆ Sset.
We prove the intermediate claim Hf0C: f0 ∈ CXY.
An exact proof term for the current goal is (SepE1 CXY (λf1 : set ⇒ K ⊆ preimage_of X f1 U) f0 Hf0).
We prove the intermediate claim HKpre: K ⊆ preimage_of X f0 U.
An exact proof term for the current goal is (SepE2 CXY (λf1 : set ⇒ K ⊆ preimage_of X f1 U) f0 Hf0).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ {g ∈ CXY|∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc N))} ⊆ Sset.
Apply (xm (K = Empty)) to the current goal.
Assume HKempty: K = Empty.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Let g be given.
Assume Hg: g ∈ {g ∈ CXY|∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc 0))}.
We will prove g ∈ Sset.
Apply (SepI CXY (λf1 : set ⇒ K ⊆ preimage_of X f1 U) g) to the current goal.
An exact proof term for the current goal is (SepE1 CXY (λg0 : set ⇒ ∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) (eps_ (ordsucc 0))) g Hg).
rewrite the current goal using HKempty (from left to right).
An exact proof term for the current goal is (Subq_Empty (preimage_of X g U)).
Assume HKne: K ≠ Empty.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).
We prove the intermediate claim HUopen: open_in Y Ty U.
An exact proof term for the current goal is (open_inI Y Ty U HTy HU).
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) (λg0 : set ⇒ continuous_map X Tx Y Ty g0) f0 Hf0C).
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) (λg0 : set ⇒ continuous_map X Tx Y Ty g0) f0 Hf0C).
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).
Set UFam to be the term {V ∈ Tx|∃x0 N0 : set, x0 ∈ K ∧ N0 ∈ ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))) ∧ open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U}.
We prove the intermediate claim HUFamSubTx: UFam ⊆ Tx.
Let V be given.
Assume HV: V ∈ UFam.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ ∃x0 N0 : set, x0 ∈ K ∧ N0 ∈ ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))) ∧ open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U) V HV).
We prove the intermediate claim HKcov: K ⊆ ⋃ UFam.
Let x be given.
Assume HxK: x ∈ K.
We will prove x ∈ ⋃ UFam.
We prove the intermediate claim HxPre: x ∈ preimage_of X f0 U.
An exact proof term for the current goal is (HKpre x HxK).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f0 x0 ∈ U) x HxPre).
We prove the intermediate claim HfxU: apply_fun f0 x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f0 x0 ∈ U) x HxPre).
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 HexNx: ∃N0 : set, N0 ∈ ω ∧ open_ball Y dY (apply_fun f0 x) (eps_ N0) ⊆ U.
An exact proof term for the current goal is (open_in_metric_topology_has_eps_ball_sub Y dY U (apply_fun f0 x) HdY HUopen HfxU).
Apply HexNx to the current goal.
Let N0 be given.
Assume HN0pack.
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (open_ball Y dY (apply_fun f0 x) (eps_ N0) ⊆ U) HN0pack).
We prove the intermediate claim HballSubU: open_ball Y dY (apply_fun f0 x) (eps_ N0) ⊆ U.
An exact proof term for the current goal is (andER (N0 ∈ ω) (open_ball Y dY (apply_fun f0 x) (eps_ N0) ⊆ U) HN0pack).
Set V0 to be the term preimage_of X f0 (open_ball Y dY (apply_fun f0 x) (eps_ (ordsucc N0))).
We prove the intermediate claim HsuccOmega: ordsucc N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0omega).
We prove the intermediate claim HepsR: eps_ (ordsucc N0) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc N0)) (SNo_eps_SNoS_omega (ordsucc N0) HsuccOmega)).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ (ordsucc N0)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc N0)) real_0 HepsR (SNo_eps_pos (ordsucc N0) HsuccOmega)).
We prove the intermediate claim HballTop: open_ball Y dY (apply_fun f0 x) (eps_ (ordsucc N0)) ∈ Ty.
An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun f0 x) (eps_ (ordsucc N0)) HdY HfxY Hepspos).
We prove the intermediate claim HV0Tx: V0 ∈ 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) (eps_ (ordsucc N0))) HballTop).
We prove the intermediate claim HxInBall: apply_fun f0 x ∈ open_ball Y dY (apply_fun f0 x) (eps_ (ordsucc N0)).
Apply (open_ballI Y dY (apply_fun f0 x) (eps_ (ordsucc N0)) (apply_fun f0 x) HfxY) to the current goal.
rewrite the current goal using (metric_on_diag_zero Y dY (apply_fun f0 x) HdY HfxY) (from left to right).
An exact proof term for the current goal is Hepspos.
We prove the intermediate claim HxInV0: x ∈ V0.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f0 x0 ∈ open_ball Y dY (apply_fun f0 x) (eps_ (ordsucc N0))) x HxX HxInBall).
We prove the intermediate claim HV0UFam: V0 ∈ UFam.
Apply (SepI Tx (λV : set ⇒ ∃x0 N1 : set, x0 ∈ K ∧ N1 ∈ ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N1))) ∧ open_ball Y dY (apply_fun f0 x0) (eps_ N1) ⊆ U) V0 HV0Tx) to the current goal.
We use x to witness the existential quantifier.
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HxK.
An exact proof term for the current goal is HN0omega.
Use reflexivity.
An exact proof term for the current goal is HballSubU.
An exact proof term for the current goal is (UnionI UFam x V0 HxInV0 HV0UFam).
We prove the intermediate claim HKcover_prop: ∀Fam : set, (Fam ⊆ Tx ∧ K ⊆ ⋃ Fam) → has_finite_subcover K Tx Fam.
An exact proof term for the current goal is (iffEL (compact_space K (subspace_topology X Tx K)) (∀Fam : set, (Fam ⊆ Tx ∧ K ⊆ ⋃ Fam) → has_finite_subcover K Tx Fam) (compact_subspace_via_ambient_covers X Tx K HTx HKsubX) HK).
We prove the intermediate claim Hfin: has_finite_subcover K Tx UFam.
An exact proof term for the current goal is (HKcover_prop UFam (andI (UFam ⊆ Tx) (K ⊆ ⋃ UFam) HUFamSubTx HKcov)).
Apply Hfin to the current goal.
Let G be given.
Assume HGtriple: G ⊆ UFam ∧ finite G ∧ K ⊆ ⋃ 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) (K ⊆ ⋃ 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) (K ⊆ ⋃ G) HGtriple)).
We prove the intermediate claim HKcovG: K ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ UFam ∧ finite G) (K ⊆ ⋃ G) HGtriple).
Set pickP to be the term λV : set ⇒ Eps_i (λp : set ⇒ p ∈ setprod K ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 (p 0)) (eps_ (ordsucc (p 1)))) ∧ open_ball Y dY (apply_fun f0 (p 0)) (eps_ (p 1)) ⊆ U).
We prove the intermediate claim HpickP: ∀V : set, V ∈ UFam → pickP V ∈ setprod K ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V) 0)) (eps_ (ordsucc ((pickP V) 1)))) ∧ open_ball Y dY (apply_fun f0 ((pickP V) 0)) (eps_ ((pickP V) 1)) ⊆ U.
Let V be given.
Assume HV: V ∈ UFam.
We prove the intermediate claim HVprop: ∃x0 N0 : set, x0 ∈ K ∧ N0 ∈ ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))) ∧ open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U.
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ ∃x0 N0 : set, x0 ∈ K ∧ N0 ∈ ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))) ∧ open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U) V HV).
Apply HVprop to the current goal.
Let x0 be given.
Assume HN0ex: ∃N0 : set, x0 ∈ K ∧ N0 ∈ ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))) ∧ open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U.
Apply HN0ex to the current goal.
Let N0 be given.
Assume Hxn: x0 ∈ K ∧ N0 ∈ ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))) ∧ open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U.
Set p0 to be the term (x0,N0).
We prove the intermediate claim Hp0In: p0 ∈ setprod K ω.
We prove the intermediate claim HABC: (x0 ∈ K ∧ N0 ∈ ω) ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))).
An exact proof term for the current goal is (andEL ((x0 ∈ K ∧ N0 ∈ ω) ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0)))) (open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U) Hxn).
We prove the intermediate claim HAB: x0 ∈ K ∧ N0 ∈ ω.
An exact proof term for the current goal is (andEL (x0 ∈ K ∧ N0 ∈ ω) (V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0)))) HABC).
We prove the intermediate claim Hx0K: x0 ∈ K.
An exact proof term for the current goal is (andEL (x0 ∈ K) (N0 ∈ ω) HAB).
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (andER (x0 ∈ K) (N0 ∈ ω) HAB).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K ω x0 N0 Hx0K HN0omega).
We prove the intermediate claim Hpack: p0 ∈ setprod K ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 (p0 0)) (eps_ (ordsucc (p0 1)))) ∧ open_ball Y dY (apply_fun f0 (p0 0)) (eps_ (p0 1)) ⊆ U.
We prove the intermediate claim Hp00: p0 0 = x0.
rewrite the current goal using (tuple_pair x0 N0) (from right to left).
An exact proof term for the current goal is (pair_ap_0 x0 N0).
We prove the intermediate claim Hp01: p0 1 = N0.
rewrite the current goal using (tuple_pair x0 N0) (from right to left).
An exact proof term for the current goal is (pair_ap_1 x0 N0).
We prove the intermediate claim HABC: (x0 ∈ K ∧ N0 ∈ ω) ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))).
An exact proof term for the current goal is (andEL ((x0 ∈ K ∧ N0 ∈ ω) ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0)))) (open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U) Hxn).
We prove the intermediate claim HVeq: V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0))).
An exact proof term for the current goal is (andER (x0 ∈ K ∧ N0 ∈ ω) (V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0)))) HABC).
We prove the intermediate claim HballSub: open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U.
An exact proof term for the current goal is (andER ((x0 ∈ K ∧ N0 ∈ ω) ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc N0)))) (open_ball Y dY (apply_fun f0 x0) (eps_ N0) ⊆ U) Hxn).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hp0In.
rewrite the current goal using Hp00 (from left to right).
rewrite the current goal using Hp01 (from left to right).
An exact proof term for the current goal is HVeq.
rewrite the current goal using Hp00 (from left to right).
rewrite the current goal using Hp01 (from left to right).
An exact proof term for the current goal is HballSub.
An exact proof term for the current goal is (Eps_i_ax (λp : set ⇒ p ∈ setprod K ω ∧ V = preimage_of X f0 (open_ball Y dY (apply_fun f0 (p 0)) (eps_ (ordsucc (p 1)))) ∧ open_ball Y dY (apply_fun f0 (p 0)) (eps_ (p 1)) ⊆ U) p0 Hpack).
Set Nidx to be the term {(pickP V) 1|V ∈ G}.
We prove the intermediate claim HNidxFin: finite Nidx.
An exact proof term for the current goal is (Repl_finite (λV0 : set ⇒ (pickP V0) 1) G HGfin).
We prove the intermediate claim HNidxSubOmega: Nidx ⊆ ω.
Let n be given.
Assume Hn: n ∈ Nidx.
Apply (ReplE_impred G (λV0 : set ⇒ (pickP V0) 1) n Hn) to the current goal.
Let V0 be given.
Assume HV0G: V0 ∈ G.
Assume Hneq: n = (pickP V0) 1.
We prove the intermediate claim HV0UFam: V0 ∈ UFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
We prove the intermediate claim HpPack: pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1)))) ∧ open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ ((pickP V0) 1)) ⊆ U.
An exact proof term for the current goal is (HpickP V0 HV0UFam).
We prove the intermediate claim HpAB: pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1)))).
An exact proof term for the current goal is (andEL (pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1))))) (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ ((pickP V0) 1)) ⊆ U) HpPack).
We prove the intermediate claim HpIn: pickP V0 ∈ setprod K ω.
An exact proof term for the current goal is (andEL (pickP V0 ∈ setprod K ω) (V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1))))) HpAB).
We prove the intermediate claim HN0: ((pickP V0) 1) ∈ ω.
An exact proof term for the current goal is (ap1_Sigma K (λ_ : set ⇒ ω) (pickP V0) HpIn).
rewrite the current goal using Hneq (from left to right).
An exact proof term for the current goal is HN0.
We prove the intermediate claim HNidxNe: Nidx ≠ Empty.
We prove the intermediate claim Hexx: ∃x0 : set, x0 ∈ K.
An exact proof term for the current goal is (nonempty_has_element K HKne).
Apply Hexx to the current goal.
Let x0 be given.
Assume Hx0K: x0 ∈ K.
We prove the intermediate claim Hx0U: x0 ∈ ⋃ G.
An exact proof term for the current goal is (HKcovG x0 Hx0K).
Apply (UnionE_impred G x0 Hx0U (Nidx ≠ Empty)) to the current goal.
Let V0 be given.
Assume Hx0V0: x0 ∈ V0.
Assume HV0G: V0 ∈ G.
Set n0 to be the term (pickP V0) 1.
We prove the intermediate claim Hn0Nidx: n0 ∈ Nidx.
An exact proof term for the current goal is (ReplI G (λV1 : set ⇒ (pickP V1) 1) V0 HV0G).
An exact proof term for the current goal is (elem_implies_nonempty Nidx n0 Hn0Nidx).
We prove the intermediate claim Hmax: ∃Nmax : set, Nmax ∈ Nidx ∧ ∀n : set, n ∈ Nidx → n ⊆ Nmax.
An exact proof term for the current goal is (finite_nonempty_subset_of_ordinal_has_max ω Nidx omega_ordinal HNidxFin HNidxSubOmega HNidxNe).
Apply Hmax to the current goal.
Let Nmax be given.
Assume HNmaxPack.
We prove the intermediate claim HNmaxIn: Nmax ∈ Nidx.
An exact proof term for the current goal is (andEL (Nmax ∈ Nidx) (∀n : set, n ∈ Nidx → n ⊆ Nmax) HNmaxPack).
We prove the intermediate claim HNmaxMax: ∀n : set, n ∈ Nidx → n ⊆ Nmax.
An exact proof term for the current goal is (andER (Nmax ∈ Nidx) (∀n : set, n ∈ Nidx → n ⊆ Nmax) HNmaxPack).
We prove the intermediate claim HNmaxOmega: Nmax ∈ ω.
An exact proof term for the current goal is (HNidxSubOmega Nmax HNmaxIn).
We use Nmax to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNmaxOmega.
Let g be given.
Assume Hg: g ∈ {g ∈ CXY|∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc Nmax))}.
We will prove g ∈ Sset.
We prove the intermediate claim HgC: g ∈ CXY.
An exact proof term for the current goal is (SepE1 CXY (λg0 : set ⇒ ∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) (eps_ (ordsucc Nmax))) g Hg).
We prove the intermediate claim HgFS: g ∈ function_space X Y.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λg0 : set ⇒ continuous_map X Tx Y Ty g0) g HgC).
We prove the intermediate claim Hgfun: function_on g X Y.
An exact proof term for the current goal is (function_on_of_function_space g X Y HgFS).
Apply (SepI CXY (λf1 : set ⇒ K ⊆ preimage_of X f1 U) g HgC) to the current goal.
Let x be given.
Assume HxK: x ∈ K.
We will prove x ∈ preimage_of X g U.
We prove the intermediate claim HxU: x ∈ ⋃ G.
An exact proof term for the current goal is (HKcovG x HxK).
Apply (UnionE_impred G x HxU (x ∈ preimage_of X g U)) to the current goal.
Let V0 be given.
Assume HxV0: x ∈ V0.
Assume HV0G: V0 ∈ G.
We prove the intermediate claim HV0UFam: V0 ∈ UFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
We prove the intermediate claim HpPack: pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1)))) ∧ open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ ((pickP V0) 1)) ⊆ U.
An exact proof term for the current goal is (HpickP V0 HV0UFam).
We prove the intermediate claim HpIn: pickP V0 ∈ setprod K ω.
We prove the intermediate claim HpAB: pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1)))).
An exact proof term for the current goal is (andEL (pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1))))) (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ ((pickP V0) 1)) ⊆ U) HpPack).
An exact proof term for the current goal is (andEL (pickP V0 ∈ setprod K ω) (V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 ((pickP V0) 0)) (eps_ (ordsucc ((pickP V0) 1))))) HpAB).
Set x0 to be the term (pickP V0) 0.
Set n0 to be the term (pickP V0) 1.
We prove the intermediate claim Hx0K: x0 ∈ K.
An exact proof term for the current goal is (ap0_Sigma K (λ_ : set ⇒ ω) (pickP V0) HpIn).
We prove the intermediate claim Hn0Omega: n0 ∈ ω.
An exact proof term for the current goal is (ap1_Sigma K (λ_ : set ⇒ ω) (pickP V0) HpIn).
We prove the intermediate claim Hn0InIdx: n0 ∈ Nidx.
An exact proof term for the current goal is (ReplI G (λV1 : set ⇒ (pickP V1) 1) V0 HV0G).
We prove the intermediate claim Hn0SubMax: n0 ⊆ Nmax.
An exact proof term for the current goal is (HNmaxMax n0 Hn0InIdx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HKsubX x HxK).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (HKsubX x0 Hx0K).
We prove the intermediate claim Hf0xY: apply_fun f0 x ∈ Y.
An exact proof term for the current goal is (Hf0fun x HxX).
We prove the intermediate claim Hf0x0Y: apply_fun f0 x0 ∈ Y.
An exact proof term for the current goal is (Hf0fun x0 Hx0X).
We prove the intermediate claim HgxY: apply_fun g x ∈ Y.
An exact proof term for the current goal is (Hgfun x HxX).
We prove the intermediate claim HV0eq: V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0))).
We prove the intermediate claim HpAB: pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0))).
An exact proof term for the current goal is (andEL (pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0)))) (open_ball Y dY (apply_fun f0 x0) (eps_ n0) ⊆ U) HpPack).
An exact proof term for the current goal is (andER (pickP V0 ∈ setprod K ω) (V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0)))) HpAB).
We prove the intermediate claim HxPre: x ∈ preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0))).
rewrite the current goal using HV0eq (from right to left).
An exact proof term for the current goal is HxV0.
We prove the intermediate claim Hf0xBall: apply_fun f0 x ∈ open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0)).
An exact proof term for the current goal is (SepE2 X (λx1 : set ⇒ apply_fun f0 x1 ∈ open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0))) x HxPre).
We prove the intermediate claim Hdist_f0: Rlt (apply_fun dY (apply_fun f0 x0,apply_fun f0 x)) (eps_ (ordsucc n0)).
An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun f0 x0) (eps_ (ordsucc n0)) (apply_fun f0 x) Hf0xBall).
We prove the intermediate claim Hdist_gf0: Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc Nmax)).
An exact proof term for the current goal is (SepE2 CXY (λg0 : set ⇒ ∀x1 : set, x1 ∈ K → Rlt (apply_fun dY (apply_fun g0 x1,apply_fun f0 x1)) (eps_ (ordsucc Nmax))) g Hg x HxK).
We prove the intermediate claim HsuccMaxOmega: ordsucc Nmax ∈ ω.
An exact proof term for the current goal is (omega_ordsucc Nmax HNmaxOmega).
We prove the intermediate claim Hsuccn0Omega: ordsucc n0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n0 Hn0Omega).
We prove the intermediate claim HepsMaxR: eps_ (ordsucc Nmax) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc Nmax)) (SNo_eps_SNoS_omega (ordsucc Nmax) HsuccMaxOmega)).
We prove the intermediate claim Hepsn0R: eps_ (ordsucc n0) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc n0)) (SNo_eps_SNoS_omega (ordsucc n0) Hsuccn0Omega)).
We prove the intermediate claim Hdist_f0g: Rlt (apply_fun dY (apply_fun f0 x,apply_fun g x)) (eps_ (ordsucc n0)).
We prove the intermediate claim Hsym: apply_fun dY (apply_fun f0 x,apply_fun g x) = apply_fun dY (apply_fun g x,apply_fun f0 x).
An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f0 x) (apply_fun g x) HdY Hf0xY HgxY).
rewrite the current goal using Hsym (from left to right).
Apply (xm (n0 = Nmax)) to the current goal.
Assume Heq: n0 = Nmax.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hdist_gf0.
Assume Hneq: n0 ≠ Nmax.
We prove the intermediate claim Hn0Ord: ordinal n0.
An exact proof term for the current goal is (nat_p_ordinal n0 (omega_nat_p n0 Hn0Omega)).
We prove the intermediate claim HNmaxOrd: ordinal Nmax.
An exact proof term for the current goal is (nat_p_ordinal Nmax (omega_nat_p Nmax HNmaxOmega)).
We prove the intermediate claim Hcase: n0 ∈ Nmax ∨ Nmax ⊆ n0.
An exact proof term for the current goal is (ordinal_In_Or_Subq n0 Nmax Hn0Ord HNmaxOrd).
We prove the intermediate claim Hn0inMax: n0 ∈ Nmax.
Apply (Hcase (n0 ∈ Nmax)) to the current goal.
Assume H0: n0 ∈ Nmax.
An exact proof term for the current goal is H0.
Assume H0: Nmax ⊆ n0.
Apply FalseE to the current goal.
Apply Hneq to the current goal.
We prove the intermediate claim HeqSub: n0 = Nmax.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ n0.
An exact proof term for the current goal is (Hn0SubMax z Hz).
Let z be given.
Assume Hz: z ∈ Nmax.
An exact proof term for the current goal is (H0 z Hz).
An exact proof term for the current goal is HeqSub.
We prove the intermediate claim HordSuccMax: ordinal (ordsucc Nmax).
An exact proof term for the current goal is (ordinal_ordsucc Nmax HNmaxOrd).
We prove the intermediate claim Hsuccn0In: ordsucc n0 ∈ ordsucc Nmax.
We prove the intermediate claim HsuccSub: ordsucc n0 ⊆ Nmax.
An exact proof term for the current goal is (ordinal_ordsucc_In_Subq Nmax HNmaxOrd n0 Hn0inMax).
We prove the intermediate claim HsuccOrd: ordinal (ordsucc n0).
An exact proof term for the current goal is (ordinal_ordsucc n0 Hn0Ord).
We prove the intermediate claim Hcase2: ordsucc n0 ∈ Nmax ∨ Nmax ⊆ ordsucc n0.
An exact proof term for the current goal is (ordinal_In_Or_Subq (ordsucc n0) Nmax HsuccOrd HNmaxOrd).
Apply (Hcase2 (ordsucc n0 ∈ ordsucc Nmax)) to the current goal.
Assume H1: ordsucc n0 ∈ Nmax.
An exact proof term for the current goal is (ordsuccI1 Nmax (ordsucc n0) H1).
Assume H1: Nmax ⊆ ordsucc n0.
We prove the intermediate claim Heq2: ordsucc n0 = Nmax.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ ordsucc n0.
An exact proof term for the current goal is (HsuccSub z Hz).
Let z be given.
Assume Hz: z ∈ Nmax.
An exact proof term for the current goal is (H1 z Hz).
rewrite the current goal using Heq2 (from left to right).
An exact proof term for the current goal is (ordsuccI2 Nmax).
We prove the intermediate claim HepsLtS: eps_ (ordsucc Nmax) < eps_ (ordsucc n0).
An exact proof term for the current goal is (SNo_eps_decr (ordsucc Nmax) HsuccMaxOmega (ordsucc n0) Hsuccn0In).
We prove the intermediate claim HepsLt: Rlt (eps_ (ordsucc Nmax)) (eps_ (ordsucc n0)).
An exact proof term for the current goal is (RltI (eps_ (ordsucc Nmax)) (eps_ (ordsucc n0)) HepsMaxR Hepsn0R HepsLtS).
An exact proof term for the current goal is (Rlt_tra (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc Nmax)) (eps_ (ordsucc n0)) Hdist_gf0 HepsLt).
We prove the intermediate claim Htri: Rle (apply_fun dY (apply_fun f0 x0,apply_fun g x)) (add_SNo (apply_fun dY (apply_fun f0 x0,apply_fun f0 x)) (apply_fun dY (apply_fun f0 x,apply_fun g x))).
An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun f0 x0) (apply_fun f0 x) (apply_fun g x) HdY Hf0x0Y Hf0xY HgxY).
We prove the intermediate claim HsumLt: Rlt (add_SNo (apply_fun dY (apply_fun f0 x0,apply_fun f0 x)) (apply_fun dY (apply_fun f0 x,apply_fun g x))) (add_SNo (eps_ (ordsucc n0)) (eps_ (ordsucc n0))).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun dY (apply_fun f0 x0,apply_fun f0 x)) (eps_ (ordsucc n0)) (apply_fun dY (apply_fun f0 x,apply_fun g x)) (eps_ (ordsucc n0)) Hdist_f0 Hdist_f0g).
We prove the intermediate claim Hn0Nat: nat_p n0.
An exact proof term for the current goal is (omega_nat_p n0 Hn0Omega).
We prove the intermediate claim HepsHalf: add_SNo (eps_ (ordsucc n0)) (eps_ (ordsucc n0)) = eps_ n0.
An exact proof term for the current goal is (eps_ordsucc_half_add n0 Hn0Nat).
We prove the intermediate claim HsumLt2: Rlt (add_SNo (apply_fun dY (apply_fun f0 x0,apply_fun f0 x)) (apply_fun dY (apply_fun f0 x,apply_fun g x))) (eps_ n0).
rewrite the current goal using HepsHalf (from right to left).
An exact proof term for the current goal is HsumLt.
We prove the intermediate claim Hdist_cg: Rlt (apply_fun dY (apply_fun f0 x0,apply_fun g x)) (eps_ n0).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun dY (apply_fun f0 x0,apply_fun g x)) (add_SNo (apply_fun dY (apply_fun f0 x0,apply_fun f0 x)) (apply_fun dY (apply_fun f0 x,apply_fun g x))) (eps_ n0) Htri HsumLt2).
We prove the intermediate claim HballSubU: open_ball Y dY (apply_fun f0 x0) (eps_ n0) ⊆ U.
An exact proof term for the current goal is (andER (pickP V0 ∈ setprod K ω ∧ V0 = preimage_of X f0 (open_ball Y dY (apply_fun f0 x0) (eps_ (ordsucc n0)))) (open_ball Y dY (apply_fun f0 x0) (eps_ n0) ⊆ U) HpPack).
We prove the intermediate claim HgxBall: apply_fun g x ∈ open_ball Y dY (apply_fun f0 x0) (eps_ n0).
An exact proof term for the current goal is (open_ballI Y dY (apply_fun f0 x0) (eps_ n0) (apply_fun g x) HgxY Hdist_cg).
We prove the intermediate claim HgxU: apply_fun g x ∈ U.
An exact proof term for the current goal is (HballSubU (apply_fun g x) HgxBall).
An exact proof term for the current goal is (SepI X (λx1 : set ⇒ apply_fun g x1 ∈ U) x HxX HgxU).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) ({g ∈ CXY|∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc N))} ⊆ Sset) HNpack).
We prove the intermediate claim Hsub: {g ∈ CXY|∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc N))} ⊆ Sset.
An exact proof term for the current goal is (andER (N ∈ ω) ({g ∈ CXY|∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc N))} ⊆ Sset) HNpack).
Set B0 to be the term {g ∈ CXY|∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) (eps_ (ordsucc N))}.
We prove the intermediate claim HB0inSub: B0 ∈ compact_convergence_subbasis_metric X Tx Y dY.
We prove the intermediate claim HB0pow: B0 ∈ 𝒫 CXY.
Apply PowerI to the current goal.
Let g be given.
Assume Hg: g ∈ B0.
An exact proof term for the current goal is (SepE1 CXY (λg0 : set ⇒ ∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) (eps_ (ordsucc N))) g Hg).
We prove the intermediate claim Hdef: compact_convergence_subbasis_metric X Tx Y dY = {S ∈ 𝒫 CXY|∃C f eps : set, compact_space C (subspace_topology X Tx C) ∧ C ⊆ X ∧ f ∈ CXY ∧ eps ∈ R ∧ Rlt 0 eps ∧ S = {g ∈ CXY|∀x : set, x ∈ C → Rlt (apply_fun dY (apply_fun g x,apply_fun f x)) eps}}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (SepI (𝒫 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}) B0 HB0pow) to the current goal.
We use K to witness the existential quantifier.
We use f0 to witness the existential quantifier.
We use (eps_ (ordsucc N)) to witness the existential quantifier.
We prove the intermediate claim HsuccOmega: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HepsR: eps_ (ordsucc N) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc N)) (SNo_eps_SNoS_omega (ordsucc N) HsuccOmega)).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ (ordsucc N)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc N)) real_0 HepsR (SNo_eps_pos (ordsucc N) HsuccOmega)).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HK.
An exact proof term for the current goal is HKsubX.
An exact proof term for the current goal is Hf0C.
An exact proof term for the current goal is HepsR.
An exact proof term for the current goal is Hepspos.
Use reflexivity.
We prove the intermediate claim HB0inScc: B0 ∈ Scc.
An exact proof term for the current goal is (binunionI1 (compact_convergence_subbasis_metric X Tx Y dY) {CXY} B0 HB0inSub).
We prove the intermediate claim HB0ne: B0 ≠ Empty.
We prove the intermediate claim Hf0in: f0 ∈ B0.
Apply (SepI CXY (λg0 : set ⇒ ∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) (eps_ (ordsucc N))) f0 Hf0C) to the current goal.
Let x be given.
Assume HxK: x ∈ K.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HKsubX x HxK).
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) (λg0 : set ⇒ continuous_map X Tx Y Ty g0) f0 Hf0C).
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 HfxY: apply_fun f0 x ∈ Y.
An exact proof term for the current goal is (Hf0fun x HxX).
We prove the intermediate claim HsuccOmega: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HepsR: eps_ (ordsucc N) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc N)) (SNo_eps_SNoS_omega (ordsucc N) HsuccOmega)).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ (ordsucc N)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc N)) real_0 HepsR (SNo_eps_pos (ordsucc N) HsuccOmega)).
rewrite the current goal using (metric_on_diag_zero Y dY (apply_fun f0 x) HdY HfxY) (from left to right).
An exact proof term for the current goal is Hepspos.
Assume HB0eq: B0 = Empty.
We prove the intermediate claim Hbad: f0 ∈ Empty.
rewrite the current goal using HB0eq (from right to left).
An exact proof term for the current goal is Hf0in.
An exact proof term for the current goal is (EmptyE f0 Hbad).
We prove the intermediate claim HB0basis: B0 ∈ Bcc.
An exact proof term for the current goal is (subbasis_elem_in_basis CXY Scc B0 HScc HB0inScc HB0ne).
We use B0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HB0basis.
Apply andI to the current goal.
Apply (SepI CXY (λg0 : set ⇒ ∀x : set, x ∈ K → Rlt (apply_fun dY (apply_fun g0 x,apply_fun f0 x)) (eps_ (ordsucc N))) f0 Hf0C) to the current goal.
Let x be given.
Assume HxK: x ∈ K.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HKsubX x HxK).
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) (λg0 : set ⇒ continuous_map X Tx Y Ty g0) f0 Hf0C).
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 HfxY: apply_fun f0 x ∈ Y.
An exact proof term for the current goal is (Hf0fun x HxX).
We prove the intermediate claim HsuccOmega: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HepsR: eps_ (ordsucc N) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc N)) (SNo_eps_SNoS_omega (ordsucc N) HsuccOmega)).
We prove the intermediate claim Hepspos: Rlt 0 (eps_ (ordsucc N)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc N)) real_0 HepsR (SNo_eps_pos (ordsucc N) HsuccOmega)).
rewrite the current goal using (metric_on_diag_zero Y dY (apply_fun f0 x) HdY HfxY) (from left to right).
An exact proof term for the current goal is Hepspos.
An exact proof term for the current goal is Hsub.
∎