Let x be given.

Assume HxC: x ∈ intersection_over_family X Ufam.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀u0 : set, u0 ∈ Ufam → z0 ∈ u0) x HxC).

We prove the intermediate claim HxAll: ∀u0 : set, u0 ∈ Ufam → x ∈ u0.

An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ ∀u0 : set, u0 ∈ Ufam → z0 ∈ u0) x HxC).

Apply (SepI X (λx0 : set ⇒ continuous_at_map X Tx Y (metric_topology Y d) f x0) x HxX) to the current goal.

We will prove continuous_at_map X Tx Y (metric_topology Y d) f x.

We prove the intermediate claim HdefCont: continuous_at_map X Tx Y (metric_topology Y d) f x = (function_on f X Y ∧ x ∈ X ∧ ∀V : set, V ∈ metric_topology Y d → apply_fun f x ∈ V → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∀u : set, u ∈ U → apply_fun f u ∈ V).

Use reflexivity.

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

Apply andI to the current goal.

An exact proof term for the current goal is Hf.

An exact proof term for the current goal is HxX.

Let V be given.

Assume HV: V ∈ metric_topology Y d.

Assume HfxV: apply_fun f x ∈ V.

We prove the intermediate claim Hexn0: ∃n0 : set, n0 ∈ ω ∧ open_ball Y d (apply_fun f x) (inv_nat (ordsucc n0)) ⊆ V.

We prove the intermediate claim HmY: metric_on Y d.

An exact proof term for the current goal is (metric_on_total_imp_metric_on Y d Hd).

Set B to be the term famunion Y (λy0 : set ⇒ {open_ball Y d y0 r|r ∈ R, Rlt 0 r}).

We prove the intermediate claim HdefMT: metric_topology Y d = generated_topology Y B.

Use reflexivity.

We prove the intermediate claim HVgen: V ∈ generated_topology Y B.

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

An exact proof term for the current goal is HV.

We prove the intermediate claim HVloc: ∀y0 ∈ V, ∃b ∈ B, y0 ∈ b ∧ b ⊆ V.

An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ ∀y0 ∈ U0, ∃b ∈ B, y0 ∈ b ∧ b ⊆ U0) V HVgen).

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

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

Apply (HVloc (apply_fun f x) HfxV) to the current goal.

Let b be given.

Assume Hbpair.

We prove the intermediate claim HbB: b ∈ B.

An exact proof term for the current goal is (andEL (b ∈ B) (apply_fun f x ∈ b ∧ b ⊆ V) Hbpair).

We prove the intermediate claim Hbprop: apply_fun f x ∈ b ∧ b ⊆ V.

An exact proof term for the current goal is (andER (b ∈ B) (apply_fun f x ∈ b ∧ b ⊆ V) Hbpair).

We prove the intermediate claim Hfxb: apply_fun f x ∈ b.

An exact proof term for the current goal is (andEL (apply_fun f x ∈ b) (b ⊆ V) Hbprop).

We prove the intermediate claim HbsubV: b ⊆ V.

An exact proof term for the current goal is (andER (apply_fun f x ∈ b) (b ⊆ V) Hbprop).

Apply (famunionE_impred Y (λy0 : set ⇒ {open_ball Y d y0 r|r ∈ R, Rlt 0 r}) b HbB (∃n0 : set, n0 ∈ ω ∧ open_ball Y d (apply_fun f x) (inv_nat (ordsucc n0)) ⊆ V)) to the current goal.

Let c be given.

Assume HcY: c ∈ Y.

Assume HbIn: b ∈ {open_ball Y d c r|r ∈ R, Rlt 0 r}.

Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball Y d c r0) b HbIn (∃n0 : set, n0 ∈ ω ∧ open_ball Y d (apply_fun f x) (inv_nat (ordsucc n0)) ⊆ V)) to the current goal.

Let r be given.

Assume HrR: r ∈ R.

Assume Hrpos: Rlt 0 r.

Assume Hbeq: b = open_ball Y d c r.

We prove the intermediate claim HfxInBall: apply_fun f x ∈ open_ball Y d c r.

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

An exact proof term for the current goal is Hfxb.

We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball Y d (apply_fun f x) s ⊆ open_ball Y d c r.

An exact proof term for the current goal is (open_ball_refine_center Y d c (apply_fun f x) r HmY HcY HfxY HrR Hrpos HfxInBall).

Apply Hexs to the current goal.

Let s be given.

Assume Hs.

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 Y d (apply_fun f x) s ⊆ open_ball Y d c r) Hs).

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 HballSubCr: open_ball Y d (apply_fun f x) s ⊆ open_ball Y d c r.

An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball Y d (apply_fun f x) s ⊆ open_ball Y d c r) Hs).

