-- Module: Mathlib.Topology.Category.TopPair
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)
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) :
                  ℝ))
              ⋯,
            ((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)
              ⋯,
            ((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) : ℝ)) ⋯,
              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) ⋯,
              fst)) :
      (↑(TopPair.fst (X := Y)) : 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))

Tactic:
simp only [TopCat.comp_app, Homotopy.h_hom_apply, ContinuousMap.Homotopy.trans_apply]

Premises used: ContinuousMap.Homotopy.trans_apply, TopCat.Homotopy.h_hom_apply, TopCat.comp_app