We will prove metrizable R_omega_space R_omega_product_topology.
We will prove ∃d : set, metric_on R_omega_space d ∧ metric_topology R_omega_space d = R_omega_product_topology.
We use Romega_D_metric to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Romega_D_metric_induces_product_topology).
We prove the intermediate claim Heq: Romega_D_metric_topology = R_omega_product_topology.
An exact proof term for the current goal is (andER (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Romega_D_metric_induces_product_topology).
We prove the intermediate claim HdefT: Romega_D_metric_topology = metric_topology R_omega_space Romega_D_metric.
Use reflexivity.
rewrite the current goal using HdefT (from right to left).
An exact proof term for the current goal is Heq.
∎