We will prove paracompact_space real_sequences uniform_topology.
We prove the intermediate claim Hmetr: metrizable real_sequences uniform_topology.
We will prove ∃d : set, metric_on real_sequences d ∧ metric_topology real_sequences d = uniform_topology.
We use uniform_metric_Romega to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is uniform_metric_Romega_is_metric.
We prove the intermediate claim Hdef: uniform_topology = metric_topology real_sequences uniform_metric_Romega.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Use reflexivity.
An exact proof term for the current goal is (metrizable_paracompact real_sequences uniform_topology Hmetr).
∎