We prove the intermediate claim HCrSubV: open_ball Y d c r ⊆ V.

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

An exact proof term for the current goal is HbsubV.

We prove the intermediate claim HballSSubV: open_ball Y d (apply_fun f x) s ⊆ V.

An exact proof term for the current goal is (Subq_tra (open_ball Y d (apply_fun f x) s) (open_ball Y d c r) V HballSubCr HCrSubV).

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) s.

An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt s HsR Hspos).

Apply HexN to the current goal.

Let N be given.

Assume HNpair.

We prove the intermediate claim HNin: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (Rlt (inv_nat (ordsucc N)) s) HNpair).

We prove the intermediate claim HinvLt: Rlt (inv_nat (ordsucc N)) s.

An exact proof term for the current goal is (andER (N ∈ ω) (Rlt (inv_nat (ordsucc N)) s) HNpair).

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HNin.

We prove the intermediate claim HsubSmall: open_ball Y d (apply_fun f x) (inv_nat (ordsucc N)) ⊆ open_ball Y d (apply_fun f x) s.

An exact proof term for the current goal is (open_ball_radius_mono Y d (apply_fun f x) (inv_nat (ordsucc N)) s HinvLt).

An exact proof term for the current goal is (Subq_tra (open_ball Y d (apply_fun f x) (inv_nat (ordsucc N))) (open_ball Y d (apply_fun f x) s) V HsubSmall HballSSubV).

Apply Hexn0 to the current goal.

Let n0 be given.

Assume Hn0: n0 ∈ ω ∧ open_ball Y d (apply_fun f x) (inv_nat (ordsucc n0)) ⊆ V.

We prove the intermediate claim Hn0in: n0 ∈ ω.

An exact proof term for the current goal is (andEL (n0 ∈ ω) (open_ball Y d (apply_fun f x) (inv_nat (ordsucc n0)) ⊆ V) Hn0).

We prove the intermediate claim HballSubV: open_ball Y d (apply_fun f x) (inv_nat (ordsucc n0)) ⊆ V.

An exact proof term for the current goal is (andER (n0 ∈ ω) (open_ball Y d (apply_fun f x) (inv_nat (ordsucc n0)) ⊆ V) Hn0).

We prove the intermediate claim HsuccOmega: ordsucc n0 ∈ ω.

An exact proof term for the current goal is (omega_ordsucc n0 Hn0in).

We prove the intermediate claim Hnot0: ordsucc n0 ∉ {0}.

Assume Hmem0: ordsucc n0 ∈ {0}.

We prove the intermediate claim Heq0: ordsucc n0 = 0.

An exact proof term for the current goal is (SingE 0 (ordsucc n0) Hmem0).

An exact proof term for the current goal is ((neq_ordsucc_0 n0) Heq0).

We prove the intermediate claim HsuccIn: ordsucc n0 ∈ ω ∖ {0}.

An exact proof term for the current goal is (setminusI ω {0} (ordsucc n0) HsuccOmega Hnot0).

Set eps0 to be the term inv_nat (ordsucc n0).

We prove the intermediate claim Heps0R: eps0 ∈ R.

An exact proof term for the current goal is (inv_nat_real (ordsucc n0) HsuccOmega).

We prove the intermediate claim Heps0Pos: Rlt 0 eps0.

An exact proof term for the current goal is (inv_nat_pos (ordsucc n0) HsuccIn).

We prove the intermediate claim Hu0in: (U_eps X Tx Y d fn eps0) ∈ Ufam.

An exact proof term for the current goal is (ReplI ω (λn1 : set ⇒ U_eps X Tx Y d fn (inv_nat (ordsucc n1))) n0 Hn0in).

We prove the intermediate claim HxU0: x ∈ (U_eps X Tx Y d fn eps0).

An exact proof term for the current goal is (HxAll (U_eps X Tx Y d fn eps0) Hu0in).

Set UFam to be the term {interior_of X Tx (A_N_eps X Y d fn N eps0)|N ∈ ω}.

We prove the intermediate claim HUepsDef: U_eps X Tx Y d fn eps0 = ⋃ UFam.

Use reflexivity.

We prove the intermediate claim HxUnion: x ∈ ⋃ UFam.

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

An exact proof term for the current goal is HxU0.

Apply (UnionE_impred UFam x HxUnion (∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∀u : set, u ∈ U → apply_fun f u ∈ V)) to the current goal.

Let W be given.

Assume HxW: x ∈ W.

Assume HWin: W ∈ UFam.

Apply (ReplE_impred ω (λN0 : set ⇒ interior_of X Tx (A_N_eps X Y d fn N0 eps0)) W HWin (∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∀u : set, u ∈ U → apply_fun f u ∈ V)) to the current goal.

Let N0 be given.

Assume HN0: N0 ∈ ω.

