-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x : (↑X : Type u)
⊢ HEq (α :=
    Quiver.Hom (V := (↑(π.obj Y) : Type u))
      ({ as := (f : (a : (↑X : Type u)) → (↑Y : Type u)) x } : FundamentalGroupoid (↑Y : Type u))
      ({ as := (g : (a : (↑X : Type u)) → (↑Y : Type u)) x } : FundamentalGroupoid (↑Y : Type u)))
    (⟦H.evalAt x⟧ :
      Quotient (α :=
        Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
          ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))
        (Path.Homotopic.setoid ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x)
            ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x) :
          Setoid
            (Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
              ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))))
    (β :=
    Quiver.Hom (V := (↑(π.obj Y) : Type u)) (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x)))
      { as := (H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (1, x) })
    (Path.Homotopic.Quotient.map
        (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          (⟦unitInterval.upath01⟧, 𝟙 (fromTop x)))
        H.uliftMap :
      Path.Homotopic.Quotient (X := (↑Y : Type u))
        ((H.uliftMap : (a : ULift.{u, 0} (↑I : Type) × (↑X : Type u)) → (↑Y : Type u))
            (as
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) ({ as := { down := 0 } }, { as := x })) :
              ULift.{u, 0} (↑I : Type) × (↑X : Type u)) :
          (↑Y : Type u))
        ((H.uliftMap : (a : ULift.{u, 0} (↑I : Type) × (↑X : Type u)) → (↑Y : Type u))
            (as
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) ({ as := { down := 1 } }, { as := x })) :
              ULift.{u, 0} (↑I : Type) × (↑X : Type u)) :
          (↑Y : Type u)))
have hp : ∀ (t : (↑I : Type)),
  Eq (α := (↑Y : Type u)) ((H.evalAt x : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
    (((fun
                (q :
                  Path (X := ULift.{u, 0} (↑I : Type) × (↑X : Type u))
                    (as
                        (Functor.obj (C :=
                          (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                          (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                          ({ as := { down := 0 } }, { as := x })) :
                      ULift.{u, 0} (↑I : Type) × (↑X : Type u))
                    (as
                      (Functor.obj (C :=
                        (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                        (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                        ({ as := { down := 1 } }, { as := x })))) ↦
              q.map sorry)
            (unitInterval.upath01.prod (Path.refl (fromTop x).as)) :
          (a : (↑I : Type)) → (↑Y : Type u))
        t :
      (↑Y : Type u))
Tactic: apply Path.Homotopic.hpath_hext