-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ 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)
have 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))) sorry)
                    sorry)
                sorry))
            (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)) sorry))
          (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))
Tactic: cases X
Cleared hypotheses: X