Assume HWdef: W = interior_of X Tx (A_N_eps X Y d fn N0 eps0).

We prove the intermediate claim HxInt: x ∈ interior_of X Tx (A_N_eps X Y d fn N0 eps0).

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

An exact proof term for the current goal is HxW.

We prove the intermediate claim HxX2: x ∈ X.

An exact proof term for the current goal is HxX.

We prove the intermediate claim HintDef: interior_of X Tx (A_N_eps X Y d fn N0 eps0) = {x0 ∈ X|∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N0 eps0)}.

Use reflexivity.

We prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N0 eps0).

We prove the intermediate claim HxInt2: x ∈ {x0 ∈ X|∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N0 eps0)}.

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

An exact proof term for the current goal is HxInt.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N0 eps0)) x HxInt2).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0: U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N0 eps0).

We prove the intermediate claim HU0pair: U0 ∈ Tx ∧ x ∈ U0.

An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ x ∈ U0) (U0 ⊆ (A_N_eps X Y d fn N0 eps0)) HU0).

We prove the intermediate claim HU0subA: U0 ⊆ (A_N_eps X Y d fn N0 eps0).

An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ x ∈ U0) (U0 ⊆ (A_N_eps X Y d fn N0 eps0)) HU0).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (andEL (U0 ∈ Tx) (x ∈ U0) HU0pair).

We prove the intermediate claim HxU0': x ∈ U0.

An exact proof term for the current goal is (andER (U0 ∈ Tx) (x ∈ U0) HU0pair).

We prove the intermediate claim Hexeps1: ∃eps1 : set, eps1 ∈ R ∧ Rlt 0 eps1 ∧ Rlt (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)) eps0.

An exact proof term for the current goal is (exists_fourfold_small_eps eps0 Heps0R Heps0Pos).

Apply Hexeps1 to the current goal.

Let eps1 be given.

Assume Heps1.

We prove the intermediate claim Heps1core: eps1 ∈ R ∧ Rlt 0 eps1.

An exact proof term for the current goal is (andEL (eps1 ∈ R ∧ Rlt 0 eps1) (Rlt (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)) eps0) Heps1).

We prove the intermediate claim Heps1R: eps1 ∈ R.

An exact proof term for the current goal is (andEL (eps1 ∈ R) (Rlt 0 eps1) Heps1core).

We prove the intermediate claim Heps1Pos: Rlt 0 eps1.

An exact proof term for the current goal is (andER (eps1 ∈ R) (Rlt 0 eps1) Heps1core).

We prove the intermediate claim H4lt: Rlt (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)) eps0.

An exact proof term for the current goal is (andER (eps1 ∈ R ∧ Rlt 0 eps1) (Rlt (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)) eps0) Heps1).

We prove the intermediate claim Hexn1: ∃n1 : set, n1 ∈ ω ∧ Rlt (inv_nat (ordsucc n1)) eps1.

An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt eps1 Heps1R Heps1Pos).

Apply Hexn1 to the current goal.

Let n1 be given.

Assume Hn1pair.

We prove the intermediate claim Hn1O: n1 ∈ ω.

An exact proof term for the current goal is (andEL (n1 ∈ ω) (Rlt (inv_nat (ordsucc n1)) eps1) Hn1pair).

We prove the intermediate claim Hinv1Lt: Rlt (inv_nat (ordsucc n1)) eps1.

An exact proof term for the current goal is (andER (n1 ∈ ω) (Rlt (inv_nat (ordsucc n1)) eps1) Hn1pair).

Set epsS to be the term inv_nat (ordsucc n1).

We prove the intermediate claim HepsSR: epsS ∈ R.

An exact proof term for the current goal is (inv_nat_real (ordsucc n1) (omega_ordsucc n1 Hn1O)).

We prove the intermediate claim HepsSle: Rle epsS eps1.

An exact proof term for the current goal is (Rlt_implies_Rle epsS eps1 Hinv1Lt).

We prove the intermediate claim HUfamIn: (U_eps X Tx Y d fn epsS) ∈ Ufam.

An exact proof term for the current goal is (ReplI ω (λn2 : set ⇒ U_eps X Tx Y d fn (inv_nat (ordsucc n2))) n1 Hn1O).

We prove the intermediate claim HxInUepsS: x ∈ U_eps X Tx Y d fn epsS.

An exact proof term for the current goal is (HxAll (U_eps X Tx Y d fn epsS) HUfamIn).

We prove the intermediate claim HUmono: U_eps X Tx Y d fn epsS ⊆ U_eps X Tx Y d fn eps1.

An exact proof term for the current goal is (U_eps_monotone X Tx Y d fn epsS eps1 HTx HepsSR Heps1R HepsSle).

