We will prove subspace_topology (setprod R R) R2_standard_topology ordered_square = product_topology unit_interval unit_interval_topology unit_interval unit_interval_topology.
We prove the intermediate claim Hsq: ordered_square = setprod unit_interval unit_interval.
Use reflexivity.
We prove the intermediate claim Hut: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
rewrite the current goal using Hsq (from left to right).
rewrite the current goal using Hut (from left to right).
rewrite the current goal using R2_standard_equals_product (from left to right).
rewrite the current goal using (product_subspace_topology R R_standard_topology R R_standard_topology unit_interval unit_interval R_standard_topology_is_topology R_standard_topology_is_topology unit_interval_sub_R unit_interval_sub_R) (from left to right).
Use reflexivity.
∎