Let X, Y, d and fn be given.
Assume Hcomp: complete_metric_space Y d.
Assume Hfn: function_on fn ω (function_space X Y).
Assume Huc: uniform_cauchy_metric X Y d fn.
We prove the intermediate claim HmY: metric_on Y d.
An exact proof term for the current goal is (andEL (metric_on Y d) (∀seq : set, sequence_on seq Y → cauchy_sequence Y d seq → ∃x : set, converges_to Y (metric_topology Y d) seq x) Hcomp).
We prove the intermediate claim Hcomplete: ∀seq : set, sequence_on seq Y → cauchy_sequence Y d seq → ∃x : set, converges_to Y (metric_topology Y d) seq x.
An exact proof term for the current goal is (andER (metric_on Y d) (∀seq : set, sequence_on seq Y → cauchy_sequence Y d seq → ∃x : set, converges_to Y (metric_topology Y d) seq x) Hcomp).
Set f to be the term graph X (λx : set ⇒ Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x)) y)).
We use f to witness the existential quantifier.
Apply andI to the current goal.
We will prove function_on f X Y.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun f x ∈ Y.
We prove the intermediate claim Hfdef: f = graph X (λx0 : set ⇒ Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x0)) y)).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq f X (λx0 : set ⇒ Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) (graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x0)) y)) x Hfdef HxX) (from left to right).
Set seqx to be the term graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x).
We prove the intermediate claim Hseqx: sequence_on seqx Y.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun seqx n ∈ Y.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x) n Hseqxdef HnO) (from left to right).
We prove the intermediate claim HfnnFS: apply_fun fn n ∈ function_space X Y.
An exact proof term for the current goal is (Hfn n HnO).
We prove the intermediate claim Hfnn_on: function_on (apply_fun fn n) X Y.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λf0 : set ⇒ function_on f0 X Y) (apply_fun fn n) HfnnFS).
An exact proof term for the current goal is (Hfnn_on x HxX).
We prove the intermediate claim Hcaux: cauchy_sequence Y d seqx.
We prove the intermediate claim Hdef: cauchy_sequence Y d seqx = (metric_on Y d ∧ sequence_on seqx Y ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seqx m,apply_fun seqx n)) eps).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HmY.
An exact proof term for the current goal is Hseqx.
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim HNbig: ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m) x0,apply_fun (apply_fun fn n) x0)) eps.
An exact proof term for the current goal is (Huc eps HepsR HepsPos).
Apply HNbig to the current goal.
Let N be given.
Assume HNpair.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m) x0,apply_fun (apply_fun fn n) x0)) eps) HNpair).
Let m and n be given.
Assume HmO: m ∈ ω.
Assume HnO: n ∈ ω.
Assume HNm: N ⊆ m.
Assume HNn: N ⊆ n.
We will prove Rlt (apply_fun d (apply_fun seqx m,apply_fun seqx n)) eps.
We prove the intermediate claim Htail: ∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m0) x0,apply_fun (apply_fun fn n0) x0)) eps.
An exact proof term for the current goal is (andER (N ∈ ω) (∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m0) x0,apply_fun (apply_fun fn n0) x0)) eps) HNpair).
We prove the intermediate claim Hseqm: apply_fun seqx m = apply_fun (apply_fun fn m) x.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x) m Hseqxdef HmO) (from left to right).
Use reflexivity.
We prove the intermediate claim Hseqn: apply_fun seqx n = apply_fun (apply_fun fn n) x.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x) n Hseqxdef HnO) (from left to right).
Use reflexivity.
rewrite the current goal using Hseqm (from left to right).
rewrite the current goal using Hseqn (from left to right).
An exact proof term for the current goal is (Htail m n HmO HnO HNm HNn x HxX).
We prove the intermediate claim Hexlim: ∃y : set, converges_to Y (metric_topology Y d) seqx y.
Apply (Hcomplete seqx Hseqx Hcaux) to the current goal.
We prove the intermediate claim HlimChosen: converges_to Y (metric_topology Y d) seqx (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)).
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y) Hexlim).
We prove the intermediate claim Hlim12: (topology_on Y (metric_topology Y d) ∧ sequence_on seqx Y) ∧ (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Y.
An exact proof term for the current goal is (andEL ((topology_on Y (metric_topology Y d) ∧ sequence_on seqx Y) ∧ (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Y) (∀U : set, U ∈ metric_topology Y d → (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U) HlimChosen).
An exact proof term for the current goal is (andER (topology_on Y (metric_topology Y d) ∧ sequence_on seqx Y) ((Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Y) Hlim12).
We will prove uniform_limit_metric X Y d fn f.
Let eps be given.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
Apply (exists_eps_lt_pos_Euclid eps HepsR HepsPos) to the current goal.
Let Nsmall be given.
Assume HNsmall: Nsmall ∈ ω ∧ eps_ Nsmall < eps.
We prove the intermediate claim HNsmallO: Nsmall ∈ ω.
An exact proof term for the current goal is (andEL (Nsmall ∈ ω) (eps_ Nsmall < eps) HNsmall).
We prove the intermediate claim HepsNltS: eps_ Nsmall < eps.
An exact proof term for the current goal is (andER (Nsmall ∈ ω) (eps_ Nsmall < eps) HNsmall).
Set delta to be the term eps_ (ordsucc Nsmall).
We prove the intermediate claim HsuccO: ordsucc Nsmall ∈ ω.
An exact proof term for the current goal is (omega_ordsucc Nsmall HNsmallO).
We prove the intermediate claim HdeltaSNoS: delta ∈ SNoS_ ω.
We prove the intermediate claim Hdef: delta = eps_ (ordsucc Nsmall).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (SNo_eps_SNoS_omega (ordsucc Nsmall) HsuccO).
We prove the intermediate claim HdeltaR: delta ∈ R.
An exact proof term for the current goal is (SNoS_omega_real delta HdeltaSNoS).
We prove the intermediate claim HdeltaPosS: 0 < delta.
We prove the intermediate claim Hdef: delta = eps_ (ordsucc Nsmall).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc Nsmall) HsuccO).
We prove the intermediate claim HdeltaPos: Rlt 0 delta.
An exact proof term for the current goal is (RltI 0 delta real_0 HdeltaR HdeltaPosS).
Apply (Huc delta HdeltaR HdeltaPos) to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0o: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn n) x)) delta) HN0pair).
We prove the intermediate claim Htail: ∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn n) x)) delta.
An exact proof term for the current goal is (andER (N0 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N0 ⊆ m → N0 ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m) x,apply_fun (apply_fun fn n) x)) delta) HN0pair).
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN0o.
Let n be given.
Assume HnO: n ∈ ω.
Assume HN0n: N0 ⊆ n.
Let x be given.
Assume HxX: x ∈ X.
We will prove Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps.
Set seqx to be the term graph ω (λk : set ⇒ apply_fun (apply_fun fn k) x).
We prove the intermediate claim Hfdef: f = graph X (λx0 : set ⇒ Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) (graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x0)) y)).
Use reflexivity.
We prove the intermediate claim HfxEq: apply_fun f x = Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y).
rewrite the current goal using (apply_fun_of_graph_eq f X (λx0 : set ⇒ Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) (graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x0)) y)) x Hfdef HxX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hseqx: sequence_on seqx Y.
Let k be given.
Assume HkO: k ∈ ω.
We will prove apply_fun seqx k ∈ Y.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x) k Hseqxdef HkO) (from left to right).
We prove the intermediate claim HfnkFS: apply_fun fn k ∈ function_space X Y.
An exact proof term for the current goal is (Hfn k HkO).
We prove the intermediate claim Hfnk_on: function_on (apply_fun fn k) X Y.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λf0 : set ⇒ function_on f0 X Y) (apply_fun fn k) HfnkFS).
An exact proof term for the current goal is (Hfnk_on x HxX).
We prove the intermediate claim Hcaux: cauchy_sequence Y d seqx.
We prove the intermediate claim Hdef: cauchy_sequence Y d seqx = (metric_on Y d ∧ sequence_on seqx Y ∧ ∀e : set, e ∈ R ∧ Rlt 0 e → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seqx m,apply_fun seqx n)) e).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HmY.
An exact proof term for the current goal is Hseqx.
Let e be given.
Assume He: e ∈ R ∧ Rlt 0 e.
We prove the intermediate claim HeR: e ∈ R.
An exact proof term for the current goal is (andEL (e ∈ R) (Rlt 0 e) He).
We prove the intermediate claim HePos: Rlt 0 e.
An exact proof term for the current goal is (andER (e ∈ R) (Rlt 0 e) He).
We prove the intermediate claim HNbig: ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m) x0,apply_fun (apply_fun fn n) x0)) e.
An exact proof term for the current goal is (Huc e HeR HePos).
Apply HNbig to the current goal.
Let N be given.
Assume HNpair.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m) x0,apply_fun (apply_fun fn n) x0)) e) HNpair).
Let m and n be given.
Assume HmO: m ∈ ω.
Assume HnO: n ∈ ω.
Assume HNm: N ⊆ m.
Assume HNn: N ⊆ n.
We will prove Rlt (apply_fun d (apply_fun seqx m,apply_fun seqx n)) e.
We prove the intermediate claim Htail: ∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m0) x0,apply_fun (apply_fun fn n0) x0)) e.
An exact proof term for the current goal is (andER (N ∈ ω) (∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn m0) x0,apply_fun (apply_fun fn n0) x0)) e) HNpair).
We prove the intermediate claim Hseqm: apply_fun seqx m = apply_fun (apply_fun fn m) x.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x) m Hseqxdef HmO) (from left to right).
Use reflexivity.
We prove the intermediate claim Hseqn: apply_fun seqx n = apply_fun (apply_fun fn n) x.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x) n Hseqxdef HnO) (from left to right).
Use reflexivity.
rewrite the current goal using Hseqm (from left to right).
rewrite the current goal using Hseqn (from left to right).
An exact proof term for the current goal is (Htail m n HmO HnO HNm HNn x HxX).
We prove the intermediate claim Hexlim: ∃y : set, converges_to Y (metric_topology Y d) seqx y.
An exact proof term for the current goal is (Hcomplete seqx Hseqx Hcaux).
We prove the intermediate claim HlimChosen: converges_to Y (metric_topology Y d) seqx (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)).
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y) Hexlim).
We prove the intermediate claim Hlim34: (∀U : set, U ∈ metric_topology Y d → (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ U → ∃N : set, N ∈ ω ∧ ∀k : set, k ∈ ω → N ⊆ k → apply_fun seqx k ∈ U).
An exact proof term for the current goal is (andER ((topology_on Y (metric_topology Y d) ∧ sequence_on seqx Y) ∧ (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Y) (∀U : set, U ∈ metric_topology Y d → (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ U → ∃N : set, N ∈ ω ∧ ∀k : set, k ∈ ω → N ⊆ k → apply_fun seqx k ∈ U) HlimChosen).
Set fx to be the term apply_fun f x.
We prove the intermediate claim HfxDef: fx = apply_fun f x.
Use reflexivity.
We prove the intermediate claim HfxEq2: fx = Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y).
rewrite the current goal using HfxDef (from left to right).
rewrite the current goal using HfxEq (from left to right).
Use reflexivity.
We prove the intermediate claim HfxY: fx ∈ Y.
rewrite the current goal using HfxEq2 (from left to right).
We prove the intermediate claim H12: (topology_on Y (metric_topology Y d) ∧ sequence_on seqx Y) ∧ (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Y.
An exact proof term for the current goal is (andEL ((topology_on Y (metric_topology Y d) ∧ sequence_on seqx Y) ∧ (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Y) (∀U : set, U ∈ metric_topology Y d → (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ U → ∃N : set, N ∈ ω ∧ ∀k : set, k ∈ ω → N ⊆ k → apply_fun seqx k ∈ U) HlimChosen).
An exact proof term for the current goal is (andER (topology_on Y (metric_topology Y d) ∧ sequence_on seqx Y) ((Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Y) H12).
Set Uball to be the term open_ball Y d fx delta.
We prove the intermediate claim HUballIn: Uball ∈ metric_topology Y d.
An exact proof term for the current goal is (open_ball_in_metric_topology Y d fx delta HmY HfxY HdeltaPos).
We prove the intermediate claim HfxInBall: fx ∈ Uball.
An exact proof term for the current goal is (center_in_open_ball Y d fx delta HmY HfxY HdeltaPos).
We prove the intermediate claim HexMx: ∃Mx : set, Mx ∈ ω ∧ ∀k : set, k ∈ ω → Mx ⊆ k → apply_fun seqx k ∈ Uball.
We prove the intermediate claim HfxInBall2: (Eps_i (λy : set ⇒ converges_to Y (metric_topology Y d) seqx y)) ∈ Uball.
rewrite the current goal using HfxEq2 (from right to left).
An exact proof term for the current goal is HfxInBall.
An exact proof term for the current goal is (Hlim34 Uball HUballIn HfxInBall2).
Apply HexMx to the current goal.
Let Mx be given.
Assume HMxpair.
We prove the intermediate claim HMxO: Mx ∈ ω.
An exact proof term for the current goal is (andEL (Mx ∈ ω) (∀k : set, k ∈ ω → Mx ⊆ k → apply_fun seqx k ∈ Uball) HMxpair).
We prove the intermediate claim HtailMx: ∀k : set, k ∈ ω → Mx ⊆ k → apply_fun seqx k ∈ Uball.
An exact proof term for the current goal is (andER (Mx ∈ ω) (∀k : set, k ∈ ω → Mx ⊆ k → apply_fun seqx k ∈ Uball) HMxpair).
Set m to be the term N0 ∪ Mx.
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (omega_binunion N0 Mx HN0o HMxO).
We prove the intermediate claim HN0subm: N0 ⊆ m.
Let t be given.
Assume Ht: t ∈ N0.
An exact proof term for the current goal is (binunionI1 N0 Mx t Ht).
We prove the intermediate claim HMxsubm: Mx ⊆ m.
Let t be given.
Assume Ht: t ∈ Mx.
An exact proof term for the current goal is (binunionI2 N0 Mx t Ht).
We prove the intermediate claim Hdnm: Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) delta.
An exact proof term for the current goal is (Htail n m HnO HmO HN0n HN0subm x HxX).
We prove the intermediate claim HmInBall: apply_fun (apply_fun fn m) x ∈ Uball.
We prove the intermediate claim HseqmEq: apply_fun seqx m = apply_fun (apply_fun fn m) x.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λk0 : set ⇒ apply_fun (apply_fun fn k0) x) m Hseqxdef HmO) (from left to right).
Use reflexivity.
rewrite the current goal using HseqmEq (from right to left).
An exact proof term for the current goal is (HtailMx m HmO HMxsubm).
We prove the intermediate claim Hdmfx0: Rlt (apply_fun d (fx,apply_fun (apply_fun fn m) x)) delta.
An exact proof term for the current goal is (open_ballE2 Y d fx delta (apply_fun (apply_fun fn m) x) HmInBall).
We prove the intermediate claim HxY1: apply_fun (apply_fun fn n) x ∈ Y.
We prove the intermediate claim HfnnFS: apply_fun fn n ∈ function_space X Y.
An exact proof term for the current goal is (Hfn n HnO).
We prove the intermediate claim Hfnn_on: function_on (apply_fun fn n) X Y.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λf0 : set ⇒ function_on f0 X Y) (apply_fun fn n) HfnnFS).
An exact proof term for the current goal is (Hfnn_on x HxX).
We prove the intermediate claim HxY2: apply_fun (apply_fun fn m) x ∈ Y.
We prove the intermediate claim HfnmFS: apply_fun fn m ∈ function_space X Y.
An exact proof term for the current goal is (Hfn m HmO).
We prove the intermediate claim Hfnm_on: function_on (apply_fun fn m) X Y.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λf0 : set ⇒ function_on f0 X Y) (apply_fun fn m) HfnmFS).
An exact proof term for the current goal is (Hfnm_on x HxX).
We prove the intermediate claim Hdmfx: Rlt (apply_fun d (apply_fun (apply_fun fn m) x,fx)) delta.
rewrite the current goal using (metric_on_symmetric Y d fx (apply_fun (apply_fun fn m) x) HmY HfxY HxY2) (from right to left).
An exact proof term for the current goal is Hdmfx0.
We prove the intermediate claim Htri: Rle (apply_fun d (apply_fun (apply_fun fn n) x,fx)) (add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) (apply_fun d (apply_fun (apply_fun fn m) x,fx))).
An exact proof term for the current goal is (metric_triangle_Rle Y d (apply_fun (apply_fun fn n) x) (apply_fun (apply_fun fn m) x) fx HmY HxY1 HxY2 HfxY).
Set a to be the term apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x).
Set b to be the term apply_fun d (apply_fun (apply_fun fn m) x,fx).
Set dn to be the term apply_fun d (apply_fun (apply_fun fn n) x,fx).
We prove the intermediate claim HaR: a ∈ R.
We prove the intermediate claim Hfun: function_on d (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_function_on Y d HmY).
We prove the intermediate claim Hab: (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) 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 fn n) x) (apply_fun (apply_fun fn m) x) HxY1 HxY2).
An exact proof term for the current goal is (Hfun (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x) Hab).
We prove the intermediate claim HbR: b ∈ R.
We prove the intermediate claim Hfun: function_on d (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_function_on Y d HmY).
We prove the intermediate claim Hab: (apply_fun (apply_fun fn m) x,fx) ∈ setprod Y Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun (apply_fun fn m) x) fx HxY2 HfxY).
An exact proof term for the current goal is (Hfun (apply_fun (apply_fun fn m) x,fx) Hab).
We prove the intermediate claim HdnR: dn ∈ R.
We prove the intermediate claim Hfun: function_on d (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_function_on Y d HmY).
We prove the intermediate claim Hab: (apply_fun (apply_fun fn n) x,fx) ∈ setprod Y Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun (apply_fun fn n) x) fx HxY1 HfxY).
An exact proof term for the current goal is (Hfun (apply_fun (apply_fun fn n) x,fx) Hab).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
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 HltA: a < delta.
An exact proof term for the current goal is (RltE_lt a delta Hdnm).
We prove the intermediate claim HltB: b < delta.
An exact proof term for the current goal is (RltE_lt b delta Hdmfx).
We prove the intermediate claim Hsum1: add_SNo b a < add_SNo b delta.
An exact proof term for the current goal is (add_SNo_Lt2 b a delta HbS HaS HdeltaS HltA).
We prove the intermediate claim Hsum2: add_SNo b delta = add_SNo delta b.
An exact proof term for the current goal is (add_SNo_com b delta HbS HdeltaS).
We prove the intermediate claim Hsum3: add_SNo delta b < add_SNo delta delta.
An exact proof term for the current goal is (add_SNo_Lt2 delta b delta HdeltaS HbS HdeltaS HltB).
We prove the intermediate claim Hsum4: add_SNo b a < add_SNo delta delta.
We prove the intermediate claim Hsum3b: add_SNo b delta < add_SNo delta delta.
rewrite the current goal using Hsum2 (from left to right).
An exact proof term for the current goal is Hsum3.
An exact proof term for the current goal is (SNoLt_tra (add_SNo b a) (add_SNo b delta) (add_SNo delta delta) (SNo_add_SNo b a HbS HaS) (SNo_add_SNo b delta HbS HdeltaS) (SNo_add_SNo delta delta HdeltaS HdeltaS) Hsum1 Hsum3b).
We prove the intermediate claim Hsum5: add_SNo a b = add_SNo b a.
An exact proof term for the current goal is (add_SNo_com a b HaS HbS).
We prove the intermediate claim Hsum6: add_SNo a b < add_SNo delta delta.
rewrite the current goal using Hsum5 (from left to right).
An exact proof term for the current goal is Hsum4.
We prove the intermediate claim HepsNR: eps_ Nsmall ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ Nsmall) (SNo_eps_SNoS_omega Nsmall HNsmallO)).
We prove the intermediate claim HepsNS: SNo (eps_ Nsmall).
An exact proof term for the current goal is (real_SNo (eps_ Nsmall) HepsNR).
We prove the intermediate claim Hhalf: add_SNo delta delta = eps_ Nsmall.
We prove the intermediate claim Hnat: nat_p Nsmall.
An exact proof term for the current goal is (omega_nat_p Nsmall HNsmallO).
An exact proof term for the current goal is (eps_ordsucc_half_add Nsmall Hnat).
We prove the intermediate claim Hsum7: add_SNo a b < eps_ Nsmall.
rewrite the current goal using Hhalf (from right to left).
An exact proof term for the current goal is Hsum6.
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HepsNlt: eps_ Nsmall < eps.
An exact proof term for the current goal is HepsNltS.
We prove the intermediate claim Hsum8: add_SNo a b < eps.
An exact proof term for the current goal is (SNoLt_tra (add_SNo a b) (eps_ Nsmall) eps (SNo_add_SNo a b HaS HbS) HepsNS HepsS Hsum7 HepsNlt).
We prove the intermediate claim HsumR: add_SNo a b ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR b HbR).
We prove the intermediate claim HsumLt: Rlt (add_SNo a b) eps.
An exact proof term for the current goal is (RltI (add_SNo a b) eps HsumR HepsR Hsum8).
We prove the intermediate claim HdnEq: dn = apply_fun d (apply_fun (apply_fun fn n) x,fx).
Use reflexivity.
rewrite the current goal using HdnEq (from left to right).
An exact proof term for the current goal is (Rle_Rlt_tra dn (add_SNo a b) eps Htri HsumLt).
∎