Let X, d, seq and x be given.
Assume Hd: metric_on X d.
Assume Hc: cauchy_sequence X d seq.
Assume Hex: ∃subseq : set, subsequence_of seq subseq ∧ converges_to X (metric_topology X d) subseq x.
We prove the intermediate claim Hc12: metric_on X d ∧ sequence_on seq X.
An exact proof term for the current goal is (andEL (metric_on X d ∧ sequence_on seq X) (∀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 seq m,apply_fun seq n)) eps) Hc).
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (andER (metric_on X d) (sequence_on seq X) Hc12).
We prove the intermediate claim Hcauch: ∀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 seq m,apply_fun seq n)) eps.
An exact proof term for the current goal is (andER (metric_on X d ∧ sequence_on seq X) (∀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 seq m,apply_fun seq n)) eps) Hc).
Apply Hex to the current goal.
Let subseq be given.
Assume Hpair.
We prove the intermediate claim Hsub: subsequence_of seq subseq.
An exact proof term for the current goal is (andEL (subsequence_of seq subseq) (converges_to X (metric_topology X d) subseq x) Hpair).
We prove the intermediate claim Hconv: converges_to X (metric_topology X d) subseq x.
An exact proof term for the current goal is (andER (subsequence_of seq subseq) (converges_to X (metric_topology X d) subseq x) Hpair).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (converges_to_point_in_X X (metric_topology X d) subseq x Hconv).
We will prove topology_on X (metric_topology X d) ∧ sequence_on seq X ∧ x ∈ X ∧ ∀U : set, U ∈ metric_topology X d → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
Apply and4I to the current goal.
An exact proof term for the current goal is (metric_topology_is_topology X d Hd).
An exact proof term for the current goal is Hseq.
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ metric_topology X d.
Assume HxU: x ∈ U.
Set B to be the term famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HTdef: metric_topology X d = generated_topology X B.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUlcl: ∀y ∈ U, ∃b ∈ B, y ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y0 ∈ U0, ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUlcl x HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpack).
We prove the intermediate claim Hbrest: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpack).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbrest).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbrest).
Apply (famunionE_impred X (λc0 : set ⇒ {open_ball X d c0 r|r ∈ R, Rlt 0 r}) b HbB (∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume HbIn: b ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b HbIn (∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U)) to the current goal.
Let r be given.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hbeq: b = open_ball X d c r.
We prove the intermediate claim Hxball: x ∈ open_ball X d c r.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ open_ball X d c r.
An exact proof term for the current goal is (open_ball_refine_center X d c x r Hd HcX HxX HrR Hrpos Hxball).
Apply Hexs to the current goal.
Let s be given.
Assume Hspack.
We prove the intermediate claim Hs12: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r) Hspack).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) Hs12).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) Hs12).
We prove the intermediate claim Hsub_ball: open_ball X d x s ⊆ open_ball X d c r.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r) Hspack).
We prove the intermediate claim HsubU: open_ball X d x s ⊆ U.
We prove the intermediate claim HballsubU: open_ball X d c r ⊆ U.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is HbsubU.
An exact proof term for the current goal is (Subq_tra (open_ball X d x s) (open_ball X d c r) U Hsub_ball HballsubU).
We prove the intermediate claim Hexeps1: ∃eps1 : set, eps1 ∈ R ∧ Rlt 0 eps1 ∧ Rlt (add_SNo eps1 eps1) s.
An exact proof term for the current goal is (exists_twofold_small_eps s HsR Hspos).
Apply Hexeps1 to the current goal.
Let eps1 be given.
Assume Heps1pack.
We prove the intermediate claim Heps1left: eps1 ∈ R ∧ Rlt 0 eps1.
An exact proof term for the current goal is (andEL (eps1 ∈ R ∧ Rlt 0 eps1) (Rlt (add_SNo eps1 eps1) s) Heps1pack).
We prove the intermediate claim Heps1R: eps1 ∈ R.
An exact proof term for the current goal is (andEL (eps1 ∈ R) (Rlt 0 eps1) Heps1left).
We prove the intermediate claim Heps1pos: Rlt 0 eps1.
An exact proof term for the current goal is (andER (eps1 ∈ R) (Rlt 0 eps1) Heps1left).
We prove the intermediate claim Heps2lt: Rlt (add_SNo eps1 eps1) s.
An exact proof term for the current goal is (andER (eps1 ∈ R ∧ Rlt 0 eps1) (Rlt (add_SNo eps1 eps1) s) Heps1pack).
We prove the intermediate claim HexN1: ∃N1 : set, N1 ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N1 ⊆ m → N1 ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps1.
An exact proof term for the current goal is (Hcauch eps1 (andI (eps1 ∈ R) (Rlt 0 eps1) Heps1R Heps1pos)).
Apply HexN1 to the current goal.
Let N1 be given.
Assume HN1pack.
We prove the intermediate claim HN1omega: N1 ∈ ω.
An exact proof term for the current goal is (andEL (N1 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N1 ⊆ m → N1 ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps1) HN1pack).
We prove the intermediate claim HN1prop: ∀m n : set, m ∈ ω → n ∈ ω → N1 ⊆ m → N1 ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps1.
An exact proof term for the current goal is (andER (N1 ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N1 ⊆ m → N1 ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps1) HN1pack).
Apply Hsub to the current goal.
Let f be given.
Assume Hfpack.
We prove the intermediate claim Hfpre: (((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) ∧ omega_strictly_increasing f).
An exact proof term for the current goal is (andEL (((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) ∧ omega_strictly_increasing f) (subseq = compose_fun ω f seq) Hfpack).
We prove the intermediate claim Hsubeq: subseq = compose_fun ω f seq.
An exact proof term for the current goal is (andER (((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) ∧ omega_strictly_increasing f) (subseq = compose_fun ω f seq) Hfpack).
We prove the intermediate claim Hfcore: (total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω.
An exact proof term for the current goal is (andEL ((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) (omega_strictly_increasing f) Hfpre).
We prove the intermediate claim Hfinc: omega_strictly_increasing f.
An exact proof term for the current goal is (andER ((total_function_on f ω ω ∧ functional_graph f) ∧ graph_domain_subset f ω) (omega_strictly_increasing f) Hfpre).
We prove the intermediate claim Hftotpair: total_function_on f ω ω ∧ functional_graph f.
An exact proof term for the current goal is (andEL (total_function_on f ω ω ∧ functional_graph f) (graph_domain_subset f ω) Hfcore).
We prove the intermediate claim Hfdom: graph_domain_subset f ω.
An exact proof term for the current goal is (andER (total_function_on f ω ω ∧ functional_graph f) (graph_domain_subset f ω) Hfcore).
We prove the intermediate claim Hftot: total_function_on f ω ω.
An exact proof term for the current goal is (andEL (total_function_on f ω ω) (functional_graph f) Hftotpair).
We prove the intermediate claim Hffg: functional_graph f.
An exact proof term for the current goal is (andER (total_function_on f ω ω) (functional_graph f) Hftotpair).
We prove the intermediate claim HfFun: function_on f ω ω.
An exact proof term for the current goal is (total_function_on_function_on f ω ω Hftot).
We prove the intermediate claim Hexk1: ∃k1 : set, k1 ∈ ω ∧ N1 ⊆ apply_fun f k1.
An exact proof term for the current goal is (omega_strictly_increasing_unbounded f N1 Hftot Hffg Hfdom Hfinc HN1omega).
Apply Hexk1 to the current goal.
Let k1 be given.
Assume Hk1pack.
We prove the intermediate claim Hk1omega: k1 ∈ ω.
An exact proof term for the current goal is (andEL (k1 ∈ ω) (N1 ⊆ apply_fun f k1) Hk1pack).
We prove the intermediate claim HN1subfk1: N1 ⊆ apply_fun f k1.
An exact proof term for the current goal is (andER (k1 ∈ ω) (N1 ⊆ apply_fun f k1) Hk1pack).
We prove the intermediate claim HballInB: open_ball X d x eps1 ∈ {open_ball X d x r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x r0) eps1 Heps1R Heps1pos).
We prove the intermediate claim HballInFam: open_ball X d x eps1 ∈ B.
An exact proof term for the current goal is (famunionI X (λc0 : set ⇒ {open_ball X d c0 r|r ∈ R, Rlt 0 r}) x (open_ball X d x eps1) HxX HballInB).
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (open_balls_form_basis X d Hd).
We prove the intermediate claim HballOpen: open_ball X d x eps1 ∈ metric_topology X d.
rewrite the current goal using HTdef (from left to right).
An exact proof term for the current goal is (generated_topology_contains_basis X B HBasis (open_ball X d x eps1) HballInFam).
We prove the intermediate claim HxInBall: x ∈ open_ball X d x eps1.
An exact proof term for the current goal is (center_in_open_ball X d x eps1 Hd HxX Heps1pos).
We prove the intermediate claim HexN2: ∃N2 : set, N2 ∈ ω ∧ ∀n : set, n ∈ ω → N2 ⊆ n → apply_fun subseq n ∈ open_ball X d x eps1.
An exact proof term for the current goal is (converges_to_neighborhoods X (metric_topology X d) subseq x Hconv (open_ball X d x eps1) HballOpen HxInBall).
Apply HexN2 to the current goal.
Let N2 be given.
Assume HN2pack.
We prove the intermediate claim HN2omega: N2 ∈ ω.
An exact proof term for the current goal is (andEL (N2 ∈ ω) (∀n : set, n ∈ ω → N2 ⊆ n → apply_fun subseq n ∈ open_ball X d x eps1) HN2pack).
We prove the intermediate claim HN2prop: ∀n : set, n ∈ ω → N2 ⊆ n → apply_fun subseq n ∈ open_ball X d x eps1.
An exact proof term for the current goal is (andER (N2 ∈ ω) (∀n : set, n ∈ ω → N2 ⊆ n → apply_fun subseq n ∈ open_ball X d x eps1) HN2pack).
We prove the intermediate claim Hk1ord: ordinal k1.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal k1 Hk1omega).
We prove the intermediate claim HN2ord: ordinal N2.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal N2 HN2omega).
We prove the intermediate claim Hcase: k1 ∈ N2 ∨ N2 ⊆ k1.
An exact proof term for the current goal is (ordinal_In_Or_Subq k1 N2 Hk1ord HN2ord).
Apply Hcase to the current goal.
Assume Hk1lt: k1 ∈ N2.
Set k to be the term N2.
We prove the intermediate claim Hkomega: k ∈ ω.
An exact proof term for the current goal is HN2omega.
We prove the intermediate claim HNk: N2 ⊆ k.
An exact proof term for the current goal is (Subq_ref N2).
We prove the intermediate claim HfkOmega: apply_fun f k ∈ ω.
An exact proof term for the current goal is (HfFun k Hkomega).
We prove the intermediate claim HfkOrd: ordinal (apply_fun f k).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (apply_fun f k) HfkOmega).
We prove the intermediate claim Hfk1In: apply_fun f k1 ∈ apply_fun f k.
An exact proof term for the current goal is (Hfinc k1 k Hk1omega Hkomega Hk1lt).
We prove the intermediate claim Htrans_fk: TransSet (apply_fun f k).
An exact proof term for the current goal is (andEL (TransSet (apply_fun f k)) (∀beta ∈ apply_fun f k, TransSet beta) HfkOrd).
We prove the intermediate claim Hsub_fk1_fk: apply_fun f k1 ⊆ apply_fun f k.
An exact proof term for the current goal is (Htrans_fk (apply_fun f k1) Hfk1In).
We prove the intermediate claim HN1subfk: N1 ⊆ apply_fun f k.
An exact proof term for the current goal is (Subq_tra N1 (apply_fun f k1) (apply_fun f k) HN1subfk1 Hsub_fk1_fk).
We prove the intermediate claim Hsubseqk: apply_fun subseq k ∈ open_ball X d x eps1.
An exact proof term for the current goal is (HN2prop k Hkomega HNk).
We use N1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1omega.
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N1 ⊆ n.
We will prove apply_fun seq n ∈ U.
We prove the intermediate claim Happ: apply_fun subseq k = apply_fun seq (apply_fun f k).
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is (compose_fun_apply ω f seq k Hkomega).
We prove the intermediate claim HfkO: apply_fun f k ∈ ω.
An exact proof term for the current goal is (HfFun k Hkomega).
We prove the intermediate claim HseqfkX: apply_fun seq (apply_fun f k) ∈ X.
An exact proof term for the current goal is (Hseq (apply_fun f k) HfkO).
We prove the intermediate claim Hdx1: Rlt (apply_fun d (x,apply_fun seq (apply_fun f k))) eps1.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is (open_ballE2 X d x eps1 (apply_fun subseq k) Hsubseqk).
We prove the intermediate claim Hsym: apply_fun d (x,apply_fun seq (apply_fun f k)) = apply_fun d (apply_fun seq (apply_fun f k),x).
An exact proof term for the current goal is (metric_on_symmetric X d x (apply_fun seq (apply_fun f k)) Hd HxX HseqfkX).
We prove the intermediate claim Hdx: Rlt (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1.
rewrite the current goal using Hsym (from right to left).
An exact proof term for the current goal is Hdx1.
We prove the intermediate claim Hdnfk: Rlt (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1.
An exact proof term for the current goal is (HN1prop n (apply_fun f k) HnO HfkO HNn HN1subfk).
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim Htri: Rle (apply_fun d (apply_fun seq n,x)) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))).
An exact proof term for the current goal is (metric_triangle_Rle X d (apply_fun seq n) (apply_fun seq (apply_fun f k)) x Hd HseqnX HseqfkX HxX).
We prove the intermediate claim Hdfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hd).
We prove the intermediate claim Hd1R: apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k)) ∈ R.
An exact proof term for the current goal is (Hdfun (apply_fun seq n,apply_fun seq (apply_fun f k)) (tuple_2_setprod_by_pair_Sigma X X (apply_fun seq n) (apply_fun seq (apply_fun f k)) HseqnX HseqfkX)).
We prove the intermediate claim Hd2R: apply_fun d (apply_fun seq (apply_fun f k),x) ∈ R.
An exact proof term for the current goal is (Hdfun (apply_fun seq (apply_fun f k),x) (tuple_2_setprod_by_pair_Sigma X X (apply_fun seq (apply_fun f k)) x HseqfkX HxX)).
We prove the intermediate claim Hd1le: Rle (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1 Hdnfk).
We prove the intermediate claim Hd2le: Rle (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1 Hdx).
We prove the intermediate claim HstepA: Rle (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1 Hd1R Hd2R Heps1R Hd2le).
We prove the intermediate claim HstepB: Rle (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1) (add_SNo eps1 eps1).
We prove the intermediate claim Hd1S: SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))).
An exact proof term for the current goal is (real_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) Hd1R).
We prove the intermediate claim Heps1S: SNo eps1.
An exact proof term for the current goal is (real_SNo eps1 Heps1R).
rewrite the current goal using (add_SNo_com (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1 Hd1S Heps1S) (from left to right).
An exact proof term for the current goal is (Rle_add_SNo_2 eps1 (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1 Heps1R Hd1R Heps1R Hd1le).
We prove the intermediate claim HsumLe: Rle (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo eps1 eps1).
An exact proof term for the current goal is (Rle_tra (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1) (add_SNo eps1 eps1) HstepA HstepB).
We prove the intermediate claim HsumLtS: Rlt (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) s.
An exact proof term for the current goal is (Rle_Rlt_tra (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo eps1 eps1) s HsumLe Heps2lt).
We prove the intermediate claim HdnxLt: Rlt (apply_fun d (apply_fun seq n,x)) s.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (apply_fun seq n,x)) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) s Htri HsumLtS).
We prove the intermediate claim HdxnLt: Rlt (apply_fun d (x,apply_fun seq n)) s.
rewrite the current goal using (metric_on_symmetric X d x (apply_fun seq n) Hd HxX HseqnX) (from left to right).
An exact proof term for the current goal is HdnxLt.
We prove the intermediate claim HseqnBall: apply_fun seq n ∈ open_ball X d x s.
An exact proof term for the current goal is (open_ballI X d x s (apply_fun seq n) HseqnX HdxnLt).
An exact proof term for the current goal is (HsubU (apply_fun seq n) HseqnBall).
Assume HN2sub: N2 ⊆ k1.
Set k to be the term k1.
We prove the intermediate claim Hkomega: k ∈ ω.
An exact proof term for the current goal is Hk1omega.
We prove the intermediate claim HNk: N2 ⊆ k.
An exact proof term for the current goal is HN2sub.
We prove the intermediate claim HN1subfk: N1 ⊆ apply_fun f k.
An exact proof term for the current goal is HN1subfk1.
We prove the intermediate claim Hsubseqk: apply_fun subseq k ∈ open_ball X d x eps1.
An exact proof term for the current goal is (HN2prop k Hkomega HNk).
We use N1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1omega.
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N1 ⊆ n.
We will prove apply_fun seq n ∈ U.
We prove the intermediate claim Happ: apply_fun subseq k = apply_fun seq (apply_fun f k).
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is (compose_fun_apply ω f seq k Hkomega).
We prove the intermediate claim HfkO: apply_fun f k ∈ ω.
An exact proof term for the current goal is (HfFun k Hkomega).
We prove the intermediate claim HseqfkX: apply_fun seq (apply_fun f k) ∈ X.
An exact proof term for the current goal is (Hseq (apply_fun f k) HfkO).
We prove the intermediate claim Hdx1: Rlt (apply_fun d (x,apply_fun seq (apply_fun f k))) eps1.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is (open_ballE2 X d x eps1 (apply_fun subseq k) Hsubseqk).
We prove the intermediate claim Hsym: apply_fun d (x,apply_fun seq (apply_fun f k)) = apply_fun d (apply_fun seq (apply_fun f k),x).
An exact proof term for the current goal is (metric_on_symmetric X d x (apply_fun seq (apply_fun f k)) Hd HxX HseqfkX).
We prove the intermediate claim Hdx: Rlt (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1.
rewrite the current goal using Hsym (from right to left).
An exact proof term for the current goal is Hdx1.
We prove the intermediate claim Hdnfk: Rlt (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1.
An exact proof term for the current goal is (HN1prop n (apply_fun f k) HnO HfkO HNn HN1subfk).
We prove the intermediate claim HseqnX: apply_fun seq n ∈ X.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim Htri: Rle (apply_fun d (apply_fun seq n,x)) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))).
An exact proof term for the current goal is (metric_triangle_Rle X d (apply_fun seq n) (apply_fun seq (apply_fun f k)) x Hd HseqnX HseqfkX HxX).
We prove the intermediate claim Hdfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hd).
We prove the intermediate claim Hd1R: apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k)) ∈ R.
An exact proof term for the current goal is (Hdfun (apply_fun seq n,apply_fun seq (apply_fun f k)) (tuple_2_setprod_by_pair_Sigma X X (apply_fun seq n) (apply_fun seq (apply_fun f k)) HseqnX HseqfkX)).
We prove the intermediate claim Hd2R: apply_fun d (apply_fun seq (apply_fun f k),x) ∈ R.
An exact proof term for the current goal is (Hdfun (apply_fun seq (apply_fun f k),x) (tuple_2_setprod_by_pair_Sigma X X (apply_fun seq (apply_fun f k)) x HseqfkX HxX)).
We prove the intermediate claim Hd1le: Rle (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1 Hdnfk).
We prove the intermediate claim Hd2le: Rle (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1.
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1 Hdx).
We prove the intermediate claim HstepA: Rle (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x)) eps1 Hd1R Hd2R Heps1R Hd2le).
We prove the intermediate claim HstepB: Rle (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1) (add_SNo eps1 eps1).
We prove the intermediate claim Hd1S: SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))).
An exact proof term for the current goal is (real_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) Hd1R).
We prove the intermediate claim Heps1S: SNo eps1.
An exact proof term for the current goal is (real_SNo eps1 Heps1R).
rewrite the current goal using (add_SNo_com (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1 Hd1S Heps1S) (from left to right).
An exact proof term for the current goal is (Rle_add_SNo_2 eps1 (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1 Heps1R Hd1R Heps1R Hd1le).
We prove the intermediate claim HsumLe: Rle (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo eps1 eps1).
An exact proof term for the current goal is (Rle_tra (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) eps1) (add_SNo eps1 eps1) HstepA HstepB).
We prove the intermediate claim HsumLtS: Rlt (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) s.
An exact proof term for the current goal is (Rle_Rlt_tra (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) (add_SNo eps1 eps1) s HsumLe Heps2lt).
We prove the intermediate claim HdnxLt: Rlt (apply_fun d (apply_fun seq n,x)) s.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (apply_fun seq n,x)) (add_SNo (apply_fun d (apply_fun seq n,apply_fun seq (apply_fun f k))) (apply_fun d (apply_fun seq (apply_fun f k),x))) s Htri HsumLtS).
We prove the intermediate claim HdxnLt: Rlt (apply_fun d (x,apply_fun seq n)) s.
rewrite the current goal using (metric_on_symmetric X d x (apply_fun seq n) Hd HxX HseqnX) (from left to right).
An exact proof term for the current goal is HdnxLt.
We prove the intermediate claim HseqnBall: apply_fun seq n ∈ open_ball X d x s.
An exact proof term for the current goal is (open_ballI X d x s (apply_fun seq n) HseqnX HdxnLt).
An exact proof term for the current goal is (HsubU (apply_fun seq n) HseqnBall).
∎