-- Lean 4 proof step from Mathlib.AlgebraicTopology.CechNerve (goal)
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 j : WidePullbackShape ι
f : i ⟶ j
⊢ 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) j)
    (Functor.map (Functor.obj (Functor.const (WidePullbackShape ι)) (piObj.{w, v, u} fun (x : ι) ↦ X)) f ≫
        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)
          j
          (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) j)
    ((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) f :
      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) j)
have id : 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 f
Cleared hypotheses: j, f