homotopy: turning intuition into mathematical argument

I’m learning about homotopy for the first time. The idea is very intuitive but I have trouble writing down the actual map to prove that something is homotopic.

For instance,

If XX is contractible space then X×YX \times Y is is homotopy
equivalent to YY.

When I read this question, I think of two lines parallel to each other and a straight line map between each corresponding points.
However, I am stuck on how to write this mathematically.
This is what I’ve tried:

Since XX is contractible, identity map is homotopic to a constant map.
Hence, ∃h:X×[0,1]→X\exists h: X \times [0,1] \rightarrow X such that h(x,0)=xh(x,0)=x
and h(x,1)=ph(x,1)=p constant. What I want to prove is: ∃f:X×Y→Y\exists f:X\times Y \rightarrow Y and g:Y→X×Yg: Y \rightarrow X\times Y such that gfgf and fgfg are homotopic to identity maps.
For instance if we take fgfg, we want to find H:Y×[0,1]→Y H: Y\times [0,1] \rightarrow Y such that H(y,0)=fgH(y,0)=fg and H(y,1)=idYH(y,1)= id_Y

This just seems too long – as I have to show that f and g exists and then show that composition is homotopic to identity (hence find another map). I cant adapt my intuition at all.

Any help would be appreciated.