Let b be given.

Assume HbB: b ∈ B.

We will prove preimage_of X f b ∈ Tx.

Apply (famunionE_impred Y (λc : set ⇒ {open_ball Y d c r|r ∈ R, Rlt 0 r}) b HbB (preimage_of X f b ∈ Tx)) 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 (preimage_of X f b ∈ Tx)) 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.

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

Set A0 to be the term preimage_of X f (open_ball Y d c r).

We prove the intermediate claim HA0subX: A0 ⊆ X.

Let x be given.

Assume Hx: x ∈ A0.

An exact proof term for the current goal is (SepE1 X (λu ⇒ apply_fun f u ∈ open_ball Y d c r) x Hx).

We prove the intermediate claim Hlocal: ∀x0 : set, x0 ∈ A0 → ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A0.

Let x0 be given.

Assume Hx0A0: x0 ∈ A0.

We will prove ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A0.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (HA0subX x0 Hx0A0).

We prove the intermediate claim Hfx0Ball: apply_fun f x0 ∈ open_ball Y d c r.

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ open_ball Y d c r) x0 Hx0A0).

We prove the intermediate claim Hfx0Y: apply_fun f x0 ∈ Y.

An exact proof term for the current goal is (Hf x0 Hx0X).

We prove the intermediate claim Hexeps0: ∃eps0 : set, eps0 ∈ R ∧ Rlt 0 eps0 ∧ open_ball Y d (apply_fun f x0) eps0 ⊆ 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 x0) r HmY HcY Hfx0Y HrR Hrpos Hfx0Ball).

Apply Hexeps0 to the current goal.

Let eps0 be given.

Assume Heps0.

We prove the intermediate claim Heps0_12: eps0 ∈ R ∧ Rlt 0 eps0.

An exact proof term for the current goal is (andEL (eps0 ∈ R ∧ Rlt 0 eps0) (open_ball Y d (apply_fun f x0) eps0 ⊆ open_ball Y d c r) Heps0).

We prove the intermediate claim Heps0R: eps0 ∈ R.

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

We prove the intermediate claim Heps0pos: Rlt 0 eps0.

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

We prove the intermediate claim Hballsub: open_ball Y d (apply_fun f x0) eps0 ⊆ open_ball Y d c r.

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

We prove the intermediate claim HexN0: ∃N0 ∈ ω, eps_ N0 < eps0.

An exact proof term for the current goal is (exists_eps_lt_pos eps0 Heps0R Heps0pos).

Apply HexN0 to the current goal.

Let N0 be given.

Assume HN0pair.

We prove the intermediate claim HN0omega: N0 ∈ ω.

An exact proof term for the current goal is (andEL (N0 ∈ ω) (eps_ N0 < eps0) HN0pair).

We prove the intermediate claim HepsN0lt: eps_ N0 < eps0.

An exact proof term for the current goal is (andER (N0 ∈ ω) (eps_ N0 < eps0) HN0pair).

We prove the intermediate claim HN0nat: nat_p N0.

An exact proof term for the current goal is (omega_nat_p N0 HN0omega).

We prove the intermediate claim Hsucc0: ordsucc N0 ∈ ω.

An exact proof term for the current goal is (omega_ordsucc N0 HN0omega).

We prove the intermediate claim Hsucc1: ordsucc (ordsucc N0) ∈ ω.

An exact proof term for the current goal is (omega_ordsucc (ordsucc N0) Hsucc0).

Set eta to be the term eps_ (ordsucc (ordsucc N0)).

We prove the intermediate claim HetaR: eta ∈ R.

An exact proof term for the current goal is (SNoS_omega_real eta (SNo_eps_SNoS_omega (ordsucc (ordsucc N0)) Hsucc1)).

We prove the intermediate claim HetaS: SNo eta.

An exact proof term for the current goal is (SNo_eps_ (ordsucc (ordsucc N0)) Hsucc1).

We prove the intermediate claim H0lt_etaS: 0 < eta.

An exact proof term for the current goal is (SNo_eps_pos (ordsucc (ordsucc N0)) Hsucc1).

We prove the intermediate claim HetaPos: Rlt 0 eta.

An exact proof term for the current goal is (RltI 0 eta real_0 HetaR H0lt_etaS).

We prove the intermediate claim HexNu: ∃Nu : set, Nu ∈ ω ∧ ∀n : set, n ∈ ω → Nu ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eta.

