-- 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),
    HasWidePushout.{0, v, u} f.left (fun (x : Fin (n + 1)) ↦ f.right) fun (x : Fin (n + 1)) ↦ f.hom
F : Arrow.{v, u} C
X : Augmented.{v, u} C
G : F ⟶ Functor.obj Augmented.toArrow X
x y : SimplexCategory
f : x ⟶ y
a :
  ∀ (j : Fin (x.len + 1)),
    CategoryStruct.comp (Y :=
        widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
        (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
          (fun (x : Fin (x.len + 1)) ↦ F.hom) j)
        (CategoryStruct.comp (Y :=
          widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
          (WidePushout.desc (WidePushout.head fun (x : Fin (y.len + 1)) ↦ F.hom)
              (fun (i : Fin (x.len + 1)) ↦
                WidePushout.ι.{0, v, u} (J := Fin (y.len + 1)) (C := C) (B := F.left) (objs :=
                  fun (x : Fin (y.len + 1)) ↦ F.right) (fun (x : Fin (y.len + 1)) ↦ F.hom)
                  ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)))
              ⋯ :
            (widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom) ⟶
              widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
          (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y)
              (fun (i : Fin (y.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ :
            (widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom) ⟶
              X.right.obj y)) =
      CategoryStruct.comp (Y :=
        widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
        (WidePushout.ι.{0, v, u} (C := C) (B := F.left) (objs := fun (x : Fin (x.len + 1)) ↦ F.right)
          (fun (x : Fin (x.len + 1)) ↦ F.hom) j)
        (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x)
            (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
          X.right.map f)
⊢ Eq (α :=
    (widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom) ⟶
      X.right.obj y)
    (CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
      (WidePushout.desc (WidePushout.head fun (x : Fin (y.len + 1)) ↦ F.hom)
          (fun (i : Fin (x.len + 1)) ↦
            WidePushout.ι.{0, v, u} (J := Fin (y.len + 1)) (C := C) (B := F.left) (objs := fun (x : Fin (y.len + 1)) ↦
              F.right) (fun (x : Fin (y.len + 1)) ↦ F.hom)
              ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)))
          ⋯ :
        (widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom) ⟶
          widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
      (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y)
          (fun (i : Fin (y.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ :
        (widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom) ⟶
          X.right.obj y))
    (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
      X.right.map f)
have a₁ : CategoryStruct.comp (Y :=
    widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom)
    (CategoryStruct.comp (Y :=
      widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
      (WidePushout.desc (WidePushout.head fun (x : Fin (y.len + 1)) ↦ F.hom)
          (fun (i : Fin (x.len + 1)) ↦
            WidePushout.ι.{0, v, u} (J := Fin (y.len + 1)) (C := C) (B := F.left) (objs := fun (x : Fin (y.len + 1)) ↦
              F.right) (fun (x : Fin (y.len + 1)) ↦ F.hom)
              ((SimplexCategory.Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i : Fin (y.len + 1)))
          sorry :
        (widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom) ⟶
          widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom)
      (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y)
          (fun (i : Fin (y.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) sorry :
        (widePushout.{0, v, u} F.left (fun (x : Fin (y.len + 1)) ↦ F.right) fun (x : Fin (y.len + 1)) ↦ F.hom) ⟶
          X.right.obj y)) =
  CategoryStruct.comp (Y :=
    widePushout.{0, v, u} F.left (fun (x : Fin (x.len + 1)) ↦ F.right) fun (x : Fin (x.len + 1)) ↦ F.hom)
    (WidePushout.head fun (x : Fin (x.len + 1)) ↦ F.hom)
    (WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x)
        (fun (i : Fin (x.len + 1)) ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) sorry ≫
      X.right.map f)
Tactic: ext