-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem mateEquiv_conjugateEquiv_vcomp {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : C ⥤ D} {R₂ : D ⥤ C}
    {L₃ : C ⥤ D} {R₃ : D ⥤ C}
    (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (α : TwoSquare G L₁ L₂ H) (β : L₃ ⟶ L₂) :
    (mateEquiv adj₁ adj₃) (α.whiskerRight β) =
      (mateEquiv adj₁ adj₂ α).whiskerBottom (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₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((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₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃) (α ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) =
    (mateEquiv adj₁ adj₂) α ≫ᵥ (mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((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₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃) (α ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) =
    (mateEquiv adj₁ adj₂) α ≫ᵥ (mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((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₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          whiskerLeft G (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)).hom ≫
        whiskerRight ((mateEquiv adj₁ adj₂) α).natTrans (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).inv ≫
            whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)).natTrans ≫
              (H.associator (𝟭 D) R₃).hom)
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((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₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          whiskerLeft G (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)).hom ≫
        whiskerRight ((mateEquiv adj₁ adj₂) α).natTrans (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).inv ≫
            whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)).natTrans ≫
              (H.associator (𝟭 D) R₃).hom)
⊢ ((mateEquiv adj₁ adj₃) (TwoSquare.mk G L₁ L₃ H (whiskerLeft G β ≫ α.natTrans))).natTrans.app b =
    (TwoSquare.mk R₁ H G R₃
            (((mateEquiv adj₁ adj₂) α).natTrans ≫
              whiskerLeft H
                ((Trans.trans
                    (Trans.trans
                      (Trans.trans
                        (Trans.trans (L₃.leftUnitor.homCongr L₂.rightUnitor).symm
                          (equivNatTrans (𝟭 C) L₂ L₃ (𝟭 D)).symm)
                        (mateEquiv adj₂ adj₃))
                      (equivNatTrans R₂ (𝟭 D) (𝟭 C) R₃))
                    (R₂.rightUnitor.homCongr R₃.leftUnitor))
                  β))).natTrans.app
      b

Tactic:
have vcompb := congr_app vcomp 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₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          whiskerLeft G (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)).hom ≫
        whiskerRight ((mateEquiv adj₁ adj₂) α).natTrans (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).inv ≫
            whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)).natTrans ≫
              (H.associator (𝟭 D) R₃).hom)
vcompb :
  ((mateEquiv adj₁ adj₃)
          (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
            ((G.associator (𝟭 C) L₃).hom ≫
              whiskerLeft G (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
                (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom))).app
      b =
    (TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
          ((R₁.associator G (𝟭 C)).hom ≫
            whiskerRight ((mateEquiv adj₁ adj₂) α).natTrans (𝟭 C) ≫
              (H.associator R₂ (𝟭 C)).inv ≫
                whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)).natTrans ≫
                  (H.associator (𝟭 D) R₃).hom)).app
      b
⊢ ((mateEquiv adj₁ adj₃) (TwoSquare.mk G L₁ L₃ H (whiskerLeft G β ≫ α.natTrans))).natTrans.app b =
    (TwoSquare.mk R₁ H G R₃
            (((mateEquiv adj₁ adj₂) α).natTrans ≫
              whiskerLeft H
                ((Trans.trans
                    (Trans.trans
                      (Trans.trans
                        (Trans.trans (L₃.leftUnitor.homCongr L₂.rightUnitor).symm
                          (equivNatTrans (𝟭 C) L₂ L₃ (𝟭 D)).symm)
                        (mateEquiv adj₂ adj₃))
                      (equivNatTrans R₂ (𝟭 D) (𝟭 C) R₃))
                    (R₂.rightUnitor.homCongr R₃.leftUnitor))
                  β))).natTrans.app
      b