An exact proof term for the current goal is (Hunif eta HetaR HetaPos).

Apply HexNu to the current goal.

Let Nu be given.

Assume HNupair.

We prove the intermediate claim HNuomega: Nu ∈ ω.

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

We prove the intermediate claim HNuprop: ∀n : set, n ∈ ω → Nu ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eta.

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

Set fn0 to be the term apply_fun fn Nu.

We prove the intermediate claim Hfn0cont: continuous_map X Tx Y (metric_topology Y d) fn0.

An exact proof term for the current goal is (Hcont Nu HNuomega).

We prove the intermediate claim Hfn0: function_on fn0 X Y.

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

We prove the intermediate claim Hfn0x0Y: apply_fun fn0 x0 ∈ Y.

An exact proof term for the current goal is (Hfn0 x0 Hx0X).

We prove the intermediate claim Hball0open: open_ball Y d (apply_fun fn0 x0) eta ∈ metric_topology Y d.

An exact proof term for the current goal is (open_ball_in_metric_topology Y d (apply_fun fn0 x0) eta HmY Hfn0x0Y HetaPos).

Set U0 to be the term preimage_of X fn0 (open_ball Y d (apply_fun fn0 x0) eta).

We prove the intermediate claim HU0Tx: U0 ∈ Tx.

An exact proof term for the current goal is (continuous_map_preimage X Tx Y (metric_topology Y d) fn0 Hfn0cont (open_ball Y d (apply_fun fn0 x0) eta) Hball0open).

We prove the intermediate claim Hx0U0: x0 ∈ U0.

We prove the intermediate claim HU0def: U0 = preimage_of X fn0 (open_ball Y d (apply_fun fn0 x0) eta).

Use reflexivity.

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

We prove the intermediate claim Hpredef: preimage_of X fn0 (open_ball Y d (apply_fun fn0 x0) eta) = {u ∈ X|apply_fun fn0 u ∈ open_ball Y d (apply_fun fn0 x0) eta}.

Use reflexivity.

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

Apply (SepI X (λu : set ⇒ apply_fun fn0 u ∈ open_ball Y d (apply_fun fn0 x0) eta) x0 Hx0X) to the current goal.

An exact proof term for the current goal is (center_in_open_ball Y d (apply_fun fn0 x0) eta HmY Hfn0x0Y HetaPos).

We prove the intermediate claim HU0subA0: U0 ⊆ A0.

Let x be given.

Assume HxU0: x ∈ U0.

We will prove x ∈ A0.

We prove the intermediate claim HU0def: U0 = preimage_of X fn0 (open_ball Y d (apply_fun fn0 x0) eta).

Use reflexivity.

We prove the intermediate claim HxU0': x ∈ preimage_of X fn0 (open_ball Y d (apply_fun fn0 x0) eta).

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

An exact proof term for the current goal is HxU0.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun fn0 u ∈ open_ball Y d (apply_fun fn0 x0) eta) x HxU0').

We prove the intermediate claim Hfn0xBall: apply_fun fn0 x ∈ open_ball Y d (apply_fun fn0 x0) eta.

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

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 fn0 x,apply_fun f x)) eta.

An exact proof term for the current goal is (HNuprop Nu HNuomega (Subq_ref Nu) x HxX).

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

We prove the intermediate claim Hsym: apply_fun d (apply_fun f x,apply_fun fn0 x) = apply_fun d (apply_fun fn0 x,apply_fun f x).

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

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

An exact proof term for the current goal is Hdfnfx.

We prove the intermediate claim Hdfn0x0: Rlt (apply_fun d (apply_fun fn0 x0,apply_fun f x0)) eta.

An exact proof term for the current goal is (HNuprop Nu HNuomega (Subq_ref Nu) x0 Hx0X).

We prove the intermediate claim Hdfx0fn0: Rlt (apply_fun d (apply_fun f x0,apply_fun fn0 x0)) eta.

We prove the intermediate claim Hsym: apply_fun d (apply_fun f x0,apply_fun fn0 x0) = apply_fun d (apply_fun fn0 x0,apply_fun f x0).

An exact proof term for the current goal is (metric_on_symmetric Y d (apply_fun f x0) (apply_fun fn0 x0) HmY Hfx0Y Hfn0x0Y).

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

An exact proof term for the current goal is Hdfn0x0.

