-- 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)
⊢ Eq (α :=
    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)))))
    (⟦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)))))
    (eqToHom ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫
          eqToHom ⋯ :
      Quiver.Hom (V := (↑(π.obj Y) : Type u)) (fromTop ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x))
        (fromTop ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x)))
have refine : 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) })
  ((π.map (TopCat.ofHom H.uliftMap)).map
      (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
        (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) :
    (π.map (TopCat.ofHom H.uliftMap)).obj
        (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 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
            { as := x : FundamentalGroupoid (↑X : Type u) })) ⟶
      (π.map (TopCat.ofHom H.uliftMap)).obj
        (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 })))
Tactic: refine (@conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _
    (FundamentalGroupoid.ext <| H.apply_one x).symm).mpr ?_