-- 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ᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
    (NatTrans.app
        (Iso.hom
          (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
            (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₃ b₃ ⋯))
        X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, 0} C ℤ) b₁ b₂ b₃ ⋯)) X ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₂ b₂ ⋯))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (Functor.map
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (NatTrans.app
              (Iso.inv
                (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                  (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₁ b₁ ⋯))
              X)))
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))
have rw : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
  (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₃) X)
    (NatTrans.app
      (Iso.hom
        (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
          (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₃ b₃ sorry))
      X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1}
          (shiftFunctor
            (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
              (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
            a₂)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
        (NatTrans.app
          (Iso.inv
            (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
              (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₂ b₂ sorry))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
        (Functor.map
          (shiftFunctor
            (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
              (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
            a₂)
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₁ b₁ sorry))
            X))))
  (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
          (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
        Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))
Tactic: rw [oppositeShiftFunctorAdd'_hom_app]