-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem eq_diag_path : (πₘ (TopCat.ofHom f)).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧
    (⟦H.evalAt x₀⟧ ≫ (πₘ (TopCat.ofHom g)).map p :
    fromTop (f x₀) ⟶ fromTop (g x₁)) = H.diagonalPath' p

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
            hcast ⋯ =
      H.diagonalPath' p

Tactic:
constructor

Result:
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast ⋯ =
    H.diagonalPath' p

case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
          hcast ⋯ =
    H.diagonalPath' p

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop (fromTop x₁).as))) ≫ hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ =
      H.diagonalPath' p

Tactic:
dsimp only [prodToProdTopI]

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
            hcast ⋯ =
      H.diagonalPath' p