We prove the intermediate claim HxInUeps1: x ∈ U_eps X Tx Y d fn eps1.

An exact proof term for the current goal is (HUmono x HxInUepsS).

We prove the intermediate claim HexU1: ∃N1 : set, N1 ∈ ω ∧ ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ⊆ A_N_eps X Y d fn N1 eps1.

An exact proof term for the current goal is (U_epsE_open_subset_A_N X Tx Y d fn eps1 x HTx HxInUeps1).

Apply HexU1 to the current goal.

Let N1 be given.

Assume HN1pair.

We prove the intermediate claim HN1O: N1 ∈ ω.

An exact proof term for the current goal is (andEL (N1 ∈ ω) (∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ⊆ A_N_eps X Y d fn N1 eps1) HN1pair).

We prove the intermediate claim HexU1b: ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ⊆ A_N_eps X Y d fn N1 eps1.

An exact proof term for the current goal is (andER (N1 ∈ ω) (∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ⊆ A_N_eps X Y d fn N1 eps1) HN1pair).

Apply HexU1b to the current goal.

Let U1 be given.

Assume HU1: U1 ∈ Tx ∧ x ∈ U1 ∧ U1 ⊆ A_N_eps X Y d fn N1 eps1.

We prove the intermediate claim HU1pair: U1 ∈ Tx ∧ x ∈ U1.

An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ x ∈ U1) (U1 ⊆ A_N_eps X Y d fn N1 eps1) HU1).

We prove the intermediate claim HU1subA: U1 ⊆ A_N_eps X Y d fn N1 eps1.

An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ x ∈ U1) (U1 ⊆ A_N_eps X Y d fn N1 eps1) HU1).

We prove the intermediate claim HU1Tx: U1 ∈ Tx.

An exact proof term for the current goal is (andEL (U1 ∈ Tx) (x ∈ U1) HU1pair).

We prove the intermediate claim HxU1: x ∈ U1.

An exact proof term for the current goal is (andER (U1 ∈ Tx) (x ∈ U1) HU1pair).

Set U01 to be the term U0 ∩ U1.

We prove the intermediate claim HU01Tx: U01 ∈ Tx.

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

We prove the intermediate claim HxU01: x ∈ U01.

An exact proof term for the current goal is (binintersectI U0 U1 x HxU0' HxU1).

We prove the intermediate claim HexNx: ∃Nx : set, Nx ∈ ω ∧ ∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps1.

An exact proof term for the current goal is (Hlim x HxX eps1 Heps1R Heps1Pos).

Apply HexNx to the current goal.

Let Nx be given.

Assume HNxpair.

We prove the intermediate claim HNxO: Nx ∈ ω.

An exact proof term for the current goal is (andEL (Nx ∈ ω) (∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps1) HNxpair).

We prove the intermediate claim HNxprop: ∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps1.

An exact proof term for the current goal is (andER (Nx ∈ ω) (∀n : set, n ∈ ω → Nx ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps1) HNxpair).

Set Nmax to be the term (N0 ∪ N1) ∪ Nx.

We prove the intermediate claim HN01O: (N0 ∪ N1) ∈ ω.

An exact proof term for the current goal is (omega_binunion N0 N1 HN0 HN1O).

We prove the intermediate claim HNmaxO: Nmax ∈ ω.

An exact proof term for the current goal is (omega_binunion (N0 ∪ N1) Nx HN01O HNxO).

Set n to be the term ordsucc Nmax.

We prove the intermediate claim HnO: n ∈ ω.

An exact proof term for the current goal is (omega_ordsucc Nmax HNmaxO).

We prove the intermediate claim HN0n: N0 ⊆ n.

An exact proof term for the current goal is (Subq_tra N0 (N0 ∪ N1) n (binunion_Subq_1 N0 N1) (Subq_tra (N0 ∪ N1) Nmax n (binunion_Subq_1 (N0 ∪ N1) Nx) (ordsuccI1 Nmax))).

We prove the intermediate claim HN1n: N1 ⊆ n.

An exact proof term for the current goal is (Subq_tra N1 (N0 ∪ N1) n (binunion_Subq_2 N0 N1) (Subq_tra (N0 ∪ N1) Nmax n (binunion_Subq_1 (N0 ∪ N1) Nx) (ordsuccI1 Nmax))).

We prove the intermediate claim HNxn: Nx ⊆ n.

An exact proof term for the current goal is (Subq_tra Nx Nmax n (binunion_Subq_2 (N0 ∪ N1) Nx) (ordsuccI1 Nmax)).

Set fnn to be the term apply_fun fn n.

We prove the intermediate claim Hncont: continuous_map X Tx Y (metric_topology Y d) fnn.

An exact proof term for the current goal is (Hcont n HnO).

We prove the intermediate claim Hfnn: function_on fnn X Y.

An exact proof term for the current goal is (continuous_map_function_on X Tx Y (metric_topology Y d) fnn Hncont).

We prove the intermediate claim HmY: metric_on Y d.

An exact proof term for the current goal is (metric_on_total_imp_metric_on Y d Hd).

We prove the intermediate claim HfnxY: apply_fun fnn x ∈ Y.

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

We prove the intermediate claim Hvball: open_ball Y d (apply_fun fnn x) eps1 ∈ metric_topology Y d.

An exact proof term for the current goal is (open_ball_in_metric_topology Y d (apply_fun fnn x) eps1 HmY HfnxY Heps1Pos).

Set U2 to be the term preimage_of X fnn (open_ball Y d (apply_fun fnn x) eps1).

We prove the intermediate claim HU2Tx: U2 ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y (metric_topology Y d) fnn Hncont (open_ball Y d (apply_fun fnn x) eps1) Hvball).

