-- 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₀₂
simp :
  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₀₂)))
⊢ 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₂))
    (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))
        (CategoryStruct.comp (Y := x₁) (Quiver.Hom.toPath e₀₁) (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:
simp only [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp