Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case h₁
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₁ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₁

pp: case h₂
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₂ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₂

pp: case h₃
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₃ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₃

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₁ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₁

case h₂
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₂ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₂

case h₃
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₃ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₃