We prove the intermediate claim HxU2: x ∈ U2.

We prove the intermediate claim HU2def: U2 = {x0 ∈ X|apply_fun fnn x0 ∈ open_ball Y d (apply_fun fnn x) eps1}.

Use reflexivity.

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

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun fnn x0 ∈ open_ball Y d (apply_fun fnn x) eps1) x HxX (center_in_open_ball Y d (apply_fun fnn x) eps1 HmY HfnxY Heps1Pos)).

Set U to be the term U01 ∩ U2.

We prove the intermediate claim HUinTx: U ∈ Tx.

An exact proof term for the current goal is (lemma_intersection_two_open X Tx U01 U2 HTx HU01Tx HU2Tx).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (binintersectI U01 U2 x HxU01 HxU2).

We use U to witness the existential quantifier.

Apply and3I to the current goal.

An exact proof term for the current goal is HUinTx.

An exact proof term for the current goal is HxU.

We will prove ∀u : set, u ∈ U → apply_fun f u ∈ V.

Let u be given.

Assume HuU: u ∈ U.

We prove the intermediate claim HuU01: u ∈ U01.

An exact proof term for the current goal is (binintersectE1 U01 U2 u HuU).

We prove the intermediate claim HuU2: u ∈ U2.

An exact proof term for the current goal is (binintersectE2 U01 U2 u HuU).

We prove the intermediate claim HuU0: u ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 U1 u HuU01).

We prove the intermediate claim HuU1: u ∈ U1.

An exact proof term for the current goal is (binintersectE2 U0 U1 u HuU01).

We prove the intermediate claim HuX: u ∈ X.

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

We prove the intermediate claim HfuY: apply_fun f u ∈ Y.

An exact proof term for the current goal is (Hf u HuX).

We prove the intermediate claim HballGoal: apply_fun f u ∈ open_ball Y d (apply_fun f x) eps0.

Apply (open_ballI Y d (apply_fun f x) eps0 (apply_fun f u) HfuY) to the current goal.

We prove the intermediate claim HfnnuY: apply_fun fnn u ∈ Y.

An exact proof term for the current goal is (Hfnn u HuX).

We prove the intermediate claim HU2def2: U2 = {x0 ∈ X|apply_fun fnn x0 ∈ open_ball Y d (apply_fun fnn x) eps1}.

Use reflexivity.

We prove the intermediate claim HuBalln: apply_fun fnn u ∈ open_ball Y d (apply_fun fnn x) eps1.

We prove the intermediate claim HuU2': u ∈ {x0 ∈ X|apply_fun fnn x0 ∈ open_ball Y d (apply_fun fnn x) eps1}.

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

An exact proof term for the current goal is HuU2.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun fnn x0 ∈ open_ball Y d (apply_fun fnn x) eps1) u HuU2').

We prove the intermediate claim Hdfnn: Rlt (apply_fun d (apply_fun fnn x,apply_fun fnn u)) eps1.

An exact proof term for the current goal is (open_ballE2 Y d (apply_fun fnn x) eps1 (apply_fun fnn u) HuBalln).

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

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

We prove the intermediate claim Hdfnfx: Rlt (apply_fun d (apply_fun fnn x,apply_fun f x)) eps1.

An exact proof term for the current goal is (HNxprop n HnO HNxn).

We prove the intermediate claim Hsym_fnn_fx: apply_fun d (apply_fun fnn x,apply_fun f x) = apply_fun d (apply_fun f x,apply_fun fnn x).

An exact proof term for the current goal is (metric_on_symmetric Y d (apply_fun fnn x) (apply_fun f x) HmY HfnxY HfxY).

We prove the intermediate claim Hdfxfn: Rlt (apply_fun d (apply_fun f x,apply_fun fnn x)) eps1.

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

An exact proof term for the current goal is Hdfnfx.

