Let X, Tx, U and V be given.

Assume HUcov: open_cover X Tx U.

Assume HPV: partition_of_unity_dominated X Tx V.

Assume Href: refine_of V U.

We will prove partition_of_unity_dominated X Tx U.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (partition_of_unity_dominated_topology X Tx V HPV).

We will prove topology_on X Tx ∧ open_cover X Tx U ∧ ∃P : set, partition_of_unity_family X Tx U P.

Apply andI to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HUcov.

Apply (partition_of_unity_dominated_ex_family_pred X Tx V HPV) to the current goal.

Let P be given.

Assume HPfamV: partition_of_unity_family X Tx V P.

We use P to witness the existential quantifier.

An exact proof term for the current goal is (partition_of_unity_family_refine X Tx U V P HPfamV Href).

∎