-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
f :
  (nerveFunctor₂.obj (Cat.of C)).obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))
obtain :
  ∀ (x y : (↑(Cat.of C) : Type u)) (f : x ⟶ y),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        ((nerveFunctor₂.obj (Cat.of D)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((nerveFunctor₂.map (functorOfNerveMap φ).toCatHom).app
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1)
                    ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
          (ComposableArrows.mk₁ f) :
        (fun (X : Type u) ↦ X)
          ((nerveFunctor₂.obj (Cat.of D)).obj
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (φ.app
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1)
                    ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
          (ComposableArrows.mk₁ f) :
        (fun (X : Type u) ↦ X)
          ((nerveFunctor₂.obj (Cat.of D)).obj
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                ⋯))))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((nerveFunctor₂.obj (Cat.of D)).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((nerveFunctor₂.map (functorOfNerveMap φ).toCatHom).app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f :
      (fun (X : Type u) ↦ X)
        ((nerveFunctor₂.obj (Cat.of D)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f :
      (fun (X : Type u) ↦ X)
        ((nerveFunctor₂.obj (Cat.of D)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))

Tactic:
obtain ⟨x, y, f, rfl⟩ := ComposableArrows.mk₁_surjective f

Premises used: CategoryTheory.ComposableArrows.mk₁_surjective, rfl