-- 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
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

Tactic:
simp only [comp_obj, id_obj, whiskerLeft_comp, assoc, mateEquiv_apply, whiskerLeft_twice,
  whiskerRight_comp, comp_app, whiskerLeft_app, whiskerRight_app, associator_hom_app, map_id,
  leftUnitor_hom_app, rightUnitor_inv_app, associator_inv_app, Functor.id_map, Functor.comp_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₂ : 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 :
  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))
⊢ ((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

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)
vcompb :
  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))
⊢ ((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:
simpa [mateEquiv]

Result:
no goals