-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ : C
e₀₁ :
  Edge (X := nerve.{v, u} C) ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀)
    ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₁)
x₂ : C
e₀₂ :
  Edge (X := nerve.{v, u} C) ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀)
    ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂)
e₁₂ :
  Edge (X := nerve.{v, u} C) ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₁)
    ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂)
h : e₀₁.CompStruct e₁₂ e₀₂
obtain :
  ∀ (f₀₁ : x₀ ⟶ x₁) (h : (edgeMk f₀₁).CompStruct e₁₂ e₀₂),
    Eq.{v + 1} (α :=
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
          C))
      (CategoryStruct.comp (Y :=
          (nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₁ : ComposableArrows.{v, u} C 0))
          ((homEquiv :
              (a :
                  Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀)
                    ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁)) →
                (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
                  (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁))
            (edgeMk f₀₁))
          ((homEquiv :
              (a :
                  Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁)
                    ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂)) →
                (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁) ⟶
                  (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂))
            e₁₂) :
        Quiver.Hom.{v, u} (V := C)
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
              ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
            C)
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
              ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
            C))
      ((homEquiv :
            (a :
                Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀)
                  ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂)) →
              (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
                (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂))
          e₀₂ :
        Quiver.Hom.{v, u} (V := C)
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
              ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
            C)
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
              ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
            C))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
        C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
        C))
    (CategoryStruct.comp (Y :=
        (nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₁ : ComposableArrows.{v, u} C 0))
        ((homEquiv :
            (a :
                Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀)
                  ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁)) →
              (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
                (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁))
          e₀₁)
        ((homEquiv :
            (a :
                Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁)
                  ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂)) →
              (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁) ⟶
                (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂))
          e₁₂) :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
          C))
    ((homEquiv :
          (a :
              Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀)
                ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂)) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
              (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂))
        e₀₂ :
      Quiver.Hom.{v, u} (V := C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
          C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
          C))

Tactic:
obtain ⟨f₀₁, rfl⟩ := edgeMk_surjective e₀₁

Premises used: rfl, CategoryTheory.nerve.edgeMk_surjective