-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 :
  ∀ (n : ℕ) (f : Arrow.{v, u} C),
    HasWidePullback.{0, v, u} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
X : Augmented.{v, u} C
F : Arrow.{v, u} C
G : Functor.obj Augmented.toArrow X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
a :
  ∀ (j : Fin ((Opposite.unop y).len + 1)),
    CategoryStruct.comp (Y :=
        widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
          fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
        (X.left.map f ≫
          WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
            (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
              X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) i)) ≫ Arrow.Hom.left G)
            ⋯)
        (WidePullback.π (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom) j) =
      CategoryStruct.comp (Y :=
        widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
          fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
          (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
              (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
                X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
              ⋯ :
            X.left.obj x ⟶
              widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
                fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
          (WidePullback.lift (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
              (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
                WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
                  ((SimplexCategory.Hom.toOrderHom f.unop :
                      (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
                    i))
              ⋯ :
            (widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
                fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) ⟶
              widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
                fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom))
        (WidePullback.π (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom) j)
⊢ Eq (α :=
    X.left.obj x ⟶
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
    (X.left.map f ≫
      WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
        (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
          X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) i)) ≫ Arrow.Hom.left G)
        ⋯)
    (CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
            X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
          ⋯ :
        X.left.obj x ⟶
          widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (WidePullback.lift (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
          (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
            WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
              ((SimplexCategory.Hom.toOrderHom f.unop :
                  (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
                i))
          ⋯ :
        (widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) ⟶
          widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom))
have a₁ : CategoryStruct.comp (Y :=
    widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
      fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
    (X.left.map f ≫
      WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
        (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
          X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop y) i)) ≫ Arrow.Hom.left G)
        sorry)
    (WidePullback.base fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom) =
  CategoryStruct.comp (Y :=
    widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
      fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
    (CategoryStruct.comp (Y :=
      widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
        fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun (i : Fin ((Opposite.unop x).len + 1)) ↦
            X.left.map (Quiver.Hom.op (⦋0⦌.const (Opposite.unop x) i)) ≫ Arrow.Hom.left G)
          sorry :
        X.left.obj x ⟶
          widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
      (WidePullback.lift (WidePullback.base fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
          (fun (i : Fin ((Opposite.unop y).len + 1)) ↦
            WidePullback.π (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom)
              ((SimplexCategory.Hom.toOrderHom f.unop :
                  (a : Fin ((Opposite.unop y).len + 1)) → Fin ((Opposite.unop x).len + 1))
                i))
          sorry :
        (widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop x).len + 1)) ↦ F.hom) ⟶
          widePullback.{0, v, u} F.right (fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.left)
            fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom))
    (WidePullback.base fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
Tactic: ext