-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
mk :
  ∀ (as : Paths C),
    Eq.{v₁ + 1} (α :=
      Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as) ⟶
        Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))
      (CategoryStruct.comp (Y :=
          Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C)
            (Functor.obj (toQuotientPaths C)
              (Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))))
          (Functor.map (quotientPathsTo C)
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (X : Quotient (pathsHomRel C)) ↦
                    Quotient.casesOn (r := pathsHomRel C) (motive := fun (t : Quotient (pathsHomRel C)) ↦
                      (h : X = t) →
                        Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                          Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                      X
                      (fun (as : Paths C) (h : X = Quotient.mk (r := pathsHomRel C) as) ↦
                        Eq.ndrec (motive := fun (X : Quotient (pathsHomRel C)) ↦
                          Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                            Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                          (Iso.refl (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as)))
                          ⋯)
                      ⋯)
                  ⋯))
              (Quotient.mk (r := pathsHomRel C) as)))
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (x : C) ↦ Iso.refl (Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x)) ⋯))
            (Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))) :
        Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as) ⟶
          Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))
      (𝟙 (Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as)) :
        Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as) ⟶
          Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))
⊢ Eq.{v₁ + 1} (α := Functor.obj (quotientPathsTo C) X ⟶ Functor.obj (quotientPathsTo C) X)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C)
          (Functor.obj (toQuotientPaths C) (Functor.obj (quotientPathsTo C) X)))
        (Functor.map (quotientPathsTo C)
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : Quotient (pathsHomRel C)) ↦
                  Quotient.casesOn (r := pathsHomRel C) (motive := fun (t : Quotient (pathsHomRel C)) ↦
                    (h : X = t) →
                      Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                        Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                    X
                    (fun (as : Paths C) (h : X = Quotient.mk (r := pathsHomRel C) as) ↦
                      Eq.ndrec (motive := fun (X : Quotient (pathsHomRel C)) ↦
                        Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                          Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                        (Iso.refl (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))) ⋯)
                    ⋯)
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (x : C) ↦ Iso.refl (Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x)) ⋯))
          (Functor.obj (quotientPathsTo C) X)) :
      Functor.obj (quotientPathsTo C) X ⟶ Functor.obj (quotientPathsTo C) X)
    (𝟙 (Functor.obj (quotientPathsTo C) X) : Functor.obj (quotientPathsTo C) X ⟶ Functor.obj (quotientPathsTo C) X)

Tactic:
cases X