∀ (X : Type u_1) (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : HSpace X]
  [inst_3 : HSpace Y] (hG : Continuous fun p => (HSpace.hmulE (p.1, p.2.1), HSpace.hmulE (p.1, p.2.2)))
  (t : ↑unitInterval),
  ∀ x ∈ {(HSpace.e, HSpace.e)},
    {
          toFun := fun x =>
            { toFun := fun p => (HSpace.hmulE (p.1, p.2.1), HSpace.hmulE (p.1, p.2.2)), continuous_toFun := hG,
                  map_zero_left := ⋯, map_one_left := ⋯ }.toFun
              (t, x),
          continuous_toFun := ⋯ }
        x =
      ({ toFun := fun p => (HSpace.hmul (p.1.1, p.2.1), HSpace.hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((ContinuousMap.id (X × Y)).prodMk (ContinuousMap.const (X × Y) (HSpace.e, HSpace.e))))
        x