We prove the intermediate claim Hdfn0ball0: Rlt (apply_fun d (apply_fun fn0 x0,apply_fun fn0 x)) eta.

An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ Rlt (apply_fun d (apply_fun fn0 x0,y0)) eta) (apply_fun fn0 x) Hfn0xBall).

We prove the intermediate claim Hdfn0ball: Rlt (apply_fun d (apply_fun fn0 x,apply_fun fn0 x0)) eta.

We prove the intermediate claim Hsym: apply_fun d (apply_fun fn0 x,apply_fun fn0 x0) = apply_fun d (apply_fun fn0 x0,apply_fun fn0 x).

An exact proof term for the current goal is (metric_on_symmetric Y d (apply_fun fn0 x) (apply_fun fn0 x0) HmY (Hfn0 x HxX) Hfn0x0Y).

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

An exact proof term for the current goal is Hdfn0ball0.

Set p to be the term apply_fun d (apply_fun f x,apply_fun fn0 x).

Set q to be the term apply_fun d (apply_fun fn0 x,apply_fun fn0 x0).

Set r0 to be the term apply_fun d (apply_fun fn0 x0,apply_fun f x0).

We prove the intermediate claim HpR: p ∈ R.

An exact proof term for the current goal is ((metric_on_function_on Y d HmY) (apply_fun f x,apply_fun fn0 x) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun f x) (apply_fun fn0 x) HfxY (Hfn0 x HxX))).

We prove the intermediate claim HqR: q ∈ R.

An exact proof term for the current goal is ((metric_on_function_on Y d HmY) (apply_fun fn0 x,apply_fun fn0 x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun fn0 x) (apply_fun fn0 x0) (Hfn0 x HxX) Hfn0x0Y)).

We prove the intermediate claim HrR: r0 ∈ R.

An exact proof term for the current goal is ((metric_on_function_on Y d HmY) (apply_fun fn0 x0,apply_fun f x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun fn0 x0) (apply_fun f x0) Hfn0x0Y Hfx0Y)).

We prove the intermediate claim HpS: SNo p.

An exact proof term for the current goal is (real_SNo p HpR).

We prove the intermediate claim HqS: SNo q.

An exact proof term for the current goal is (real_SNo q HqR).

We prove the intermediate claim HrS: SNo r0.

An exact proof term for the current goal is (real_SNo r0 HrR).

We prove the intermediate claim HpLt: p < eta.

An exact proof term for the current goal is (RltE_lt p eta Hdfxfn).

We prove the intermediate claim HqLt: q < eta.

An exact proof term for the current goal is (RltE_lt q eta Hdfn0ball).

We prove the intermediate claim HrLt: r0 < eta.

An exact proof term for the current goal is (RltE_lt r0 eta Hdfn0x0).

We prove the intermediate claim Hsum_pqr_lt: add_SNo p (add_SNo q r0) < add_SNo eta (add_SNo eta eta).

An exact proof term for the current goal is (add_SNo_Lt4 p q r0 eta eta eta HpS HqS HrS HetaS HetaS HetaS HpLt HqLt HrLt).

We prove the intermediate claim Heta3S: SNo (add_SNo eta (add_SNo eta eta)).

An exact proof term for the current goal is (SNo_add_SNo_3 eta eta eta HetaS HetaS HetaS).

We prove the intermediate claim Heta3S_left: SNo (add_SNo (add_SNo eta eta) eta).

We prove the intermediate claim Heta2S: SNo (add_SNo eta eta).

An exact proof term for the current goal is (SNo_add_SNo eta eta HetaS HetaS).

An exact proof term for the current goal is (SNo_add_SNo (add_SNo eta eta) eta Heta2S HetaS).

We prove the intermediate claim HepsN0S: SNo (eps_ N0).

An exact proof term for the current goal is (real_SNo (eps_ N0) (SNoS_omega_real (eps_ N0) (SNo_eps_SNoS_omega N0 HN0omega))).

We prove the intermediate claim Heta_lt_eta2: eta < add_SNo eta eta.

We prove the intermediate claim H0S: SNo 0.

An exact proof term for the current goal is SNo_0.

We prove the intermediate claim Htmp: add_SNo eta 0 < add_SNo eta eta.

An exact proof term for the current goal is (add_SNo_Lt2 eta 0 eta HetaS H0S HetaS H0lt_etaS).

