-- 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)
j : Fin (n + 1 + 1)
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.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) 0) :
      (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) 0 :
          (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) ⟶
      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)
have a₁ : ∀ (i_1 : Fin (n + 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_2 : Fin (n + 1 + 1)) ↦
              WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_2))
            sorry))
        (WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) i_1.succ) :
      (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_2 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_2)) 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.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) i_1.succ :
          (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)
Tactic: induction j using Fin.cases
Cleared hypotheses: j