-- Module: Mathlib.AlgebraicTopology.CechNerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
ι : Type w
inst_2 : HasFiniteProducts.{v, u} C
inst_3 : Finite ι
X : C
i : WidePullbackShape ι
id :
  Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
        (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none ⟶
      Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none)
        (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (WidePullbackShape.Hom.id none))
        (Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          none
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) :
      Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)
    ((Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          none
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) ≫
        Functor.map (wideCospan ι X) (WidePullbackShape.Hom.id none) :
      Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
          (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) none)
id₁ :
  ∀ (val : ι),
    Eq.{v + 1} (α :=
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (some val) ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) (some val))
      (CategoryStruct.comp (Y :=
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
            (some val))
          (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
            (WidePullbackShape.Hom.id (some val)))
          (Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
            Functor.obj.{w, v, w, u}
                (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
              Functor.obj.{w, v, w, u} (wideCospan ι X) x)
            (some val)
            (terminal.from
              (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
            fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) :
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
            (some val) ⟶
          Functor.obj.{w, v, w, u} (wideCospan ι X) (some val))
      ((Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
            Functor.obj.{w, v, w, u}
                (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) x ⟶
              Functor.obj.{w, v, w, u} (wideCospan ι X) x)
            (some val)
            (terminal.from
              (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
                (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
            fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) ≫
          Functor.map (wideCospan ι X) (WidePullbackShape.Hom.id (some val)) :
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
            (some val) ⟶
          Functor.obj.{w, v, w, u} (wideCospan ι X) (some val))
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) i ⟶
      Functor.obj.{w, v, w, u} (wideCospan ι X) i)
    (CategoryStruct.comp (Y :=
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          i)
        (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
          (WidePullbackShape.Hom.id i))
        (Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          i
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) i ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) i)
    ((Option.casesOn (motive := fun (x : WidePullbackShape ι) ↦
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X))
              x ⟶
            Functor.obj.{w, v, w, u} (wideCospan ι X) x)
          i
          (terminal.from
            (Functor.obj.{w, v, w, u} (C := WidePullbackShape ι)
              (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) none))
          fun (i : ι) ↦ limit.π (Discrete.functor fun (x : ι) ↦ X) { as := i }) ≫
        Functor.map (wideCospan ι X) (WidePullbackShape.Hom.id i) :
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) i ⟶
        Functor.obj.{w, v, w, u} (wideCospan ι X) i)

Tactic:
cases i