rewrite the current goal using (add_SNo_0R eta HetaS) (from right to left) at position 1.

An exact proof term for the current goal is Htmp.

We prove the intermediate claim Heta3lt_4eta: add_SNo (add_SNo eta eta) eta < add_SNo (add_SNo eta eta) (add_SNo eta eta).

An exact proof term for the current goal is (add_SNo_Lt2 (add_SNo eta eta) eta (add_SNo eta eta) (SNo_add_SNo eta eta HetaS HetaS) HetaS (SNo_add_SNo eta eta HetaS HetaS) Heta_lt_eta2).

We prove the intermediate claim H4eta_eq_epsN0: add_SNo (add_SNo eta eta) (add_SNo eta eta) = eps_ N0.

We prove the intermediate claim Heq1: add_SNo eta eta = eps_ (ordsucc N0).

rewrite the current goal using (eps_ordsucc_half_add (ordsucc N0) (omega_nat_p (ordsucc N0) Hsucc0)) (from right to left).

Use reflexivity.

rewrite the current goal using Heq1 (from left to right) at position 1.

rewrite the current goal using (eps_ordsucc_half_add N0 HN0nat) (from right to left).

Use reflexivity.

We prove the intermediate claim Heta3lt_epsN0: add_SNo (add_SNo eta eta) eta < eps_ N0.

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

An exact proof term for the current goal is Heta3lt_4eta.

We prove the intermediate claim Heta3lt_eps0: add_SNo (add_SNo eta eta) eta < eps0.

An exact proof term for the current goal is (SNoLt_tra (add_SNo (add_SNo eta eta) eta) (eps_ N0) eps0 Heta3S_left HepsN0S (real_SNo eps0 Heps0R) Heta3lt_epsN0 HepsN0lt).

We prove the intermediate claim Hsumlt_eps0: add_SNo p (add_SNo q r0) < eps0.

We prove the intermediate claim Hmid: add_SNo eta (add_SNo eta eta) < eps0.

rewrite the current goal using (add_SNo_assoc eta eta eta HetaS HetaS HetaS) (from left to right).

An exact proof term for the current goal is Heta3lt_eps0.

An exact proof term for the current goal is (SNoLt_tra (add_SNo p (add_SNo q r0)) (add_SNo eta (add_SNo eta eta)) eps0 (SNo_add_SNo p (add_SNo q r0) HpS (SNo_add_SNo q r0 HqS HrS)) (SNo_add_SNo eta (add_SNo eta eta) HetaS (SNo_add_SNo eta eta HetaS HetaS)) (real_SNo eps0 Heps0R) Hsum_pqr_lt Hmid).

We prove the intermediate claim HsumR: add_SNo p (add_SNo q r0) ∈ R.

An exact proof term for the current goal is (real_add_SNo p HpR (add_SNo q r0) (real_add_SNo q HqR r0 HrR)).

We prove the intermediate claim HsumRlt: Rlt (add_SNo p (add_SNo q r0)) eps0.

An exact proof term for the current goal is (RltI (add_SNo p (add_SNo q r0)) eps0 HsumR Heps0R Hsumlt_eps0).

We prove the intermediate claim Htri1: Rle (apply_fun d (apply_fun f x,apply_fun f x0)) (add_SNo p (apply_fun d (apply_fun fn0 x,apply_fun f x0))).

An exact proof term for the current goal is (metric_triangle_Rle Y d (apply_fun f x) (apply_fun fn0 x) (apply_fun f x0) HmY HfxY (Hfn0 x HxX) Hfx0Y).

We prove the intermediate claim Htri2: Rle (apply_fun d (apply_fun fn0 x,apply_fun f x0)) (add_SNo q r0).

An exact proof term for the current goal is (metric_triangle_Rle Y d (apply_fun fn0 x) (apply_fun fn0 x0) (apply_fun f x0) HmY (Hfn0 x HxX) Hfn0x0Y Hfx0Y).

We prove the intermediate claim Hadd: Rle (add_SNo p (apply_fun d (apply_fun fn0 x,apply_fun f x0))) (add_SNo p (add_SNo q r0)).

An exact proof term for the current goal is (Rle_add_SNo_2 p (apply_fun d (apply_fun fn0 x,apply_fun f x0)) (add_SNo q r0) HpR ((metric_on_function_on Y d HmY) (apply_fun fn0 x,apply_fun f x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun fn0 x) (apply_fun f x0) (Hfn0 x HxX) Hfx0Y)) (real_add_SNo q HqR r0 HrR) Htri2).