We prove the intermediate claim HuA1: u ∈ A_N_eps X Y d fn N1 eps1.

An exact proof term for the current goal is (HU1subA u HuU1).

We prove the intermediate claim Htailu: ∀n0 : set, n0 ∈ ω → N1 ⊆ n0 → ∀m0 : set, m0 ∈ ω → N1 ⊆ m0 → Rle (apply_fun d (apply_fun (apply_fun fn n0) u,apply_fun (apply_fun fn m0) u)) eps1.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀n0 : set, n0 ∈ ω → N1 ⊆ n0 → ∀m0 : set, m0 ∈ ω → N1 ⊆ m0 → Rle (apply_fun d (apply_fun (apply_fun fn n0) x0,apply_fun (apply_fun fn m0) x0)) eps1) u HuA1).

We prove the intermediate claim HexNu: ∃Nu : set, Nu ∈ ω ∧ ∀k : set, k ∈ ω → Nu ⊆ k → Rlt (apply_fun d (apply_fun (apply_fun fn k) u,apply_fun f u)) eps1.

An exact proof term for the current goal is (Hlim u HuX eps1 Heps1R Heps1Pos).

Apply HexNu to the current goal.

Let Nu be given.

Assume HNuPair.

We prove the intermediate claim HNuO: Nu ∈ ω.

An exact proof term for the current goal is (andEL (Nu ∈ ω) (∀k : set, k ∈ ω → Nu ⊆ k → Rlt (apply_fun d (apply_fun (apply_fun fn k) u,apply_fun f u)) eps1) HNuPair).

We prove the intermediate claim HNuProp: ∀k : set, k ∈ ω → Nu ⊆ k → Rlt (apply_fun d (apply_fun (apply_fun fn k) u,apply_fun f u)) eps1.

An exact proof term for the current goal is (andER (Nu ∈ ω) (∀k : set, k ∈ ω → Nu ⊆ k → Rlt (apply_fun d (apply_fun (apply_fun fn k) u,apply_fun f u)) eps1) HNuPair).

Set Mmax2 to be the term n ∪ Nu.

We prove the intermediate claim HMmax2O: Mmax2 ∈ ω.

An exact proof term for the current goal is (omega_binunion n Nu HnO HNuO).

Set m to be the term ordsucc Mmax2.

We prove the intermediate claim HmO: m ∈ ω.

An exact proof term for the current goal is (omega_ordsucc Mmax2 HMmax2O).

We prove the intermediate claim HnSubm: n ⊆ m.

An exact proof term for the current goal is (Subq_tra n Mmax2 m (binunion_Subq_1 n Nu) (ordsuccI1 Mmax2)).

We prove the intermediate claim HNuSubm: Nu ⊆ m.

An exact proof term for the current goal is (Subq_tra Nu Mmax2 m (binunion_Subq_2 n Nu) (ordsuccI1 Mmax2)).

We prove the intermediate claim HN1m: N1 ⊆ m.

An exact proof term for the current goal is (Subq_tra N1 n m HN1n HnSubm).

Set fnm to be the term apply_fun fn m.

We prove the intermediate claim Hmcont: continuous_map X Tx Y (metric_topology Y d) fnm.

An exact proof term for the current goal is (Hcont m HmO).

We prove the intermediate claim Hfnm: function_on fnm X Y.

An exact proof term for the current goal is (continuous_map_function_on X Tx Y (metric_topology Y d) fnm Hmcont).

We prove the intermediate claim HfmuY: apply_fun fnm u ∈ Y.

An exact proof term for the current goal is (Hfnm u HuX).

We prove the intermediate claim Hd_fmu_fu: Rlt (apply_fun d (apply_fun fnm u,apply_fun f u)) eps1.

An exact proof term for the current goal is (HNuProp m HmO HNuSubm).

We prove the intermediate claim Hd_fmu_fu_le: Rle (apply_fun d (apply_fun fnm u,apply_fun f u)) eps1.

An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (apply_fun fnm u,apply_fun f u)) eps1 Hd_fmu_fu).

We prove the intermediate claim Hd_fnu_fmu_le: Rle (apply_fun d (apply_fun fnn u,apply_fun fnm u)) eps1.

An exact proof term for the current goal is (Htailu n HnO HN1n m HmO HN1m).

We prove the intermediate claim Htri_n_u: Rle (apply_fun d (apply_fun fnn u,apply_fun f u)) (add_SNo (apply_fun d (apply_fun fnn u,apply_fun fnm u)) (apply_fun d (apply_fun fnm u,apply_fun f u))).

An exact proof term for the current goal is (metric_triangle_Rle Y d (apply_fun fnn u) (apply_fun fnm u) (apply_fun f u) HmY HfnnuY HfmuY HfuY).

