-- Module: Mathlib.AlgebraicTopology.CechNerve
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)
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)
          ⋯)
      (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)
            ⋯ :
          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.base fun (x : Fin ((Opposite.unop y).len + 1)) ↦ F.hom)
⊢ 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))

Tactic:
ext