Let m be given.
We will prove completely_regular_space (euclidean_space m) (euclidean_topology m).
We prove the intermediate claim HRtop: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
Apply (andER (∀Y : set, Y ⊆ R → completely_regular_space R R_standard_topology → completely_regular_space Y (subspace_topology R R_standard_topology Y)) (∀I Xi : set, completely_regular_spaces_family I Xi → completely_regular_space (product_space I Xi) (product_topology_full I Xi)) (completely_regular_subspace_product R R_standard_topology HRtop) m (const_space_family m R R_standard_topology)) to the current goal.
We prove the intermediate claim Hfam: completely_regular_spaces_family m (const_space_family m R R_standard_topology).
Let i be given.
Assume Hi: i ∈ m.
We will prove completely_regular_space (product_component (const_space_family m R R_standard_topology) i) (product_component_topology (const_space_family m R R_standard_topology) i).
rewrite the current goal using (product_component_def (const_space_family m R R_standard_topology) i) (from left to right).
rewrite the current goal using (product_component_topology_def (const_space_family m R R_standard_topology) i) (from left to right).
rewrite the current goal using (const_space_family_apply m R R_standard_topology i Hi) (from left to right).
rewrite the current goal using (tuple_2_0_eq R R_standard_topology) (from left to right).
rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).
An exact proof term for the current goal is R_standard_topology_completely_regular.
An exact proof term for the current goal is Hfam.
∎