-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← U.cechIsoCechNerveApp_hom_π hT, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π