-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ 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₂))
          (edgeMk f₁₂)) :
      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₂))
        (edgeMk f₀₂) :
      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))
have h₁ : 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) =
    (x₀ ⟶ x₂) →
  (nerveEquiv : (a : ComposableArrows C 0) → C)
        ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) =
      x₀ →
    (nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₁ : ComposableArrows.{v, u} C 0) =
        x₁ →
      (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₀₁) =
        f₀₁
Tactic: convert! (nerve.nonempty_compStruct_iff _ _ _).1 ⟨h⟩