Let n be given.
Assume HnO: n ∈ ω.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set X to be the term product_space ω Xi.
Set Tx to be the term box_topology ω Xi.
Set B to be the term box_basis ω Xi.
Set Y to be the term Romega_tilde n.
Set Ty to be the term subspace_topology X R_omega_product_topology Y.
We prove the intermediate claim HXeq: X = R_omega_space.
Use reflexivity.
We prove the intermediate claim HTxeq: Tx = R_omega_box_topology.
Use reflexivity.
rewrite the current goal using HXeq (from right to left).
rewrite the current goal using HTxeq (from right to left).
We will prove subspace_topology X Tx Y ⊆ subspace_topology X R_omega_product_topology Y.
We prove the intermediate claim HTxOn: topology_on X Tx.
Apply (box_topology_is_topology_on ω Xi) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove topology_on (space_family_set Xi i) (space_family_topology Xi i).
rewrite the current goal using (space_family_set_const_space_family ω R R_standard_topology i Hi) (from left to right).
rewrite the current goal using (space_family_topology_const_space_family ω R R_standard_topology i Hi) (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HYsubX: Y ⊆ X.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (Romega_tilde_sub_Romega n).
We prove the intermediate claim HBasis: basis_on X B.
Apply (box_basis_is_basis_on ω Xi) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove topology_on (space_family_set Xi i) (space_family_topology Xi i).
rewrite the current goal using (space_family_set_const_space_family ω R R_standard_topology i Hi) (from left to right).
rewrite the current goal using (space_family_topology_const_space_family ω R R_standard_topology i Hi) (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HBpair: basis_on X B ∧ generated_topology X B = Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HBasis.
Use reflexivity.
We prove the intermediate claim HsubBasis: basis_on Y {b0 ∩ Y|b0 ∈ B} ∧ generated_topology Y {b0 ∩ Y|b0 ∈ B} = subspace_topology X Tx Y.
An exact proof term for the current goal is (subspace_basis X Tx Y B HTxOn HYsubX HBpair).
We prove the intermediate claim HgenEq: generated_topology Y {b0 ∩ Y|b0 ∈ B} = subspace_topology X Tx Y.
An exact proof term for the current goal is (andER (basis_on Y {b0 ∩ Y|b0 ∈ B}) (generated_topology Y {b0 ∩ Y|b0 ∈ B} = subspace_topology X Tx Y) HsubBasis).
We prove the intermediate claim HTyOn: topology_on Y (subspace_topology X R_omega_product_topology Y).
We prove the intermediate claim HTprod: topology_on X R_omega_product_topology.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is Romega_product_topology_is_topology.
An exact proof term for the current goal is (subspace_topology_is_topology X R_omega_product_topology Y HTprod HYsubX).
We prove the intermediate claim HbasicSub: {b0 ∩ Y|b0 ∈ B} ⊆ subspace_topology X R_omega_product_topology Y.
Let U be given.
Assume HU: U ∈ {b0 ∩ Y|b0 ∈ B}.
We will prove U ∈ subspace_topology X R_omega_product_topology Y.
Apply (ReplE_impred B (λb0 : set ⇒ b0 ∩ Y) U HU (U ∈ subspace_topology X R_omega_product_topology Y)) to the current goal.
Let b0 be given.
Assume Hb0B: b0 ∈ B.
Assume HUeq: U = b0 ∩ Y.
rewrite the current goal using HUeq (from left to right).
rewrite the current goal using HXeq (from left to right).
We prove the intermediate claim HYeq: Y = Romega_tilde n.
Use reflexivity.
rewrite the current goal using HYeq (from left to right).
rewrite the current goal using HYeq (from left to right).
An exact proof term for the current goal is (Romega_box_basis_cap_Romega_tilde_in_product_subspace n b0 HnO Hb0B).
We prove the intermediate claim HgenSub: generated_topology Y {b0 ∩ Y|b0 ∈ B} ⊆ subspace_topology X R_omega_product_topology Y.
An exact proof term for the current goal is (generated_topology_finer_weak Y {b0 ∩ Y|b0 ∈ B} (subspace_topology X R_omega_product_topology Y) HTyOn HbasicSub).
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HgenSub.
∎