-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
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 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  (F.map g ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁)) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
⊢ Eq.{v_2 + 1} (α := F.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁)
    (((Equiv.symm (adj.homEquiv Z (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁)) :
            Equiv.{v_1 + 1, v_2 + 1} (Z ⟶ G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁))
              (F.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁)) :
          (a : Z ⟶ G.obj ((shiftFunctor D 1).obj T.obj₁)) → F.obj Z ⟶ (shiftFunctor D 1).obj T.obj₁)
        (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁) :
      F.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁)
    (((Equiv.symm (adj.homEquiv Z (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁)) :
            Equiv.{v_1 + 1, v_2 + 1} (Z ⟶ G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁))
              (F.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁)) :
          (a : Z ⟶ G.obj ((shiftFunctor D 1).obj T.obj₁)) → F.obj Z ⟶ (shiftFunctor D 1).obj T.obj₁)
        (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
              (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
            h ≫
          G.map T.mor₃) :
      F.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) T.obj₁)

Tactic:
simp only [Functor.comp_obj, homEquiv_counit, Functor.id_obj, Functor.map_comp, assoc,
        homEquiv_unit, counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
        ← h₂, adj.shift_counit_app, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.shift_counit_app, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Adjunction.counit_naturality_assoc, CategoryTheory.Adjunction.left_triangle_components_assoc