-- 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₃)
      (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

Tactic:
unfold TwoSquare.whiskerLeft TwoSquare.whiskerTop conjugateEquiv

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₃) (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

Proof state:
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
⊢ (mateEquiv adj₁ adj₃) (β.whiskerLeft α) = ((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)

Tactic:
ext b

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
⊢ ((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
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b

Tactic:
have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β

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₃) ((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