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.map f✝.unop.hom₃).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₃)) = 𝟙 (op (F.obj (unop X✝).obj₃)) ≫ (F.map f✝.unop.hom₃).op

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.map f✝.unop.hom₂).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₂)) = 𝟙 (op (F.obj (unop X✝).obj₂)) ≫ (F.map f✝.unop.hom₂).op

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.map f✝.unop.hom₁).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₁)) = 𝟙 (op (F.obj (unop X✝).obj₁)) ≫ (F.map f✝.unop.hom₁).op

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.map f✝.unop.hom₃).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₃)) = 𝟙 (op (F.obj (unop X✝).obj₃)) ≫ (F.map f✝.unop.hom₃).op

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.map f✝.unop.hom₂).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₂)) = 𝟙 (op (F.obj (unop X✝).obj₂)) ≫ (F.map f✝.unop.hom₂).op

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.map f✝.unop.hom₁).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₁)) = 𝟙 (op (F.obj (unop X✝).obj₁)) ≫ (F.map f✝.unop.hom₁).op