We prove the intermediate claim Hsum_le: Rle (add_SNo (apply_fun d (apply_fun fnn u,apply_fun fnm u)) (apply_fun d (apply_fun fnm u,apply_fun f u))) (add_SNo eps1 eps1).

Set d1 to be the term apply_fun d (apply_fun fnn u,apply_fun fnm u).

Set d2 to be the term apply_fun d (apply_fun fnm u,apply_fun f u).

We prove the intermediate claim Hd1le: Rle d1 eps1.

An exact proof term for the current goal is Hd_fnu_fmu_le.

We prove the intermediate claim Hd2le: Rle d2 eps1.

An exact proof term for the current goal is Hd_fmu_fu_le.

We prove the intermediate claim Hd1R: d1 ∈ R.

An exact proof term for the current goal is (RleE_left d1 eps1 Hd1le).

We prove the intermediate claim Hd2R: d2 ∈ R.

An exact proof term for the current goal is (RleE_left d2 eps1 Hd2le).

We prove the intermediate claim Hd1S: SNo d1.

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

We prove the intermediate claim Hd2S: SNo d2.

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

We prove the intermediate claim Heps1S: SNo eps1.

An exact proof term for the current goal is (real_SNo eps1 Heps1R).

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

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

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

We prove the intermediate claim HstepA: Rle (add_SNo d2 d1) (add_SNo d2 eps1).

An exact proof term for the current goal is (Rle_add_SNo_2 d2 d1 eps1 Hd2R Hd1R Heps1R Hd1le).

We prove the intermediate claim Hcomm2: add_SNo d2 eps1 = add_SNo eps1 d2.

An exact proof term for the current goal is (add_SNo_com d2 eps1 Hd2S Heps1S).

We prove the intermediate claim HstepA': Rle (add_SNo d2 d1) (add_SNo eps1 d2).

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

An exact proof term for the current goal is HstepA.

We prove the intermediate claim HstepB: Rle (add_SNo eps1 d2) (add_SNo eps1 eps1).

An exact proof term for the current goal is (Rle_add_SNo_2 eps1 d2 eps1 Heps1R Hd2R Heps1R Hd2le).

