Let i be given.
Assume Hi3: i ∈ 3.
We will prove space_family_set (const_space_family 3 R R_standard_topology) i = R.
Set Xi to be the term const_space_family 3 R R_standard_topology.
We prove the intermediate claim HXi: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply 3 R R_standard_topology i Hi3).
We will prove (apply_fun Xi i) 0 = R.
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
∎