-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₁, v₃, u₁, u₃} A C
H : Functor.{v₂, v₄, u₂, u₄} B D
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₃, v₄, u₃, u₄} C D
R₃ : Functor.{v₄, v₃, u₄, u₃} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃ : (a : TwoSquare (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)) → TwoSquare R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          G.whiskerLeft (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
            (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom)) =
    TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
      ((R₁.associator G (𝟭 C)).inv ≫
        whiskerRight (natTrans ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α)) (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).hom ≫
            H.whiskerLeft
                (natTrans
                  ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
                    (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))) ≫
              (H.associator (𝟭 D) R₃).inv)
vcompb :
  app
      ((mateEquiv adj₁ adj₃ : (a : TwoSquare (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)) → TwoSquare R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃)
        (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
          ((G.associator (𝟭 C) L₃).hom ≫
            G.whiskerLeft (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
              (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom)))
      b =
    (TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
          ((R₁.associator G (𝟭 C)).inv ≫
            whiskerRight (natTrans ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α)) (𝟭 C) ≫
              (H.associator R₂ (𝟭 C)).hom ≫
                H.whiskerLeft
                    (natTrans
                      ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
                        (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))) ≫
                  (H.associator (𝟭 D) R₃).inv)).app
      b
⊢ adj₃.unit.app (G.obj (R₁.obj b)) ≫
      R₃.map (β.app (G.obj (R₁.obj b))) ≫ R₃.map (α.natTrans.app (R₁.obj b)) ≫ R₃.map (H.map (adj₁.counit.app b)) =
    adj₂.unit.app (G.obj (R₁.obj b)) ≫
      R₂.map (α.natTrans.app (R₁.obj b)) ≫
        R₂.map (H.map (adj₁.counit.app b)) ≫
          adj₃.unit.app (R₂.obj (H.obj b)) ≫ R₃.map (β.app (R₂.obj (H.obj b))) ≫ R₃.map (adj₂.counit.app (H.obj b))

Tactic:
simp only [comp_obj, id_obj, whiskerLeft_comp, assoc, mateEquiv_apply, whiskerLeft_twice,
    Iso.hom_inv_id_assoc, whiskerRight_comp, comp_app, Functor.whiskerLeft_app,
    Functor.whiskerRight_app, associator_hom_app, map_id, associator_inv_app, leftUnitor_hom_app,
    rightUnitor_inv_app, Functor.id_map, Functor.comp_map, id_comp, whiskerRight_twice,
    comp_id] at vcompb

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Functor.id_map, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Functor.whiskerLeft_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerLeft_twice, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.whiskerRight_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.rightUnitor_inv_app, CategoryTheory.Functor.leftUnitor_hom_app, CategoryTheory.Functor.whiskerRight_twice, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp, CategoryTheory.mateEquiv_apply