An exact proof term for the current goal is (Rle_tra (add_SNo d2 d1) (add_SNo eps1 d2) (add_SNo eps1 eps1) HstepA' HstepB).

We prove the intermediate claim Hd_fnu_fu_le2: Rle (apply_fun d (apply_fun fnn u,apply_fun f u)) (add_SNo eps1 eps1).

An exact proof term for the current goal is (Rle_tra (apply_fun d (apply_fun fnn u,apply_fun f u)) (add_SNo (apply_fun d (apply_fun fnn u,apply_fun fnm u)) (apply_fun d (apply_fun fnm u,apply_fun f u))) (add_SNo eps1 eps1) Htri_n_u Hsum_le).

Set a to be the term apply_fun d (apply_fun f x,apply_fun fnn x).

Set b to be the term apply_fun d (apply_fun fnn x,apply_fun fnn u).

Set c to be the term apply_fun d (apply_fun fnn u,apply_fun f u).

We prove the intermediate claim Ha_le: Rle a eps1.

An exact proof term for the current goal is (Rlt_implies_Rle a eps1 Hdfxfn).

We prove the intermediate claim Hb_le: Rle b eps1.

An exact proof term for the current goal is (Rlt_implies_Rle b eps1 Hdfnn).

We prove the intermediate claim Hc_le: Rle c (add_SNo eps1 eps1).

An exact proof term for the current goal is Hd_fnu_fu_le2.

Set y to be the term apply_fun d (apply_fun fnn x,apply_fun f u).

We prove the intermediate claim Htri_y: Rle y (add_SNo b c).

An exact proof term for the current goal is (metric_triangle_Rle Y d (apply_fun fnn x) (apply_fun fnn u) (apply_fun f u) HmY HfnxY HfnnuY HfuY).

We prove the intermediate claim Htri_x: Rle (apply_fun d (apply_fun f x,apply_fun f u)) (add_SNo a y).

An exact proof term for the current goal is (metric_triangle_Rle Y d (apply_fun f x) (apply_fun fnn x) (apply_fun f u) HmY HfxY HfnxY HfuY).

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (RleE_left a eps1 Ha_le).

We prove the intermediate claim HbR: b ∈ R.

An exact proof term for the current goal is (RleE_left b eps1 Hb_le).

We prove the intermediate claim HcR: c ∈ R.

An exact proof term for the current goal is (RleE_left c (add_SNo eps1 eps1) Hc_le).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (RleE_left y (add_SNo b c) Htri_y).

We prove the intermediate claim HbcR: add_SNo b c ∈ R.

An exact proof term for the current goal is (RleE_right y (add_SNo b c) Htri_y).

We prove the intermediate claim Hstep_xy: Rle (add_SNo a y) (add_SNo a (add_SNo b c)).

An exact proof term for the current goal is (Rle_add_SNo_2 a y (add_SNo b c) HaR HyR HbcR Htri_y).

We prove the intermediate claim Hd_le_abc: Rle (apply_fun d (apply_fun f x,apply_fun f u)) (add_SNo a (add_SNo b c)).

An exact proof term for the current goal is (Rle_tra (apply_fun d (apply_fun f x,apply_fun f u)) (add_SNo a y) (add_SNo a (add_SNo b c)) Htri_x Hstep_xy).

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 HcS: SNo c.

An exact proof term for the current goal is (real_SNo c HcR).

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 Hcomm_bc: add_SNo b c = add_SNo c b.

An exact proof term for the current goal is (add_SNo_com b c HbS HcS).

Set t to be the term add_SNo eps1 (add_SNo eps1 eps1).

We prove the intermediate claim HtR: t ∈ R.

An exact proof term for the current goal is (real_add_SNo eps1 Heps1R (add_SNo eps1 eps1) (real_add_SNo eps1 Heps1R eps1 Heps1R)).

We prove the intermediate claim Hbc_le_t: Rle (add_SNo b c) t.

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

We prove the intermediate claim Hstep1: Rle (add_SNo c b) (add_SNo c eps1).

An exact proof term for the current goal is (Rle_add_SNo_2 c b eps1 HcR HbR Heps1R Hb_le).

We prove the intermediate claim Hcomm_c: add_SNo c eps1 = add_SNo eps1 c.

An exact proof term for the current goal is (add_SNo_com c eps1 HcS Heps1S).

We prove the intermediate claim Hstep1': Rle (add_SNo c b) (add_SNo eps1 c).

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

An exact proof term for the current goal is Hstep1.

We prove the intermediate claim HccR: 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 Hstep2: Rle (add_SNo eps1 c) t.

An exact proof term for the current goal is (Rle_add_SNo_2 eps1 c (add_SNo eps1 eps1) Heps1R HcR HccR Hc_le).

An exact proof term for the current goal is (Rle_tra (add_SNo c b) (add_SNo eps1 c) t Hstep1' Hstep2).

We prove the intermediate claim Habct: Rle (add_SNo a (add_SNo b c)) (add_SNo a t).

An exact proof term for the current goal is (Rle_add_SNo_2 a (add_SNo b c) t HaR HbcR HtR Hbc_le_t).

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 HtS: SNo t.

An exact proof term for the current goal is (real_SNo t HtR).

We prove the intermediate claim Hcomm_at: add_SNo a t = add_SNo t a.

An exact proof term for the current goal is (add_SNo_com a t HaS HtS).

We prove the intermediate claim HstepA: Rle (add_SNo t a) (add_SNo t eps1).

An exact proof term for the current goal is (Rle_add_SNo_2 t a eps1 HtR HaR Heps1R Ha_le).

We prove the intermediate claim Hcomm_te: add_SNo t eps1 = add_SNo eps1 t.

An exact proof term for the current goal is (add_SNo_com t eps1 HtS Heps1S).

We prove the intermediate claim Hat_le: Rle (add_SNo a t) (add_SNo eps1 t).

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

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

An exact proof term for the current goal is HstepA.

We prove the intermediate claim Hd_le_et: Rle (apply_fun d (apply_fun f x,apply_fun f u)) (add_SNo eps1 t).

An exact proof term for the current goal is (Rle_tra (apply_fun d (apply_fun f x,apply_fun f u)) (add_SNo a (add_SNo b c)) (add_SNo eps1 t) Hd_le_abc (Rle_tra (add_SNo a (add_SNo b c)) (add_SNo a t) (add_SNo eps1 t) Habct Hat_le)).

We prove the intermediate claim Heps11R: 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 Heps11S: SNo (add_SNo eps1 eps1).

An exact proof term for the current goal is (real_SNo (add_SNo eps1 eps1) Heps11R).

We prove the intermediate claim Hassoc: add_SNo eps1 t = add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1).

rewrite the current goal using (add_SNo_assoc eps1 eps1 (add_SNo eps1 eps1) Heps1S Heps1S Heps11S) (from left to right).

Use reflexivity.

We prove the intermediate claim Hd_le_s4: Rle (apply_fun d (apply_fun f x,apply_fun f u)) (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)).

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

An exact proof term for the current goal is Hd_le_et.

An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (apply_fun f x,apply_fun f u)) (add_SNo (add_SNo eps1 eps1) (add_SNo eps1 eps1)) eps0 Hd_le_s4 H4lt).

Apply HballSubV to the current goal.

An exact proof term for the current goal is HballGoal.