Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₁ ≫
      (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₂).hom =
    (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₁

pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₂ ≫
      (mapHomologicalComplexIso φ G).hom =
    (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₂).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₂

pp: case refine_3
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) 1).map
        (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃

Tactic:
· dsimp
    simp only [comp_id, id_comp]

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₂ ≫
      (mapHomologicalComplexIso φ G).hom =
    (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₂).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₂

case refine_3
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) 1).map
        (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