Let X, d and Fam be given.
Assume Hd: metric_on X d.
Assume Hseqc: sequentially_compact X (metric_topology X d).
Assume Hcov: open_cover_of X (metric_topology X d) Fam.
We will prove ∃N : set, N ∈ ω ∧ lebesgue_number_metric X d Fam (eps_ N).
Apply (xm (X = Empty)) to the current goal.
Assume HXEmpty: X = Empty.
We use 0 to witness the existential quantifier.
We prove the intermediate claim H0o: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Apply andI to the current goal.
An exact proof term for the current goal is H0o.
We will prove lebesgue_number_metric X d Fam (eps_ 0).
rewrite the current goal using HXEmpty (from left to right).
We will prove eps_ 0 ∈ R ∧ Rlt 0 (eps_ 0) ∧ ∀x : set, x ∈ Empty → ∃U : set, U ∈ Fam ∧ open_ball Empty d x (eps_ 0) ⊆ U.
We prove the intermediate claim Heps0R: eps_ 0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ 0) (SNo_eps_SNoS_omega 0 H0o)).
We prove the intermediate claim Heps0posS: 0 < eps_ 0.
An exact proof term for the current goal is (SNo_eps_pos 0 H0o).
We prove the intermediate claim Heps0pos: Rlt 0 (eps_ 0).
An exact proof term for the current goal is (RltI 0 (eps_ 0) real_0 Heps0R Heps0posS).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Heps0R.
An exact proof term for the current goal is Heps0pos.
Let x be given.
Assume HxE: x ∈ Empty.
We will prove ∃U : set, U ∈ Fam ∧ open_ball Empty d x (eps_ 0) ⊆ U.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
Assume HXne: ¬ (X = Empty).
Apply (xm (∃N : set, N ∈ ω ∧ lebesgue_number_metric X d Fam (eps_ N))) to the current goal.
Assume Hex: ∃N : set, N ∈ ω ∧ lebesgue_number_metric X d Fam (eps_ N).
An exact proof term for the current goal is Hex.
Assume Hno: ¬ (∃N : set, N ∈ ω ∧ lebesgue_number_metric X d Fam (eps_ N)).
We will prove ∃N : set, N ∈ ω ∧ lebesgue_number_metric X d Fam (eps_ N).
We prove the intermediate claim HnoN: ∀n : set, n ∈ ω → ¬ (lebesgue_number_metric X d Fam (eps_ n)).
Let n be given.
Assume HnO: n ∈ ω.
Assume Hleb: lebesgue_number_metric X d Fam (eps_ n).
Apply Hno to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
An exact proof term for the current goal is Hleb.
Set badpt to be the term (λn : set ⇒ Eps_i (λx : set ⇒ x ∈ X ∧ ∀U : set, U ∈ Fam → ¬ (open_ball X d x (eps_ n) ⊆ U))).
We prove the intermediate claim Hbadpt: ∀n : set, n ∈ ω → badpt n ∈ X ∧ ∀U : set, U ∈ Fam → ¬ (open_ball X d (badpt n) (eps_ n) ⊆ U).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HepsR: eps_ n ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ n) (SNo_eps_SNoS_omega n HnO)).
We prove the intermediate claim HepsPosS: 0 < eps_ n.
An exact proof term for the current goal is (SNo_eps_pos n HnO).
We prove the intermediate claim HepsPos: Rlt 0 (eps_ n).
An exact proof term for the current goal is (RltI 0 (eps_ n) real_0 HepsR HepsPosS).
We prove the intermediate claim HnotAll: ¬ (∀x : set, x ∈ X → ∃U : set, U ∈ Fam ∧ open_ball X d x (eps_ n) ⊆ U).
Assume Hall: ∀x : set, x ∈ X → ∃U : set, U ∈ Fam ∧ open_ball X d x (eps_ n) ⊆ U.
Apply (HnoN n HnO) to the current goal.
We will prove lebesgue_number_metric X d Fam (eps_ n).
We will prove eps_ n ∈ R ∧ Rlt 0 (eps_ n) ∧ ∀x : set, x ∈ X → ∃U : set, U ∈ Fam ∧ open_ball X d x (eps_ n) ⊆ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HepsR.
An exact proof term for the current goal is HepsPos.
An exact proof term for the current goal is Hall.
Apply (not_all_ex_demorgan_i (λx : set ⇒ x ∈ X → ∃U : set, U ∈ Fam ∧ open_ball X d x (eps_ n) ⊆ U) HnotAll) to the current goal.
Let x be given.
Assume HxNotImp: ¬ (x ∈ X → ∃U : set, U ∈ Fam ∧ open_ball X d x (eps_ n) ⊆ U).
We prove the intermediate claim HxX: x ∈ X.
Apply (xm (x ∈ X)) to the current goal.
Assume HxX0: x ∈ X.
An exact proof term for the current goal is HxX0.
Assume HxNotX: ¬ (x ∈ X).
Apply FalseE to the current goal.
Apply HxNotImp to the current goal.
Assume HxX0: x ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxNotX HxX0).
We prove the intermediate claim HnotEx: ¬ (∃U : set, U ∈ Fam ∧ open_ball X d x (eps_ n) ⊆ U).
Assume HexU: ∃U : set, U ∈ Fam ∧ open_ball X d x (eps_ n) ⊆ U.
Apply HxNotImp to the current goal.
Assume _: x ∈ X.
An exact proof term for the current goal is HexU.
We prove the intermediate claim HforU: ∀U : set, U ∈ Fam → ¬ (open_ball X d x (eps_ n) ⊆ U).
Let U be given.
Assume HUfam: U ∈ Fam.
Assume Hsub: open_ball X d x (eps_ n) ⊆ U.
Apply HnotEx to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUfam.
An exact proof term for the current goal is Hsub.
We prove the intermediate claim HxBad: x ∈ X ∧ ∀U : set, U ∈ Fam → ¬ (open_ball X d x (eps_ n) ⊆ U).
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HforU.
An exact proof term for the current goal is (Eps_i_ax (λx0 : set ⇒ x0 ∈ X ∧ ∀U : set, U ∈ Fam → ¬ (open_ball X d x0 (eps_ n) ⊆ U)) x HxBad).
Set seq to be the term graph ω (λn : set ⇒ badpt n).
We prove the intermediate claim Hseqval: ∀n : set, n ∈ ω → badpt n ∈ X.
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (badpt n ∈ X) (∀U : set, U ∈ Fam → ¬ (open_ball X d (badpt n) (eps_ n) ⊆ U)) (Hbadpt n HnO)).
We prove the intermediate claim Htotseq: total_function_on seq ω X.
We prove the intermediate claim Hdef: seq = graph ω (λn : set ⇒ badpt n).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (total_function_on_graph ω X (λn : set ⇒ badpt n) Hseqval).
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (total_function_on_function_on seq ω X Htotseq).
Apply Hseqc to the current goal.
Assume HTx HseqcProp.
Apply (HseqcProp seq Hseq) to the current goal.
Let subseq be given.
Assume Hexsub.
Apply Hexsub to the current goal.
Let x0 be given.
Assume Hpack.
We prove the intermediate claim Hsubseq: 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 x0) Hpack).
We prove the intermediate claim Hconv: converges_to X (metric_topology X d) subseq x0.
An exact proof term for the current goal is (andER (subsequence_of seq subseq) (converges_to X (metric_topology X d) subseq x0) Hpack).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (converges_to_point_in_X X (metric_topology X d) subseq x0 Hconv).
We prove the intermediate claim HXcov: X ⊆ ⋃ Fam.
An exact proof term for the current goal is (open_cover_of_covers X (metric_topology X d) Fam Hcov).
We prove the intermediate claim Hx0Union: x0 ∈ ⋃ Fam.
An exact proof term for the current goal is (HXcov x0 Hx0X).
Apply (UnionE Fam x0 Hx0Union) to the current goal.
Let U0 be given.
Assume Hx0pack: x0 ∈ U0 ∧ U0 ∈ Fam.
We prove the intermediate claim Hx0U0: x0 ∈ U0.
An exact proof term for the current goal is (andEL (x0 ∈ U0) (U0 ∈ Fam) Hx0pack).
We prove the intermediate claim HU0Fam: U0 ∈ Fam.
An exact proof term for the current goal is (andER (x0 ∈ U0) (U0 ∈ Fam) Hx0pack).
We prove the intermediate claim HU0open: U0 ∈ metric_topology X d.
An exact proof term for the current goal is (open_cover_of_members_open X (metric_topology X d) Fam U0 Hcov HU0Fam).
We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x0 r ⊆ U0).
An exact proof term for the current goal is (metric_topology_neighborhood_contains_ball X d x0 U0 Hd Hx0X HU0open Hx0U0).
Apply Hexr to the current goal.
Let r be given.
Assume Hrpack.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r ∧ open_ball X d x0 r ⊆ U0) Hrpack).
We prove the intermediate claim Hrrest: Rlt 0 r ∧ open_ball X d x0 r ⊆ U0.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ open_ball X d x0 r ⊆ U0) Hrpack).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball X d x0 r ⊆ U0) Hrrest).
We prove the intermediate claim HballsubU0: open_ball X d x0 r ⊆ U0.
An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball X d x0 r ⊆ U0) Hrrest).
We prove the intermediate claim HexN0: ∃N0 ∈ ω, eps_ N0 < r.
An exact proof term for the current goal is (exists_eps_lt_pos r HrR Hrpos).
Apply HexN0 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 ∈ ω) (eps_ N0 < r) HN0pack).
We prove the intermediate claim HepsN0ltS: eps_ N0 < r.
An exact proof term for the current goal is (andER (N0 ∈ ω) (eps_ N0 < r) HN0pack).
We prove the intermediate claim HN0nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0omega).
Set N1 to be the term ordsucc N0.
We prove the intermediate claim HN1omega: N1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0omega).
Set eps1 to be the term eps_ N1.
We prove the intermediate claim Heps1R: eps1 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps1 (SNo_eps_SNoS_omega N1 HN1omega)).
We prove the intermediate claim Heps1PosS: 0 < eps1.
An exact proof term for the current goal is (SNo_eps_pos N1 HN1omega).
We prove the intermediate claim Heps1Pos: Rlt 0 eps1.
An exact proof term for the current goal is (RltI 0 eps1 real_0 Heps1R Heps1PosS).
We prove the intermediate claim HepsN0R: eps_ N0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N0) (SNo_eps_SNoS_omega N0 HN0omega)).
We prove the intermediate claim HepsN0lt: Rlt (eps_ N0) r.
An exact proof term for the current goal is (RltI (eps_ N0) r HepsN0R HrR HepsN0ltS).
We prove the intermediate claim HsumEq: add_SNo eps1 eps1 = eps_ N0.
An exact proof term for the current goal is (eps_ordsucc_half_add N0 HN0nat).
We prove the intermediate claim HsumR: add_SNo eps1 eps1 ∈ R.
An exact proof term for the current goal is (real_add_SNo eps1 Heps1R eps1 Heps1R).
We prove the intermediate claim HsumRlt: Rlt (add_SNo eps1 eps1) r.
rewrite the current goal using HsumEq (from left to right).
An exact proof term for the current goal is HepsN0lt.
Set B1 to be the term open_ball X d x0 eps1.
We prove the intermediate claim HB1open: B1 ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d x0 eps1 Hd Hx0X Heps1Pos).
We prove the intermediate claim Hx0B1: x0 ∈ B1.
An exact proof term for the current goal is (center_in_open_ball X d x0 eps1 Hd Hx0X Heps1Pos).
We prove the intermediate claim HexK: ∃K : set, K ∈ ω ∧ ∀k : set, k ∈ ω → K ⊆ k → apply_fun subseq k ∈ B1.
An exact proof term for the current goal is (converges_to_neighborhoods X (metric_topology X d) subseq x0 Hconv B1 HB1open Hx0B1).
Apply HexK to the current goal.
Let K be given.
Assume HKpack.
We prove the intermediate claim HKomega: K ∈ ω.
An exact proof term for the current goal is (andEL (K ∈ ω) (∀k : set, k ∈ ω → K ⊆ k → apply_fun subseq k ∈ B1) HKpack).
We prove the intermediate claim HeventB1: ∀k : set, k ∈ ω → K ⊆ k → apply_fun subseq k ∈ B1.
An exact proof term for the current goal is (andER (K ∈ ω) (∀k : set, k ∈ ω → K ⊆ k → apply_fun subseq k ∈ B1) HKpack).
Apply Hsubseq to the current goal.
Let f be given.
Assume 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 ω) ∧ 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 Hfcore2: (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) Hfcore).
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) Hfcore).
We prove the intermediate claim Hfcore3: 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 ω) Hfcore2).
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 ω) Hfcore2).
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) Hfcore3).
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) Hfcore3).
We prove the intermediate claim HsuccN1omega: ordsucc N1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N1 HN1omega).
We prove the intermediate claim Hexk0: ∃k0 : set, k0 ∈ ω ∧ ordsucc N1 ⊆ apply_fun f k0.
An exact proof term for the current goal is (omega_strictly_increasing_unbounded f (ordsucc N1) Hftot Hffg Hfdom Hfinc HsuccN1omega).
Apply Hexk0 to the current goal.
Let k0 be given.
Assume Hk0pack.
We prove the intermediate claim Hk0omega: k0 ∈ ω.
An exact proof term for the current goal is (andEL (k0 ∈ ω) (ordsucc N1 ⊆ apply_fun f k0) Hk0pack).
We prove the intermediate claim HsuccN1sub_fk0: ordsucc N1 ⊆ apply_fun f k0.
An exact proof term for the current goal is (andER (k0 ∈ ω) (ordsucc N1 ⊆ apply_fun f k0) Hk0pack).
We prove the intermediate claim HdirO: directed_set ω (inclusion_rel ω).
An exact proof term for the current goal is omega_directed_by_inclusion_rel.
Apply (directed_set_pair_upper_bound ω (inclusion_rel ω) K k0 HdirO HKomega Hk0omega) to the current goal.
Let k be given.
Assume Hkpack.
We prove the intermediate claim Hk1: k ∈ ω ∧ (K,k) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andEL (k ∈ ω ∧ (K,k) ∈ inclusion_rel ω) ((k0,k) ∈ inclusion_rel ω) Hkpack).
We prove the intermediate claim Hk0le: (k0,k) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andER (k ∈ ω ∧ (K,k) ∈ inclusion_rel ω) ((k0,k) ∈ inclusion_rel ω) Hkpack).
We prove the intermediate claim Hkomega: k ∈ ω.
An exact proof term for the current goal is (andEL (k ∈ ω) ((K,k) ∈ inclusion_rel ω) Hk1).
We prove the intermediate claim HKle: (K,k) ∈ inclusion_rel ω.
An exact proof term for the current goal is (andER (k ∈ ω) ((K,k) ∈ inclusion_rel ω) Hk1).
We prove the intermediate claim HKsubk: K ⊆ k.
An exact proof term for the current goal is (andER ((K,k) ∈ setprod ω ω) (K ⊆ k) (inclusion_relE ω K k HKle)).
We prove the intermediate claim Hk0subk: k0 ⊆ k.
An exact proof term for the current goal is (andER ((k0,k) ∈ setprod ω ω) (k0 ⊆ k) (inclusion_relE ω k0 k Hk0le)).
We prove the intermediate claim HsubkB1: apply_fun subseq k ∈ B1.
An exact proof term for the current goal is (HeventB1 k Hkomega HKsubk).
We prove the intermediate claim HsubkX: apply_fun subseq k ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x0 eps1 (apply_fun subseq k) HsubkB1).
We prove the intermediate claim Hfk0O: apply_fun f k0 ∈ ω.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω ω k0 Hftot Hk0omega).
We prove the intermediate claim HfkO: apply_fun f k ∈ ω.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω ω k Hftot Hkomega).
We prove the intermediate claim Hordk0: ordinal k0.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal k0 Hk0omega).
We prove the intermediate claim Hordk: ordinal k.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal k Hkomega).
We prove the intermediate claim Hk0EqOrIn: k0 = k ∨ k0 ∈ k.
Apply (ordinal_trichotomy_or_impred k0 k Hordk0 Hordk (k0 = k ∨ k0 ∈ k)) to the current goal.
Assume Hk0in: k0 ∈ k.
An exact proof term for the current goal is (orIR (k0 = k) (k0 ∈ k) Hk0in).
Assume Hk0eq: k0 = k.
An exact proof term for the current goal is (orIL (k0 = k) (k0 ∈ k) Hk0eq).
Assume Hkin: k ∈ k0.
Apply FalseE to the current goal.
We prove the intermediate claim Hkk: k ∈ k.
An exact proof term for the current goal is (Hk0subk k Hkin).
An exact proof term for the current goal is (In_irref k Hkk).
We prove the intermediate claim Hfk0sub_fk: apply_fun f k0 ⊆ apply_fun f k.
Apply (xm (k0 = k)) to the current goal.
Assume Hk0eq: k0 = k.
rewrite the current goal using Hk0eq (from left to right).
An exact proof term for the current goal is (Subq_ref (apply_fun f k)).
Assume Hk0ne: ¬ (k0 = k).
We prove the intermediate claim Hk0in: k0 ∈ k.
Apply (ordinal_trichotomy_or_impred k0 k Hordk0 Hordk (k0 ∈ k)) to the current goal.
Assume Hk0in0: k0 ∈ k.
An exact proof term for the current goal is Hk0in0.
Assume Hk0eq: k0 = k.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hk0ne Hk0eq).
Assume Hkin: k ∈ k0.
Apply FalseE to the current goal.
We prove the intermediate claim Hkk: k ∈ k.
An exact proof term for the current goal is (Hk0subk k Hkin).
An exact proof term for the current goal is (In_irref k Hkk).
We prove the intermediate claim Hfk0in_fk: apply_fun f k0 ∈ apply_fun f k.
An exact proof term for the current goal is (Hfinc k0 k Hk0omega Hkomega Hk0in).
We prove the intermediate claim Hord_fk: ordinal (apply_fun f k).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (apply_fun f k) HfkO).
We prove the intermediate claim Ht_fk: TransSet (apply_fun f k).
An exact proof term for the current goal is (ordinal_TransSet (apply_fun f k) Hord_fk).
An exact proof term for the current goal is (Ht_fk (apply_fun f k0) Hfk0in_fk).
We prove the intermediate claim HsuccN1sub_fk: ordsucc N1 ⊆ apply_fun f k.
An exact proof term for the current goal is (Subq_tra (ordsucc N1) (apply_fun f k0) (apply_fun f k) HsuccN1sub_fk0 Hfk0sub_fk).
We prove the intermediate claim HN1InSucc: N1 ∈ ordsucc N1.
An exact proof term for the current goal is (ordsuccI2 N1).
We prove the intermediate claim HN1in_fk: N1 ∈ apply_fun f k.
An exact proof term for the current goal is (HsuccN1sub_fk N1 HN1InSucc).
We prove the intermediate claim HepsfkSlt: eps_ (apply_fun f k) < eps1.
An exact proof term for the current goal is (SNo_eps_decr (apply_fun f k) HfkO N1 HN1in_fk).
We prove the intermediate claim HepsfkR: eps_ (apply_fun f k) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (apply_fun f k)) (SNo_eps_SNoS_omega (apply_fun f k) HfkO)).
We prove the intermediate claim HepsfkRlt: Rlt (eps_ (apply_fun f k)) eps1.
An exact proof term for the current goal is (RltI (eps_ (apply_fun f k)) eps1 HepsfkR Heps1R HepsfkSlt).
We prove the intermediate claim HBallSubU0: open_ball X d (apply_fun subseq k) (eps_ (apply_fun f k)) ⊆ U0.
Let y be given.
Assume HyBall: y ∈ open_ball X d (apply_fun subseq k) (eps_ (apply_fun f k)).
We will prove y ∈ U0.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d (apply_fun subseq k) (eps_ (apply_fun f k)) y HyBall).
We prove the intermediate claim Hdy: Rlt (apply_fun d (apply_fun subseq k,y)) (eps_ (apply_fun f k)).
An exact proof term for the current goal is (open_ballE2 X d (apply_fun subseq k) (eps_ (apply_fun f k)) y HyBall).
We prove the intermediate claim Hdx0subk: Rlt (apply_fun d (x0,apply_fun subseq k)) eps1.
An exact proof term for the current goal is (open_ballE2 X d x0 eps1 (apply_fun subseq k) HsubkB1).
We prove the intermediate claim Hdsubk: apply_fun d (x0,apply_fun subseq k) ∈ R.
We prove the intermediate claim Hfun: 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 Hpair: (x0,apply_fun subseq k) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 (apply_fun subseq k) Hx0X HsubkX).
An exact proof term for the current goal is (Hfun (x0,apply_fun subseq k) Hpair).
We prove the intermediate claim HdyR: apply_fun d (apply_fun subseq k,y) ∈ R.
We prove the intermediate claim Hfun: 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 Hpair: (apply_fun subseq k,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X (apply_fun subseq k) y HsubkX HyX).
An exact proof term for the current goal is (Hfun (apply_fun subseq k,y) Hpair).
We prove the intermediate claim Hdx0subkLt: apply_fun d (x0,apply_fun subseq k) < eps1.
An exact proof term for the current goal is (RltE_lt (apply_fun d (x0,apply_fun subseq k)) eps1 Hdx0subk).
We prove the intermediate claim HdyLt: apply_fun d (apply_fun subseq k,y) < eps1.
We prove the intermediate claim HdyRlt: Rlt (apply_fun d (apply_fun subseq k,y)) eps1.
An exact proof term for the current goal is (Rlt_tra (apply_fun d (apply_fun subseq k,y)) (eps_ (apply_fun f k)) eps1 Hdy HepsfkRlt).
An exact proof term for the current goal is (RltE_lt (apply_fun d (apply_fun subseq k,y)) eps1 HdyRlt).
We prove the intermediate claim Hdx0subkS: SNo (apply_fun d (x0,apply_fun subseq k)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x0,apply_fun subseq k)) Hdsubk).
We prove the intermediate claim HdyS: SNo (apply_fun d (apply_fun subseq k,y)).
An exact proof term for the current goal is (real_SNo (apply_fun d (apply_fun subseq k,y)) HdyR).
We prove the intermediate claim Heps1S: SNo eps1.
An exact proof term for the current goal is (real_SNo eps1 Heps1R).
We prove the intermediate claim Hsum1S: add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y)) < add_SNo (apply_fun d (x0,apply_fun subseq k)) eps1.
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y)) eps1 Hdx0subkS HdyS Heps1S HdyLt).
We prove the intermediate claim Hsum1R: Rlt (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) (add_SNo (apply_fun d (x0,apply_fun subseq k)) eps1).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) (add_SNo (apply_fun d (x0,apply_fun subseq k)) eps1) (real_add_SNo (apply_fun d (x0,apply_fun subseq k)) Hdsubk (apply_fun d (apply_fun subseq k,y)) HdyR) (real_add_SNo (apply_fun d (x0,apply_fun subseq k)) Hdsubk eps1 Heps1R) Hsum1S).
We prove the intermediate claim Hsum2S: add_SNo (apply_fun d (x0,apply_fun subseq k)) eps1 < add_SNo eps1 eps1.
An exact proof term for the current goal is (add_SNo_Lt1 (apply_fun d (x0,apply_fun subseq k)) eps1 eps1 Hdx0subkS Heps1S Heps1S Hdx0subkLt).
We prove the intermediate claim Hsum2R: Rlt (add_SNo (apply_fun d (x0,apply_fun subseq k)) eps1) (add_SNo eps1 eps1).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (x0,apply_fun subseq k)) eps1) (add_SNo eps1 eps1) (real_add_SNo (apply_fun d (x0,apply_fun subseq k)) Hdsubk eps1 Heps1R) (real_add_SNo eps1 Heps1R eps1 Heps1R) Hsum2S).
We prove the intermediate claim HsumRlt_r: Rlt (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) r.
An exact proof term for the current goal is (Rlt_tra (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) (add_SNo eps1 eps1) r (Rlt_tra (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) (add_SNo (apply_fun d (x0,apply_fun subseq k)) eps1) (add_SNo eps1 eps1) Hsum1R Hsum2R) HsumRlt).
We prove the intermediate claim HtriNot: ¬ (Rlt (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) (apply_fun d (x0,y))).
An exact proof term for the current goal is (metric_on_triangle X d x0 (apply_fun subseq k) y Hd Hx0X HsubkX HyX).
We prove the intermediate claim Hdx0yR: apply_fun d (x0,y) ∈ R.
We prove the intermediate claim Hfun: 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 Hpair: (x0,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 y Hx0X HyX).
An exact proof term for the current goal is (Hfun (x0,y) Hpair).
We prove the intermediate claim HsumR: add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (x0,apply_fun subseq k)) Hdsubk (apply_fun d (apply_fun subseq k,y)) HdyR).
We prove the intermediate claim Htri: Rle (apply_fun d (x0,y)) (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))).
Apply (RleI (apply_fun d (x0,y)) (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) Hdx0yR HsumR) to the current goal.
Assume Hbad: Rlt (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) (apply_fun d (x0,y)).
An exact proof term for the current goal is (HtriNot Hbad).
We prove the intermediate claim Hdx0yLt: Rlt (apply_fun d (x0,y)) r.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (apply_fun d (x0,y)) (add_SNo (apply_fun d (x0,apply_fun subseq k)) (apply_fun d (apply_fun subseq k,y))) r Htri HsumRlt_r).
We prove the intermediate claim HyBallx0: y ∈ open_ball X d x0 r.
An exact proof term for the current goal is (open_ballI X d x0 r y HyX Hdx0yLt).
An exact proof term for the current goal is (HballsubU0 y HyBallx0).
We prove the intermediate claim HsubkEq0: 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 Hseqdef: seq = graph ω (λn : set ⇒ badpt n).
Use reflexivity.
We prove the intermediate claim Hseqfk: apply_fun seq (apply_fun f k) = badpt (apply_fun f k).
rewrite the current goal using Hseqdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λn : set ⇒ badpt n) (apply_fun f k) HfkO).
We prove the intermediate claim HsubkEq: apply_fun subseq k = badpt (apply_fun f k).
rewrite the current goal using HsubkEq0 (from left to right).
rewrite the current goal using Hseqfk (from left to right).
Use reflexivity.
We prove the intermediate claim Hbadk: ∀U : set, U ∈ Fam → ¬ (open_ball X d (apply_fun subseq k) (eps_ (apply_fun f k)) ⊆ U).
Let U be given.
Assume HUfam: U ∈ Fam.
rewrite the current goal using HsubkEq (from left to right).
An exact proof term for the current goal is (andER (badpt (apply_fun f k) ∈ X) (∀U0 : set, U0 ∈ Fam → ¬ (open_ball X d (badpt (apply_fun f k)) (eps_ (apply_fun f k)) ⊆ U0)) (Hbadpt (apply_fun f k) HfkO) U HUfam).
Apply FalseE to the current goal.
An exact proof term for the current goal is ((Hbadk U0 HU0Fam) HBallSubU0).
∎