-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
refine_1 :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Triangle.obj₁ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))
      (Triangle.obj₂
        (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))
    (Triangle.mor₁ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₂
            (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))))
    (Iso.hom
        (Iso.refl
          (Triangle.obj₁
            (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))) ≫
      Triangle.mor₁
        (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
refine_2 :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Triangle.obj₂ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))
      (Triangle.obj₃
        (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))
    (Triangle.mor₂ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)) ≫
        Iso.hom (mapHomologicalComplexIso φ G) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Triangle.obj₂ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))
        (Triangle.obj₃
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))
    (Iso.hom
          (Iso.refl
            (Triangle.obj₂
              (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))) ≫
        Triangle.mor₂
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Triangle.obj₂ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))
        (Triangle.obj₃
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))
refine_3 :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Triangle.obj₃ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))
      (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Triangle.obj₁
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))))
    (Triangle.mor₃ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)) ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Iso.hom
          (Iso.refl
            (Triangle.obj₁
              (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ))))))
    (CategoryStruct.comp (Y :=
      Triangle.obj₃
        (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
      (Iso.hom (mapHomologicalComplexIso φ G) :
        Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
          (Triangle.obj₃ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))
          (Triangle.obj₃
            (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))
      (Triangle.mor₃
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
        Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
          (Triangle.obj₃
            (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Triangle.obj₁
              (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
                (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))))
⊢ Iso (C := Triangle (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)))
    (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ))
    (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (mapHomologicalComplexIso φ G) ?_ ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk