-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
obj :
  V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)) →
    D
map :
  {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))} →
    Edge x y → (obj x ⟶ obj y)
map_id :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀
    {x₀ x₁ x₂ :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₁ :
  (Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
        Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂)) =
      (obj x₀ ⟶ obj x₂) →
    Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) =
        obj x₀ →
      Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
            (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
            (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₁) =
          obj x₁ →
        CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
            (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₁)) =
          map e₀₁
h₂ :
  (Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
        Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂)) =
      (obj x₀ ⟶ obj x₂) →
    Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₁) =
        obj x₁ →
      Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
            (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
            (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂) =
          obj x₂ →
        CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
            (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₁₂)) =
          map e₁₂
h₃ :
  (Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
        Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
          (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
          (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂)) =
      (obj x₀ ⟶ obj x₂) →
    CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₂)) =
      map e₀₂
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
      Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂))
    (CategoryStruct.comp (Y :=
      Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₁))
      (CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₁)))
      (CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₁₂))))
    (CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₂)))

Tactic:
convert! map_comp h