-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem iterated_mateEquiv_conjugateEquiv (α : TwoSquare F₁ L₁ L₂ F₂) :
    (mateEquiv adj₄ adj₃ (mateEquiv adj₁ adj₂ α)).natTrans =
      conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) α

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
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
⊢ ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

Tactic:
ext d

Result:
case w.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
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
d : D
⊢ ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans.app d =
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α).app d

Proof state:
case w.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
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
d : D
⊢ ({
              toFun := fun α =>
                TwoSquare.mk U₂ R₂ R₁ U₁
                  (whiskerLeft (U₂ ⋙ R₁) adj₃.unit ≫
                    whiskerRight (whiskerLeft U₂ α.natTrans) U₁ ≫ whiskerRight adj₄.counit (R₂ ⋙ U₁)),
              invFun := fun β =>
                TwoSquare.mk R₁ F₂ F₁ R₂
                  (whiskerRight adj₄.unit (R₁ ⋙ F₁) ≫
                    whiskerRight (whiskerLeft F₂ β.natTrans) F₁ ≫ whiskerLeft (F₂ ⋙ R₂) adj₃.counit),
              left_inv := ⋯, right_inv := ⋯ }
            ({
                toFun := fun α =>
                  TwoSquare.mk R₁ F₂ F₁ R₂
                    (whiskerLeft (R₁ ⋙ F₁) adj₂.unit ≫
                      whiskerRight (whiskerLeft R₁ α.natTrans) R₂ ≫ whiskerRight adj₁.counit (F₂ ⋙ R₂)),
                invFun := fun β =>
                  TwoSquare.mk F₁ L₁ L₂ F₂
                    (whiskerRight adj₁.unit (F₁ ⋙ L₂) ≫
                      whiskerRight (whiskerLeft L₁ β.natTrans) L₂ ≫ whiskerLeft (L₁ ⋙ F₂) adj₂.counit),
                left_inv := ⋯, right_inv := ⋯ }
              α)).natTrans.app
      d =
    ((Trans.trans
            (Trans.trans
              (Trans.trans
                (Trans.trans ((F₁ ⋙ L₂).leftUnitor.homCongr (L₁ ⋙ F₂).rightUnitor).symm
                  (equivNatTrans (𝟭 A) (L₁ ⋙ F₂) (F₁ ⋙ L₂) (𝟭 D)).symm)
                {
                  toFun := fun α =>
                    TwoSquare.mk (U₂ ⋙ R₁) (𝟭 D) (𝟭 A) (R₂ ⋙ U₁)
                      (whiskerLeft ((U₂ ⋙ R₁) ⋙ 𝟭 A)
                          (mk'
                              {
                                homEquiv := fun x x_1 =>
                                  (adj₂.homEquiv (F₁.obj x) x_1).trans (adj₃.homEquiv x (R₂.obj x_1)),
                                unit :=
                                  adj₃.unit ≫
                                    whiskerRight
                                        (F₁.rightUnitor.inv ≫ whiskerLeft F₁ adj₂.unit ≫ (F₁.associator L₂ R₂).inv) U₁ ≫
                                      ((F₁ ⋙ L₂).associator R₂ U₁).hom,
                                counit :=
                                  ((R₂ ⋙ U₁).associator F₁ L₂).inv ≫
                                    whiskerRight
                                        ((R₂.associator U₁ F₁).hom ≫ whiskerLeft R₂ adj₃.counit ≫ R₂.rightUnitor.hom)
                                        L₂ ≫
                                      adj₂.counit,
                                homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit ≫
                        whiskerRight (whiskerLeft (U₂ ⋙ R₁) α.natTrans) (R₂ ⋙ U₁) ≫
                          whiskerRight
                            (mk'
                                {
                                  homEquiv := fun x x_1 =>
                                    (adj₄.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (U₂.obj x_1)),
                                  unit :=
                                    adj₁.unit ≫
                                      whiskerRight
                                          (L₁.rightUnitor.inv ≫ whiskerLeft L₁ adj₄.unit ≫ (L₁.associator F₂ U₂).inv)
                                          R₁ ≫
                                        ((L₁ ⋙ F₂).associator U₂ R₁).hom,
                                  counit :=
                                    ((U₂ ⋙ R₁).associator L₁ F₂).inv ≫
                                      whiskerRight
                                          ((U₂.associator R₁ L₁).hom ≫ whiskerLeft U₂ adj₁.counit ≫ U₂.rightUnitor.hom)
                                          F₂ ≫
                                        adj₄.counit,
                                  homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit
                            (𝟭 D ⋙ R₂ ⋙ U₁)),
                  invFun := fun β =>
                    TwoSquare.mk (𝟭 A) (L₁ ⋙ F₂) (F₁ ⋙ L₂) (𝟭 D)
                      (whiskerRight
                          (mk'
                              {
                                homEquiv := fun x x_1 =>
                                  (adj₄.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (U₂.obj x_1)),
                                unit :=
                                  adj₁.unit ≫
                                    whiskerRight
                                        (L₁.rightUnitor.inv ≫ whiskerLeft L₁ adj₄.unit ≫ (L₁.associator F₂ U₂).inv) R₁ ≫
                                      ((L₁ ⋙ F₂).associator U₂ R₁).hom,
                                counit :=
                                  ((U₂ ⋙ R₁).associator L₁ F₂).inv ≫
                                    whiskerRight
                                        ((U₂.associator R₁ L₁).hom ≫ whiskerLeft U₂ adj₁.counit ≫ U₂.rightUnitor.hom)
                                        F₂ ≫
                                      adj₄.counit,
                                homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit
                          (𝟭 A ⋙ F₁ ⋙ L₂) ≫
                        whiskerRight (whiskerLeft (L₁ ⋙ F₂) β.natTrans) (F₁ ⋙ L₂) ≫
                          whiskerLeft ((L₁ ⋙ F₂) ⋙ 𝟭 D)
                            (mk'
                                {
                                  homEquiv := fun x x_1 =>
                                    (adj₂.homEquiv (F₁.obj x) x_1).trans (adj₃.homEquiv x (R₂.obj x_1)),
                                  unit :=
                                    adj₃.unit ≫
                                      whiskerRight
                                          (F₁.rightUnitor.inv ≫ whiskerLeft F₁ adj₂.unit ≫ (F₁.associator L₂ R₂).inv)
                                          U₁ ≫
                                        ((F₁ ⋙ L₂).associator R₂ U₁).hom,
                                  counit :=
                                    ((R₂ ⋙ U₁).associator F₁ L₂).inv ≫
                                      whiskerRight
                                          ((R₂.associator U₁ F₁).hom ≫ whiskerLeft R₂ adj₃.counit ≫ R₂.rightUnitor.hom)
                                          L₂ ≫
                                        adj₂.counit,
                                  homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit),
                  left_inv := ⋯, right_inv := ⋯ })
              (equivNatTrans (U₂ ⋙ R₁) (𝟭 D) (𝟭 A) (R₂ ⋙ U₁)))
            ((U₂ ⋙ R₁).rightUnitor.homCongr (R₂ ⋙ U₁).leftUnitor))
          α).app
      d

Tactic:
simp

Result:
no goals