We will prove first_countable_space real_sequences uniform_topology ∧ ¬ second_countable_space real_sequences uniform_topology.
Apply andI to the current goal.
An exact proof term for the current goal is uniform_topology_first_countable.
Assume Hsc: second_countable_space real_sequences uniform_topology.
We will prove False.
We prove the intermediate claim Hdisc: discrete_subspace real_sequences uniform_topology binary_sequences_Romega.
An exact proof term for the current goal is binary_sequences_Romega_discrete_in_uniform_topology.
We prove the intermediate claim Hcount: countable_set binary_sequences_Romega.
An exact proof term for the current goal is (second_countable_discrete_subspace_countable real_sequences uniform_topology binary_sequences_Romega Hsc Hdisc).
An exact proof term for the current goal is (binary_sequences_Romega_uncountable Hcount).
∎