-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
a :
  ∀ (j : Fin (n + 1 + 1)),
    Eq (α :=
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        f.left)
      (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
              f.hom)
            (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
            (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
              (fun (i_1 : Fin (n + 1 + 1)) ↦
                WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_1))
              ⋯))
          (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) j) :
        (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
          f.left)
      (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (CategoryStruct.comp (Y :=
              widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
              (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
                  (fun (i_1 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_1)) ⋯ :
                (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                    f.hom) ⟶
                  widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
              (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
            (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                f.hom) ⟶
              widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) j :
            (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                f.hom) ⟶
              f.left) :
        (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
          f.left)
⊢ Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
          (fun (i_1 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_1))
          ⋯) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (fun (i_1 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_1)) ⋯ :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
        (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
have a₁ : Eq (α :=
  (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶ f.right)
  (CategoryStruct.comp (Y :=
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
      (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
          (fun (i_1 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_1))
          sorry))
      (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom) :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
      f.right)
  (CategoryStruct.comp (Y :=
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
      (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
          (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
              (fun (i_1 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_1)) sorry :
            (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                f.hom) ⟶
              widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
          (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
        (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
      (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom :
        (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
          f.right) :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom) ⟶
      f.right)
Tactic: ext j