Let V be given.

Assume HV: V ∈ Ty.

We will prove preimage_of X g V ∈ Tx.

Set U to be the term preimage_of X g V.

We prove the intermediate claim HUSubX: U ⊆ X.

Let x be given.

Assume HxU: x ∈ U.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun g x0 ∈ V) x HxU).

Apply (topology_elem_of_local_neighborhoods X Tx U HTx HUSubX) to the current goal.

Let x0 be given.

Assume Hx0U: x0 ∈ U.

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

We prove the intermediate claim Hx0X: x0 ∈ X.

An exact proof term for the current goal is (SepE1 X (λx1 : set ⇒ apply_fun g x1 ∈ V) x0 Hx0U).

We prove the intermediate claim Hgx0V: apply_fun g x0 ∈ V.

An exact proof term for the current goal is (SepE2 X (λx1 : set ⇒ apply_fun g x1 ∈ V) x0 Hx0U).

We prove the intermediate claim Hgx0Y: apply_fun g x0 ∈ Y.

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

We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball Y dY (apply_fun g x0) r ⊆ V).

An exact proof term for the current goal is (metric_topology_neighborhood_contains_ball Y dY (apply_fun g x0) V HdY Hgx0Y HV Hgx0V).

Apply Hexr to the current goal.

Let r be given.

Assume Hrpack: r ∈ R ∧ (Rlt 0 r ∧ open_ball Y dY (apply_fun g x0) r ⊆ V).

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 Y dY (apply_fun g x0) r ⊆ V) Hrpack).

We prove the intermediate claim Hrmid: Rlt 0 r ∧ open_ball Y dY (apply_fun g x0) r ⊆ V.

An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ open_ball Y dY (apply_fun g x0) r ⊆ V) Hrpack).

We prove the intermediate claim Hrpos: r ∈ R ∧ Rlt 0 r.

Apply andI to the current goal.

An exact proof term for the current goal is HrR.

An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball Y dY (apply_fun g x0) r ⊆ V) Hrmid).

We prove the intermediate claim HballSubV: open_ball Y dY (apply_fun g x0) r ⊆ V.

An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball Y dY (apply_fun g x0) r ⊆ V) Hrmid).

We prove the intermediate claim HexW: ∃W : set, W ∈ Tx ∧ x0 ∈ W ∧ ∀g0 : set, g0 ∈ Ascoli_g_pointwise_closure X Tx Y dY F → ∀x1 : set, x1 ∈ X → x1 ∈ W → Rlt (apply_fun dY (apply_fun g0 x1,apply_fun g0 x0)) r.

An exact proof term for the current goal is (Ascoli_g_pointwise_closure_equicontinuous_bound X Tx Y dY F x0 r HTx HdY HFsubC Hequi Hx0X Hrpos).

Apply HexW to the current goal.

Let W be given.

Assume HWpack.

We use W to witness the existential quantifier.

We prove the intermediate claim HWcore: W ∈ Tx ∧ x0 ∈ W.

An exact proof term for the current goal is (andEL (W ∈ Tx ∧ x0 ∈ W) (∀g0 : set, g0 ∈ Ascoli_g_pointwise_closure X Tx Y dY F → ∀x1 : set, x1 ∈ X → x1 ∈ W → Rlt (apply_fun dY (apply_fun g0 x1,apply_fun g0 x0)) r) HWpack).

We prove the intermediate claim HWT: W ∈ Tx.

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

We prove the intermediate claim Hx0W: x0 ∈ W.

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

Apply andI to the current goal.

An exact proof term for the current goal is HWT.

An exact proof term for the current goal is Hx0W.

Let x1 be given.

Assume Hx1W: x1 ∈ W.

We will prove x1 ∈ U.

We will prove x1 ∈ {x ∈ X|apply_fun g x ∈ V}.

We prove the intermediate claim Hx1X: x1 ∈ X.

An exact proof term for the current goal is (topology_elem_subset X Tx W HTx HWT x1 Hx1W).

Apply (SepI X (λx2 : set ⇒ apply_fun g x2 ∈ V) x1 Hx1X) to the current goal.

We prove the intermediate claim Hineq: Rlt (apply_fun dY (apply_fun g x1,apply_fun g x0)) r.

We prove the intermediate claim Htail: ∀g0 : set, g0 ∈ Ascoli_g_pointwise_closure X Tx Y dY F → ∀x2 : set, x2 ∈ X → x2 ∈ W → Rlt (apply_fun dY (apply_fun g0 x2,apply_fun g0 x0)) r.

An exact proof term for the current goal is (andER (W ∈ Tx ∧ x0 ∈ W) (∀g0 : set, g0 ∈ Ascoli_g_pointwise_closure X Tx Y dY F → ∀x2 : set, x2 ∈ X → x2 ∈ W → Rlt (apply_fun dY (apply_fun g0 x2,apply_fun g0 x0)) r) HWpack).

An exact proof term for the current goal is (Htail g Hgcl x1 Hx1X Hx1W).

We prove the intermediate claim Hball: apply_fun g x1 ∈ open_ball Y dY (apply_fun g x0) r.

We prove the intermediate claim Hgx1Y: apply_fun g x1 ∈ Y.

An exact proof term for the current goal is (Hgfun x1 Hx1X).

We prove the intermediate claim Hgx0Y: apply_fun g x0 ∈ Y.

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

We prove the intermediate claim Hsym: apply_fun dY (apply_fun g x0,apply_fun g x1) = apply_fun dY (apply_fun g x1,apply_fun g x0).

An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun g x0) (apply_fun g x1) HdY Hgx0Y Hgx1Y).

We prove the intermediate claim Hineq2: Rlt (apply_fun dY (apply_fun g x0,apply_fun g x1)) r.

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

An exact proof term for the current goal is Hineq.

An exact proof term for the current goal is (open_ballI Y dY (apply_fun g x0) r (apply_fun g x1) Hgx1Y Hineq2).

An exact proof term for the current goal is (HballSubV (apply_fun g x1) Hball).