We prove the intermediate claim Htri3: Rle (apply_fun d (apply_fun f x,apply_fun f x0)) (add_SNo p (add_SNo q r0)).

An exact proof term for the current goal is (Rle_tra (apply_fun d (apply_fun f x,apply_fun f x0)) (add_SNo p (apply_fun d (apply_fun fn0 x,apply_fun f x0))) (add_SNo p (add_SNo q r0)) Htri1 Hadd).

We prove the intermediate claim Hdlt: Rlt (apply_fun d (apply_fun f x,apply_fun f x0)) eps0.

An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (apply_fun f x,apply_fun f x0)) (add_SNo p (add_SNo q r0)) eps0 Htri3 HsumRlt).

We prove the intermediate claim Hsymd: apply_fun d (apply_fun f x0,apply_fun f x) = apply_fun d (apply_fun f x,apply_fun f x0).

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

We prove the intermediate claim Hdlt2: Rlt (apply_fun d (apply_fun f x0,apply_fun f x)) eps0.

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

An exact proof term for the current goal is Hdlt.

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

We prove the intermediate claim HdefBall: open_ball Y d (apply_fun f x0) eps0 = {y ∈ Y|Rlt (apply_fun d (apply_fun f x0,y)) eps0}.

Use reflexivity.

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

Apply (SepI Y (λy0 : set ⇒ Rlt (apply_fun d (apply_fun f x0,y0)) eps0) (apply_fun f x) HfxY) to the current goal.

An exact proof term for the current goal is Hdlt2.

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

An exact proof term for the current goal is (Hballsub (apply_fun f x) Hfx_in_refined).

We prove the intermediate claim HA0def: A0 = preimage_of X f (open_ball Y d c r).

Use reflexivity.

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

We prove the intermediate claim HpredefA0: preimage_of X f (open_ball Y d c r) = {u ∈ X|apply_fun f u ∈ open_ball Y d c r}.

Use reflexivity.

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

Apply (SepI X (λu : set ⇒ apply_fun f u ∈ open_ball Y d c r) x HxX) to the current goal.

An exact proof term for the current goal is Hfx_in_ball.

We use U0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU0Tx.

An exact proof term for the current goal is Hx0U0.

An exact proof term for the current goal is HU0subA0.

We prove the intermediate claim HA0subInt: A0 ⊆ interior_of X Tx A0.

Let x0 be given.

Assume Hx0A0: x0 ∈ A0.

We will prove x0 ∈ interior_of X Tx A0.

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (HA0subX x0 Hx0A0).

We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A0.

An exact proof term for the current goal is (Hlocal x0 Hx0A0).

Apply HexU to the current goal.

Let U be given.

Assume HUconj.

We prove the intermediate claim HUand: U ∈ Tx ∧ x0 ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x0 ∈ U) (U ⊆ A0) HUconj).

We prove the intermediate claim HUsub: U ⊆ A0.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ x0 ∈ U) (U ⊆ A0) HUconj).

We prove the intermediate claim HU: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (x0 ∈ U) HUand).

We prove the intermediate claim Hx0U: x0 ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx) (x0 ∈ U) HUand).

We prove the intermediate claim HdefInt: interior_of X Tx A0 = {x ∈ X|∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ A0}.

Use reflexivity.

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

Apply (SepI X (λx : set ⇒ ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ A0) x0 Hx0X) 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 HU.

An exact proof term for the current goal is Hx0U.

An exact proof term for the current goal is HUsub.

We prove the intermediate claim HintSub: interior_of X Tx A0 ⊆ A0.

An exact proof term for the current goal is (interior_subset X Tx A0 HTx).

We prove the intermediate claim HeqA0: A0 = interior_of X Tx A0.

Apply set_ext to the current goal.

An exact proof term for the current goal is HA0subInt.

An exact proof term for the current goal is HintSub.

We prove the intermediate claim HintOpen: interior_of X Tx A0 ∈ Tx.

An exact proof term for the current goal is (interior_is_open X Tx A0 HTx HA0subX).

We prove the intermediate claim HA0def: preimage_of X f (open_ball Y d c r) = A0.

Use reflexivity.

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

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

An exact proof term for the current goal is HintOpen.