-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
inst_3 : Category.{v₄, u₄} F
G : Functor.{v₁, v₃, u₁, u₃} C E
H : Functor.{v₂, v₄, u₂, u₄} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
L₂ : Functor.{v₃, v₄, u₃, u₄} E F
R₂ : Functor.{v₄, v₃, u₄, u₃} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X : C
h :
  L₂.map (G.map (adj₁.unit.app X)) ≫ α.natTrans.app (R₁.obj (L₁.obj X)) ≫ H.map (adj₁.counit.app (L₁.obj X)) =
    α.natTrans.app X
⊢ app
      (natTrans
        ((fun (β : TwoSquare R₁ H G R₂) ↦
            TwoSquare.mk G L₁ L₂ H
              ((G ⋙ L₂).leftUnitor.inv ≫
                whiskerRight adj₁.unit (G ⋙ L₂) ≫
                  ((L₁ ⋙ R₁).associator G L₂).inv ≫
                    whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                      whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                        whiskerRight (L₁.associator H R₂).inv L₂ ≫
                          ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                            (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
          ((fun (α : TwoSquare G L₁ L₂ H) ↦
              TwoSquare.mk R₁ H G R₂
                ((R₁ ⋙ G).rightUnitor.inv ≫
                  (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                    (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                      R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                        R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                          R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                            (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                              whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
            α)))
      X =
    α.natTrans.app X

Tactic:
simp only [comp_obj, whiskerLeft_comp, whiskerLeft_twice, assoc, Iso.hom_inv_id_assoc,
      whiskerRight_comp, comp_app, id_obj, leftUnitor_inv_app, Functor.whiskerRight_app,
      Functor.comp_map, associator_inv_app, associator_hom_app, map_id, Functor.whiskerLeft_app,
      rightUnitor_inv_app, leftUnitor_hom_app, rightUnitor_hom_app, comp_id, id_comp,
      counit_naturality, counit_naturality_assoc, left_triangle_components_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.rightUnitor_hom_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Functor.whiskerLeft_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerLeft_twice, CategoryTheory.Functor.leftUnitor_inv_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.whiskerRight_comp, CategoryTheory.Adjunction.counit_naturality_assoc, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.rightUnitor_inv_app, CategoryTheory.Functor.leftUnitor_hom_app, CategoryTheory.Adjunction.left_triangle_components_assoc, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp