Let X, Tx, Y, Ty and x0 be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume Hx0X: x0 ∈ X.
Set idY to be the term {(y,y)|y ∈ Y}.
Set c to be the term const_fun Y x0.
Set f to be the term pair_map Y c idY.
Set Slice to be the term setprod {x0} Y.
Set Tslice to be the term subspace_topology (setprod X Y) (product_topology X Tx Y Ty) Slice.
We prove the intermediate claim HTprod: topology_on (setprod X Y) (product_topology X Tx Y Ty).
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim Hc: continuous_map Y Ty X Tx c.
An exact proof term for the current goal is (const_fun_continuous Y Ty X Tx x0 HTy HTx Hx0X).
We prove the intermediate claim Hid: continuous_map Y Ty Y Ty idY.
An exact proof term for the current goal is (identity_continuous Y Ty HTy).
We prove the intermediate claim HfProd: continuous_map Y Ty (setprod X Y) (product_topology X Tx Y Ty) f.
An exact proof term for the current goal is (maps_into_products Y Ty X Tx Y Ty c idY Hc Hid).
We prove the intermediate claim HSingSub: {x0} ⊆ X.
An exact proof term for the current goal is (singleton_subset x0 X Hx0X).
We prove the intermediate claim HSlicesub: Slice ⊆ setprod X Y.
An exact proof term for the current goal is (setprod_Subq {x0} Y X Y HSingSub (Subq_ref Y)).
We prove the intermediate claim Himg: ∀y : set, y ∈ Y → apply_fun f y ∈ Slice.
Let y be given.
Assume HyY: y ∈ Y.
We will prove apply_fun f y ∈ Slice.
We prove the intermediate claim Happ: apply_fun f y = (apply_fun c y,apply_fun idY y).
An exact proof term for the current goal is (pair_map_apply Y X Y c idY y HyY).
We prove the intermediate claim Hcapp: apply_fun c y = x0.
An exact proof term for the current goal is (const_fun_apply Y x0 y HyY).
We prove the intermediate claim Hidapp: apply_fun idY y = y.
An exact proof term for the current goal is (identity_function_apply Y y HyY).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using Hcapp (from left to right).
rewrite the current goal using Hidapp (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x0} Y x0 y (SingI x0) HyY).
We prove the intermediate claim Hf: continuous_map Y Ty Slice Tslice f.
An exact proof term for the current goal is (continuous_map_range_restrict Y Ty (setprod X Y) (product_topology X Tx Y Ty) f Slice HfProd HSlicesub Himg).
We prove the intermediate claim HprojPair: continuous_map (setprod X Y) (product_topology X Tx Y Ty) X Tx (projection_map1 X Y) ∧ continuous_map (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y).
An exact proof term for the current goal is (projection_maps_continuous X Tx Y Ty HTx HTy).
We prove the intermediate claim Hproj2: continuous_map (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y).
An exact proof term for the current goal is (andER (continuous_map (setprod X Y) (product_topology X Tx Y Ty) X Tx (projection_map1 X Y)) (continuous_map (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y)) HprojPair).
We prove the intermediate claim Hg: continuous_map Slice Tslice Y Ty (projection_map2 X Y).
An exact proof term for the current goal is (continuous_on_subspace (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y) Slice HTprod HSlicesub Hproj2).
We will prove continuous_map Y Ty Slice Tslice f ∧ ∃g : set, continuous_map Slice Tslice Y Ty g ∧ (∀x : set, x ∈ Y → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Slice → apply_fun f (apply_fun g y) = y).
Apply andI to the current goal.
An exact proof term for the current goal is Hf.
We use (projection_map2 X Y) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hg.
Let y be given.
Assume HyY: y ∈ Y.
We will prove apply_fun (projection_map2 X Y) (apply_fun f y) = y.
We prove the intermediate claim Happf: apply_fun f y = (apply_fun c y,apply_fun idY y).
An exact proof term for the current goal is (pair_map_apply Y X Y c idY y HyY).
We prove the intermediate claim Hcapp: apply_fun c y = x0.
An exact proof term for the current goal is (const_fun_apply Y x0 y HyY).
We prove the intermediate claim Hidapp: apply_fun idY y = y.
An exact proof term for the current goal is (identity_function_apply Y y HyY).
We prove the intermediate claim HxyXY: (x0,y) ∈ setprod X Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y x0 y Hx0X HyY).
rewrite the current goal using Happf (from left to right).
rewrite the current goal using Hcapp (from left to right).
rewrite the current goal using Hidapp (from left to right).
We prove the intermediate claim Happ2: apply_fun (projection_map2 X Y) (x0,y) = (x0,y) 1.
An exact proof term for the current goal is (projection2_apply X Y (x0,y) HxyXY).
rewrite the current goal using Happ2 (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq x0 y).
Let p be given.
Assume HpSlice: p ∈ Slice.
We will prove apply_fun f (apply_fun (projection_map2 X Y) p) = p.
We prove the intermediate claim HpXY: p ∈ setprod X Y.
An exact proof term for the current goal is (HSlicesub p HpSlice).
We prove the intermediate claim Hp1Y: (p 1) ∈ Y.
An exact proof term for the current goal is (ap1_Sigma {x0} (λ_ : set ⇒ Y) p HpSlice).
We prove the intermediate claim Happ2: apply_fun (projection_map2 X Y) p = p 1.
An exact proof term for the current goal is (projection2_apply X Y p HpXY).
rewrite the current goal using Happ2 (from left to right).
We prove the intermediate claim Happf: apply_fun f (p 1) = (apply_fun c (p 1),apply_fun idY (p 1)).
An exact proof term for the current goal is (pair_map_apply Y X Y c idY (p 1) Hp1Y).
We prove the intermediate claim Hcapp: apply_fun c (p 1) = x0.
An exact proof term for the current goal is (const_fun_apply Y x0 (p 1) Hp1Y).
We prove the intermediate claim Hidapp: apply_fun idY (p 1) = (p 1).
An exact proof term for the current goal is (identity_function_apply Y (p 1) Hp1Y).
rewrite the current goal using Happf (from left to right).
rewrite the current goal using Hcapp (from left to right).
rewrite the current goal using Hidapp (from left to right).
We prove the intermediate claim Hp0Sing: (p 0) ∈ {x0}.
An exact proof term for the current goal is (ap0_Sigma {x0} (λ_ : set ⇒ Y) p HpSlice).
We prove the intermediate claim Hp0eq: (p 0) = x0.
An exact proof term for the current goal is (singleton_elem (p 0) x0 Hp0Sing).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta {x0} Y p HpSlice).
We prove the intermediate claim HtupleEq: (p 0,p 1) = p.
rewrite the current goal using Heta (from right to left).
Use reflexivity.
rewrite the current goal using Hp0eq (from right to left) at position 1.
An exact proof term for the current goal is HtupleEq.
∎