Let y be given.
Assume HyR: y ∈ R.
We will prove y ∈ space_family_union 3 (const_space_family 3 R R_standard_topology).
Set Xi to be the term const_space_family 3 R R_standard_topology.
Set S to be the term {space_family_set Xi i|i ∈ 3}.
We will prove y ∈ ⋃ S.
We prove the intermediate claim H2in3: 2 ∈ 3.
An exact proof term for the current goal is In_2_3.
We prove the intermediate claim HXi2: apply_fun Xi 2 = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply 3 R R_standard_topology 2 H2in3).
We prove the intermediate claim HSf2: space_family_set Xi 2 = R.
We will prove (apply_fun Xi 2) 0 = R.
rewrite the current goal using HXi2 (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
We prove the intermediate claim Helt: space_family_set Xi 2 ∈ S.
An exact proof term for the current goal is (ReplI 3 (λi : set ⇒ space_family_set Xi i) 2 H2in3).
We prove the intermediate claim HySf2: y ∈ space_family_set Xi 2.
rewrite the current goal using HSf2 (from left to right).
An exact proof term for the current goal is HyR.
An exact proof term for the current goal is (UnionI S y (space_family_set Xi 2) HySf2 Helt).
∎