-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_mateEquiv_vcomp {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : A ⥤ B} {R₂ : B ⥤ A}
    {L₃ : C ⥤ D} {R₃ : D ⥤ C}
    (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (α : L₂ ⟶ L₁) (β : TwoSquare G L₂ L₃ H) :
    (mateEquiv adj₁ adj₃) (β.whiskerLeft α) =
      (mateEquiv adj₂ adj₃ β).whiskerTop (conjugateEquiv adj₁ adj₂ α)

Proof state:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃) ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ β) =
    (mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ᵥ (mateEquiv adj₂ adj₃) β
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b

Tactic:
unfold vComp hComp at vcomp

Result:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (((𝟭 A).associator G L₃).hom ≫
          whiskerLeft (𝟭 A) β.natTrans ≫
            ((𝟭 A).associator L₂ H).inv ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).hom ≫
        whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
          ((𝟭 B).associator R₂ G).inv ≫
            whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).hom)
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b

Proof state:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (((𝟭 A).associator G L₃).hom ≫
          whiskerLeft (𝟭 A) β.natTrans ≫
            ((𝟭 A).associator L₂ H).inv ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).hom ≫
        whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
          ((𝟭 B).associator R₂ G).inv ≫
            whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).hom)
vcompb :
  ((mateEquiv adj₁ adj₃)
          (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
            (((𝟭 A).associator G L₃).hom ≫
              whiskerLeft (𝟭 A) β.natTrans ≫
                ((𝟭 A).associator L₂ H).inv ≫
                  whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫
                    (L₁.associator (𝟭 B) H).hom))).app
      b =
    (TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
          ((R₁.associator (𝟭 A) G).hom ≫
            whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
              ((𝟭 B).associator R₂ G).inv ≫
                whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).hom)).app
      b
⊢ ((mateEquiv adj₁ adj₃) (TwoSquare.mk G L₁ L₃ H (β.natTrans ≫ whiskerRight α H))).natTrans.app b =
    (TwoSquare.mk R₁ H G R₃
            (whiskerRight
                ((Trans.trans
                    (Trans.trans
                      (Trans.trans
                        (Trans.trans (L₂.leftUnitor.homCongr L₁.rightUnitor).symm
                          (equivNatTrans (𝟭 A) L₁ L₂ (𝟭 B)).symm)
                        (mateEquiv adj₁ adj₂))
                      (equivNatTrans R₁ (𝟭 B) (𝟭 A) R₂))
                    (R₁.rightUnitor.homCongr R₂.leftUnitor))
                  α)
                G ≫
              ((mateEquiv adj₂ adj₃) β).natTrans)).natTrans.app
      b

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

Result:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (((𝟭 A).associator G L₃).hom ≫
          whiskerLeft (𝟭 A) β.natTrans ≫
            ((𝟭 A).associator L₂ H).inv ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).hom ≫
        whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
          ((𝟭 B).associator R₂ G).inv ≫
            whiskerLeft (𝟭 B) ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).hom)
vcompb :
  adj₃.unit.app (G.obj (R₁.obj b)) ≫
      R₃.map (β.natTrans.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) =
    G.map (adj₂.unit.app (R₁.obj b)) ≫
      G.map (R₂.map (α.app (R₁.obj b))) ≫
        G.map (R₂.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))
⊢ ((mateEquiv adj₁ adj₃) (TwoSquare.mk G L₁ L₃ H (β.natTrans ≫ whiskerRight α H))).natTrans.app b =
    (TwoSquare.mk R₁ H G R₃
            (whiskerRight
                ((Trans.trans
                    (Trans.trans
                      (Trans.trans
                        (Trans.trans (L₂.leftUnitor.homCongr L₁.rightUnitor).symm
                          (equivNatTrans (𝟭 A) L₁ L₂ (𝟭 B)).symm)
                        (mateEquiv adj₁ adj₂))
                      (equivNatTrans R₁ (𝟭 B) (𝟭 A) R₂))
                    (R₁.rightUnitor.homCongr R₂.leftUnitor))
                  α)
                G ≫
              ((mateEquiv adj₂ adj₃) β).natTrans)).natTrans.app
      b