-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫ NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₂ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₃ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₄ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
            NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₅ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      Quiver.Hom.op (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0) (Opposite.unop X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₆ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0) (Opposite.unop X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₇ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫ NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
have rw₈ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
  (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X))
  (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X))
Tactic: rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
    id_comp, Iso.hom_inv_id_app]