-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
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⦌ ⋯))
⊢ 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⦌
              ⋯))))
have 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⦌ sorry))))
    ((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⦌
                  sorry))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := sorry }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := sorry })))
        (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⦌
              sorry))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  sorry))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := sorry }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := sorry })))
        (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⦌
              sorry))))
Tactic: obtain ⟨x, y, f, rfl⟩ := ComposableArrows.mk₁_surjective f
Cleared hypotheses: f