-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
n : SimplexCategoryᵒᵖ
i :
  ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC := fun (X : SimplexCategory) ↦
    Fin (X.len + 1)) (Opposite.unop n)
rw :
  Eq (α := (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
    (CategoryStruct.comp (Y := Functor.obj U.cech n) (Iso.inv (U.cechIsoCechNerveApp hT n))
        (Iso.hom (U.cechIsoCechNerveApp hT n) ≫
          WidePullback.π
            (fun
                (x :
                  ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                    fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
              (isTerminalIncl T hT).from U)
            i) :
      (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
    (WidePullback.π
        (fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          (isTerminalIncl T hT).from U)
        i :
      (widePullback (Functor.obj (incl C) T)
          (fun
              (x :
                ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                  fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
            U)
          fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          (isTerminalIncl T hT).from U) ⟶
        U)
⊢ Eq (α := (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
    (CategoryStruct.comp (Y := Functor.obj U.cech n) (Iso.inv (U.cechIsoCechNerveApp hT n)) (U.powerπ i) :
      (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
    (WidePullback.π
        (fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          (isTerminalIncl T hT).from U)
        i :
      (widePullback (Functor.obj (incl C) T)
          (fun
              (x :
                ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                  fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
            U)
          fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          (isTerminalIncl T hT).from U) ⟶
        U)
have rw₁ : Eq (α := (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
  (WidePullback.π
    (fun
        (x :
          ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
      (isTerminalIncl T hT).from U)
    i)
  (WidePullback.π
    (fun
        (x :
          ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
      (isTerminalIncl T hT).from U)
    i)
Tactic: rw [← U.cechIsoCechNerveApp_hom_π hT, Iso.inv_hom_id_assoc]