-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : ComposableArrows.{v, u} C 0
e₀₁ : Edge (X := nerve.{v, u} C) x₀ x₁
e₁₂ : Edge (X := nerve.{v, u} C) x₁ x₂
e₀₂ : Edge (X := nerve.{v, u} C) x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x₀ : C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C) x₂ : C))
    (CategoryStruct.comp (Y := (nerveEquiv : (a : ComposableArrows C 0) → C) x₁)
        ((homEquiv :
            (a : Edge x₀ x₁) →
              (nerveEquiv : (a : ComposableArrows C 0) → C) x₀ ⟶ (nerveEquiv : (a : ComposableArrows C 0) → C) x₁)
          e₀₁)
        ((homEquiv :
            (a : Edge x₁ x₂) →
              (nerveEquiv : (a : ComposableArrows C 0) → C) x₁ ⟶ (nerveEquiv : (a : ComposableArrows C 0) → C) x₂)
          e₁₂) :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x₀ : C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C) x₂ : C))
    ((homEquiv :
          (a : Edge x₀ x₂) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) x₀ ⟶ (nerveEquiv : (a : ComposableArrows C 0) → C) x₂)
        e₀₂ :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x₀ : C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C) x₂ : C))
have obtain : ∀ (x₀ : C) {e₀₁ : Edge (X := nerve.{v, u} C) ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀) x₁}
  {e₀₂ : Edge (X := nerve.{v, u} C) ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀) x₂}
  (h : e₀₁.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) x₂ : C))
    (CategoryStruct.comp (Y := (nerveEquiv : (a : ComposableArrows C 0) → C) x₁)
        ((homEquiv :
            (a : Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) x₁) →
              (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
                (nerveEquiv : (a : ComposableArrows C 0) → C) x₁)
          e₀₁)
        ((homEquiv :
            (a : Edge x₁ x₂) →
              (nerveEquiv : (a : ComposableArrows C 0) → C) x₁ ⟶ (nerveEquiv : (a : ComposableArrows C 0) → C) 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) x₂ : C))
    ((homEquiv :
          (a : Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) x₂) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
              (nerveEquiv : (a : ComposableArrows C 0) → C) 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) x₂ : C))
Tactic: obtain ⟨x₀, rfl⟩ := nerveEquiv.symm.surjective x₀
Cleared hypotheses: x₀, e₀₁, e₀₂, h