-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
this :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    (Triangle.mk o.m₃.op o.m₁.op
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₂₃))))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) Z₂₃ :
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) Z₂₃ ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1) Z₂₃)
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            ((Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₂₃.unop) ≫
                NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₂) ≫
              v₁₂) :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₂₃))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) Z₁₂)))
⊢ w₂₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) v₁₂ =
    CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₂₃))))
      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) Z₂₃ :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) Z₂₃ ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1) Z₂₃)
      (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          ((Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₂₃.unop) ≫
              NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₂) ≫
            v₁₂) :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₂₃))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) Z₁₂)
have h : w₂₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) v₁₂ =
  CategoryStruct.comp (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₂₃))))
    (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) Z₂₃ :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) Z₂₃ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1) Z₂₃)
    (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
        (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₂₃.unop) ≫
          NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₂ ≫ v₁₂) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₂₃))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) Z₁₂)
Tactic: rw [Category.assoc, Functor.map_comp, Functor.map_comp,
        ← opShiftFunctorEquivalence_counitIso_hom_app_shift,
        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, Iso.inv_hom_id_app_assoc]