We will prove topology_on real_sequences uniform_topology.

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).

An exact proof term for the current goal is (metric_topology_is_topology real_sequences uniform_metric_Romega uniform_metric_Romega_is_metric).

∎