-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : HSpace X
inst_3 : HSpace Y
G : (↑I : Type) × X × Y → X × Y :=
  fun (p : (↑I : Type) × X × Y) ↦
    ((eHmul : (a : (↑I : Type) × X) → X) (p.1, p.2.1), (eHmul : (a : (↑I : Type) × Y) → Y) (p.1, p.2.2))
hG : Continuous G
map_zero_left :
  ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (0, x) =
      (comp
            {
              toFun := fun (p : (X × Y) × X × Y) ↦
                ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
              continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
            (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))) :
          (a : X × Y) → X × Y)
        x
map_one_left :
  ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG : C((↑I : Type) × X × Y, X × Y) }.toFun (1, x) =
      (ContinuousMap.id (X × Y) : (a : X × Y) → X × Y) x
prop' :
  ∀ (t : (↑I : Type)) (x : X × Y),
    Membership.mem (γ := Set (X × Y)) {(@e _ inst _, @e _ inst_1 _)} x →
      Eq (α := X × Y)
        (({
                toFun := fun (x : X × Y) ↦
                  (Homotopy.toContinuousMap (f₀ :=
                        comp
                          {
                            toFun := fun (p : (X × Y) × X × Y) ↦
                              ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                            continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                          (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))))
                        (f₁ := ContinuousMap.id (X × Y))
                        { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ :
                          Homotopy
                            (comp
                              {
                                toFun := fun (p : (X × Y) × X × Y) ↦
                                  ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                                continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                              (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))))
                            (ContinuousMap.id (X × Y)) }).toFun
                    (t, x),
                continuous_toFun := ⋯ : C(X × Y, X × Y) } :
              (a : X × Y) → X × Y)
            x :
          X × Y)
        ((comp
                {
                  toFun := fun (p : (X × Y) × X × Y) ↦
                    ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
                  continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
                (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))) :
              (a : X × Y) → X × Y)
            x :
          X × Y)
⊢ HomotopyRel
    (comp
      {
        toFun := fun (p : (X × Y) × X × Y) ↦
          ((hmul : (a : X × X) → X) (p.1.1, p.2.1), (hmul : (a : Y × Y) → Y) (p.1.2, p.2.2)),
        continuous_toFun := ⋯ : C((X × Y) × X × Y, X × Y) }
      (prodMk (const (X × Y) (@e _ inst _, @e _ inst_1 _)) (ContinuousMap.id (X × Y))))
    (ContinuousMap.id (X × Y)) {(@e _ inst _, @e _ inst_1 _)}

Tactic:
use! ⟨G, hG⟩