-- Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
H₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₁ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
R₁ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
H₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
eL : Equivalence.{v_2, v_3, u_2, u_3} C₂ C₃
eR : Equivalence.{v_5, v_6, u_5, u_6} D₂ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this_1 : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ :=
  (CatCommSq.vInvEquiv H₂ eL eR H₃ :
      (a : CatCommSq H₂ eL.functor eR.functor H₃) → CatCommSq H₃ eL.inverse eR.inverse H₂)
    inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
h :
  w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map ((natTrans w'.hom).app (L₁.obj X₁)) ≫
          eR.inverse.map (H₃.map (eL.counitIso.inv.app (eL.functor.obj (L₁.obj X₁)))) ≫
            eR.inverse.map
                ((CatCommSq.iso H₂ eL.functor eR.functor H₃).inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
              eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
                H₂.map (eL.unitIso.inv.app (L₁.obj X₁))
⊢ w.natTrans.app X₁ = ((w ≫ᵥ w'.hom).vComp' w''.hom α β).natTrans.app X₁

Tactic:
simp only [Functor.comp_obj, vComp'_app, Iso.trans_inv, Functor.isoWhiskerLeft_inv,
          Iso.symm_inv, assoc, NatTrans.comp_app, Functor.id_obj, Functor.rightUnitor_inv_app,
          Functor.whiskerLeft_app, Functor.associator_inv_app, comp_id, id_comp, vComp_app,
          Functor.map_comp, Equivalence.inv_fun_map, CatCommSq.vInv_iso_hom_app, Iso.trans_hom,
          Functor.isoWhiskerLeft_hom, Iso.symm_hom, Functor.associator_hom_app,
          Functor.rightUnitor_hom_app, Iso.hom_inv_id_app_assoc, w'', α, β]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Equivalence.inv_fun_map, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.rightUnitor_hom_app, CategoryTheory.Iso.symm_hom, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.CatCommSq.vInv_iso_hom_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Iso.symm_inv, CategoryTheory.Category.comp_id, CategoryTheory.Functor.isoWhiskerLeft_inv, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.TwoSquare.vComp_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.TwoSquare.vComp'_app, CategoryTheory.Functor.rightUnitor_inv_app, CategoryTheory.Functor.isoWhiskerLeft_hom, CategoryTheory.Iso.trans_inv, CategoryTheory.Category.id_comp