-- Lean 4 proof step from Mathlib.Topology.Category.TopPair (goal)
Goal:
X_1 Y_1 X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
fst : (↑(TopPair.snd (X := X)) : Type u)
snd : (↑I : Type u)
⊢ Eq (α := (↑(TopPair.fst (X := Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (map ▷ I ≫ Homotopy.h (F.fst.trans G.fst)) :
          (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑TopPair.fst : Type u))
        (fst, snd) :
      (↑(TopPair.fst (X := Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (Homotopy.h (F.snd.trans G.snd) ≫ map) :
          (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑TopPair.fst : Type u))
        (fst, snd) :
      (↑(TopPair.fst (X := Y)) : Type u))
have w : Eq (α := (↑(TopPair.fst (X := Y)) : Type u))
  (if h :
        (↑((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := tensorObj (𝒞 := instCategory) (TopPair.snd (X := X)) I) (map ▷ I) :
                      (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑(TopPair.fst ⊗ I) : Type u))
                    (fst, snd)).2) :
            ℝ) ≤
          1 / 2 then
      (F.fst : (a : (↑unitInterval : Type) × (↑TopPair.fst : Type u)) → (↑TopPair.fst : Type u))
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval)
            (HMul.hMul (α := ℝ) 2
              (↑((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (X := tensorObj (𝒞 := instCategory) (TopPair.snd (X := X)) I) (map ▷ I) :
                          (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑(TopPair.fst ⊗ I) : Type u))
                        (fst, snd)).2) :
                ℝ))
            sorry,
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  tensorObj (𝒞 := instCategory) (TopPair.snd (X := X)) I) (map ▷ I) :
                (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑(TopPair.fst ⊗ I) : Type u))
              (fst, snd)).1)
    else
      (G.fst : (a : (↑unitInterval : Type) × (↑TopPair.fst : Type u)) → (↑TopPair.fst : Type u))
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval)
            (HMul.hMul (α := ℝ) 2
                (↑((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) (X := tensorObj (𝒞 := instCategory) (TopPair.snd (X := X)) I) (map ▷ I) :
                            (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑(TopPair.fst ⊗ I) : Type u))
                          (fst, snd)).2) :
                  ℝ) -
              1)
            sorry,
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  tensorObj (𝒞 := instCategory) (TopPair.snd (X := X)) I) (map ▷ I) :
                (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑(TopPair.fst ⊗ I) : Type u))
              (fst, snd)).1) :
    (↑(TopPair.fst (X := Y)) : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          TopPair.snd (X := Y)) map :
        (a : (↑TopPair.snd : Type u)) → (↑TopPair.fst : Type u))
      (if h : (↑((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) snd) : ℝ) ≤ 1 / 2 then
        (F.snd : (a : (↑unitInterval : Type) × (↑TopPair.snd : Type u)) → (↑TopPair.snd : Type u))
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval)
              (HMul.hMul (α := ℝ) 2 (↑((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) snd) : ℝ)) sorry,
            fst)
      else
        (G.snd : (a : (↑unitInterval : Type) × (↑TopPair.snd : Type u)) → (↑TopPair.snd : Type u))
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ unitInterval)
              (HMul.hMul (α := ℝ) 2 (↑((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) snd) : ℝ) - 1) sorry,
            fst)) :
    (↑(TopPair.fst (X := Y)) : Type u))
Tactic: simp only [TopCat.comp_app, Homotopy.h_hom_apply, ContinuousMap.Homotopy.trans_apply]