-- 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
a :
  ∀ (j : Fin 1),
    Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
      (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
          (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
            (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
            (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
              (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) ⋯))
          (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
        (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
      (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
          ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫
            S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) ⋯)
          (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
        (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
⊢ Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
    (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
        (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
          (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) ⋯) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
    ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) ⋯ :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
have a₁ : Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.right)
  (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
      (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
        (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
          (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) sorry))
      (WidePullback.base fun (x : Fin 1) ↦ f.hom) :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.right)
  (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
      ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫
        S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) sorry)
      (WidePullback.base fun (x : Fin 1) ↦ f.hom) :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.right)
Tactic: ext j