-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h₂ :
  Eq (α :=
    Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
    ((fun
            (f :
              X.obj
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) ↦
          ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 _proof_2 _proof_5).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := _proof_2 })))
          x) :
      ComposableArrows C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
          (a :
              (fun (X : Type u) ↦ X)
                (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 })))
        y :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))
h₀ :
  Eq (α :=
    Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
    ((fun
            (f :
              X.obj
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) ↦
          ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _proof_2 _proof_5).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := _proof_2 })))
          x) :
      ComposableArrows C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
          (a :
              (fun (X : Type u) ↦ X)
                (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 })))
        y :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
obtain :
  ∀
    (x₀ x₁ x₂ :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) (h : e₀₁.CompStruct e₁₂ e₀₂)
    (h₂ :
      Eq (α :=
        Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
        ((fun
                (f :
                  X.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) ↦
              ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 _proof_2 _proof_5).op) :
                (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
                  (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := _proof_2 })))
              h.simplex) :
          ComposableArrows C 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
                (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 })))
            y :
          (fun (X : Type u) ↦ X)
            (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))))
    (h₀ :
      Eq (α :=
        Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
        ((fun
                (f :
                  X.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) ↦
              ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _proof_2 _proof_5).op) :
                (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
                  (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := _proof_2 })))
              h.simplex) :
          ComposableArrows C 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
                (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 })))
            y :
          (fun (X : Type u) ↦ X)
            (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))),
    Eq (α :=
      Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
      ((fun
              (f :
                X.obj
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) ↦
            ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 _proof_2 _proof_5).op) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := _proof_2 })))
            h.simplex) :
        ComposableArrows C 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 _proof_2 _proof_5).op) :
            (a :
                (fun (X : Type u) ↦ X)
                  (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
              (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 })))
          y :
        (fun (X : Type u) ↦ X)
          (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
            (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))
⊢ Eq (α :=
    Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
    ((fun
            (f :
              X.obj
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) ↦
          ComposableArrows.mk₁ (F.map (homMk (Edge.mk' f))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 _proof_2 _proof_5).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := _proof_2 })))
          x) :
      ComposableArrows C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 _proof_2 _proof_5).op) :
          (a :
              (fun (X : Type u) ↦ X)
                (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1 + 1⦌, property := _proof_5 }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 })))
        y :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
          (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))

Tactic:
obtain ⟨x₀, x₁, x₂, e₀₁, e₁₂, e₀₂, h, rfl⟩ := Edge.CompStruct.exists_of_simplex x

Premises used: SSet.Truncated.Edge.CompStruct.exists_of_simplex, rfl