-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G₁ : Functor.{v₁, v₃, u₁, u₃} A C
G₂ : Functor.{v₃, v₅, u₃, u₅} C E
H₁ : Functor.{v₂, v₄, u₂, u₄} B D
H₂ : Functor.{v₄, v₆, u₄, u₆} D F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₃, v₄, u₃, u₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
L₃ : Functor.{v₅, v₆, u₅, u₆} E F
R₃ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
h :
  ∀ (b : B),
    app
        (natTrans
          (({
                toFun := fun (α : TwoSquare (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)) ↦
                  TwoSquare.mk R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃
                    ((R₁ ⋙ G₁ ⋙ G₂).rightUnitor.inv ≫
                      (R₁ ⋙ G₁ ⋙ G₂).whiskerLeft adj₃.unit ≫
                        (R₁.associator (G₁ ⋙ G₂) (L₃ ⋙ R₃)).hom ≫
                          R₁.whiskerLeft ((G₁ ⋙ G₂).associator L₃ R₃).inv ≫
                            R₁.whiskerLeft (whiskerRight α.natTrans R₃) ≫
                              R₁.whiskerLeft (L₁.associator (H₁ ⋙ H₂) R₃).hom ≫
                                (R₁.associator L₁ ((H₁ ⋙ H₂) ⋙ R₃)).inv ≫
                                  whiskerRight adj₁.counit ((H₁ ⋙ H₂) ⋙ R₃) ≫ ((H₁ ⋙ H₂) ⋙ R₃).leftUnitor.hom),
                invFun := fun (β : TwoSquare R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃) ↦
                  TwoSquare.mk (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)
                    (((G₁ ⋙ G₂) ⋙ L₃).leftUnitor.inv ≫
                      whiskerRight adj₁.unit ((G₁ ⋙ G₂) ⋙ L₃) ≫
                        ((L₁ ⋙ R₁).associator (G₁ ⋙ G₂) L₃).inv ≫
                          whiskerRight (L₁.associator R₁ (G₁ ⋙ G₂)).hom L₃ ≫
                            whiskerRight (L₁.whiskerLeft β.natTrans) L₃ ≫
                              whiskerRight (L₁.associator (H₁ ⋙ H₂) R₃).inv L₃ ≫
                                ((L₁ ⋙ H₁ ⋙ H₂).associator R₃ L₃).hom ≫
                                  (L₁ ⋙ H₁ ⋙ H₂).whiskerLeft adj₃.counit ≫ (L₁ ⋙ H₁ ⋙ H₂).rightUnitor.hom),
                left_inv := ⋯, right_inv := ⋯ } :
              (a : TwoSquare (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)) → TwoSquare R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃)
            (TwoSquare.mk (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)
              ((G₁.associator G₂ L₃).hom ≫
                G₁.whiskerLeft β.natTrans ≫
                  (G₁.associator L₂ H₂).inv ≫ whiskerRight α.natTrans H₂ ≫ (L₁.associator H₁ H₂).hom))))
        b =
      (TwoSquare.mk R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃
              ((R₁.associator G₁ G₂).inv ≫
                whiskerRight
                    (natTrans
                      (({
                            toFun := fun (α : TwoSquare G₁ L₁ L₂ H₁) ↦
                              TwoSquare.mk R₁ H₁ G₁ R₂
                                ((R₁ ⋙ G₁).rightUnitor.inv ≫
                                  (R₁ ⋙ G₁).whiskerLeft adj₂.unit ≫
                                    (R₁.associator G₁ (L₂ ⋙ R₂)).hom ≫
                                      R₁.whiskerLeft (G₁.associator L₂ R₂).inv ≫
                                        R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                                          R₁.whiskerLeft (L₁.associator H₁ R₂).hom ≫
                                            (R₁.associator L₁ (H₁ ⋙ R₂)).inv ≫
                                              whiskerRight adj₁.counit (H₁ ⋙ R₂) ≫ (H₁ ⋙ R₂).leftUnitor.hom),
                            invFun := fun (β : TwoSquare R₁ H₁ G₁ R₂) ↦
                              TwoSquare.mk G₁ L₁ L₂ H₁
                                ((G₁ ⋙ L₂).leftUnitor.inv ≫
                                  whiskerRight adj₁.unit (G₁ ⋙ L₂) ≫
                                    ((L₁ ⋙ R₁).associator G₁ L₂).inv ≫
                                      whiskerRight (L₁.associator R₁ G₁).hom L₂ ≫
                                        whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                                          whiskerRight (L₁.associator H₁ R₂).inv L₂ ≫
                                            ((L₁ ⋙ H₁).associator R₂ L₂).hom ≫
                                              (L₁ ⋙ H₁).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H₁).rightUnitor.hom),
                            left_inv := ⋯, right_inv := ⋯ : TwoSquare G₁ L₁ L₂ H₁ ≃ TwoSquare R₁ H₁ G₁ R₂ } :
                          (a : TwoSquare G₁ L₁ L₂ H₁) → TwoSquare R₁ H₁ G₁ R₂)
                        α))
                    G₂ ≫
                  (H₁.associator R₂ G₂).hom ≫
                    H₁.whiskerLeft
                        (natTrans
                          (({
                                toFun := fun (α : TwoSquare G₂ L₂ L₃ H₂) ↦
                                  TwoSquare.mk R₂ H₂ G₂ R₃
                                    ((R₂ ⋙ G₂).rightUnitor.inv ≫
                                      (R₂ ⋙ G₂).whiskerLeft adj₃.unit ≫
                                        (R₂.associator G₂ (L₃ ⋙ R₃)).hom ≫
                                          R₂.whiskerLeft (G₂.associator L₃ R₃).inv ≫
                                            R₂.whiskerLeft (whiskerRight α.natTrans R₃) ≫
                                              R₂.whiskerLeft (L₂.associator H₂ R₃).hom ≫
                                                (R₂.associator L₂ (H₂ ⋙ R₃)).inv ≫
                                                  whiskerRight adj₂.counit (H₂ ⋙ R₃) ≫ (H₂ ⋙ R₃).leftUnitor.hom),
                                invFun := fun (β : TwoSquare R₂ H₂ G₂ R₃) ↦
                                  TwoSquare.mk G₂ L₂ L₃ H₂
                                    ((G₂ ⋙ L₃).leftUnitor.inv ≫
                                      whiskerRight adj₂.unit (G₂ ⋙ L₃) ≫
                                        ((L₂ ⋙ R₂).associator G₂ L₃).inv ≫
                                          whiskerRight (L₂.associator R₂ G₂).hom L₃ ≫
                                            whiskerRight (L₂.whiskerLeft β.natTrans) L₃ ≫
                                              whiskerRight (L₂.associator H₂ R₃).inv L₃ ≫
                                                ((L₂ ⋙ H₂).associator R₃ L₃).hom ≫
                                                  (L₂ ⋙ H₂).whiskerLeft adj₃.counit ≫ (L₂ ⋙ H₂).rightUnitor.hom),
                                left_inv := ⋯, right_inv := ⋯ : TwoSquare G₂ L₂ L₃ H₂ ≃ TwoSquare R₂ H₂ G₂ R₃ } :
                              (a : TwoSquare G₂ L₂ L₃ H₂) → TwoSquare R₂ H₂ G₂ R₃)
                            β)) ≫
                      (H₁.associator H₂ R₃).inv)).natTrans.app
        b
⊢ ({
          toFun := fun (α : TwoSquare (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)) ↦
            TwoSquare.mk R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃
              ((R₁ ⋙ G₁ ⋙ G₂).rightUnitor.inv ≫
                (R₁ ⋙ G₁ ⋙ G₂).whiskerLeft adj₃.unit ≫
                  (R₁.associator (G₁ ⋙ G₂) (L₃ ⋙ R₃)).hom ≫
                    R₁.whiskerLeft ((G₁ ⋙ G₂).associator L₃ R₃).inv ≫
                      R₁.whiskerLeft (whiskerRight α.natTrans R₃) ≫
                        R₁.whiskerLeft (L₁.associator (H₁ ⋙ H₂) R₃).hom ≫
                          (R₁.associator L₁ ((H₁ ⋙ H₂) ⋙ R₃)).inv ≫
                            whiskerRight adj₁.counit ((H₁ ⋙ H₂) ⋙ R₃) ≫ ((H₁ ⋙ H₂) ⋙ R₃).leftUnitor.hom),
          invFun := fun (β : TwoSquare R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃) ↦
            TwoSquare.mk (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)
              (((G₁ ⋙ G₂) ⋙ L₃).leftUnitor.inv ≫
                whiskerRight adj₁.unit ((G₁ ⋙ G₂) ⋙ L₃) ≫
                  ((L₁ ⋙ R₁).associator (G₁ ⋙ G₂) L₃).inv ≫
                    whiskerRight (L₁.associator R₁ (G₁ ⋙ G₂)).hom L₃ ≫
                      whiskerRight (L₁.whiskerLeft β.natTrans) L₃ ≫
                        whiskerRight (L₁.associator (H₁ ⋙ H₂) R₃).inv L₃ ≫
                          ((L₁ ⋙ H₁ ⋙ H₂).associator R₃ L₃).hom ≫
                            (L₁ ⋙ H₁ ⋙ H₂).whiskerLeft adj₃.counit ≫ (L₁ ⋙ H₁ ⋙ H₂).rightUnitor.hom),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : TwoSquare (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)) → TwoSquare R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃)
      (TwoSquare.mk (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)
        ((G₁.associator G₂ L₃).hom ≫
          G₁.whiskerLeft β.natTrans ≫
            (G₁.associator L₂ H₂).inv ≫ whiskerRight α.natTrans H₂ ≫ (L₁.associator H₁ H₂).hom)) =
    TwoSquare.mk R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃
      ((R₁.associator G₁ G₂).inv ≫
        whiskerRight
            (natTrans
              (({
                    toFun := fun (α : TwoSquare G₁ L₁ L₂ H₁) ↦
                      TwoSquare.mk R₁ H₁ G₁ R₂
                        ((R₁ ⋙ G₁).rightUnitor.inv ≫
                          (R₁ ⋙ G₁).whiskerLeft adj₂.unit ≫
                            (R₁.associator G₁ (L₂ ⋙ R₂)).hom ≫
                              R₁.whiskerLeft (G₁.associator L₂ R₂).inv ≫
                                R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                                  R₁.whiskerLeft (L₁.associator H₁ R₂).hom ≫
                                    (R₁.associator L₁ (H₁ ⋙ R₂)).inv ≫
                                      whiskerRight adj₁.counit (H₁ ⋙ R₂) ≫ (H₁ ⋙ R₂).leftUnitor.hom),
                    invFun := fun (β : TwoSquare R₁ H₁ G₁ R₂) ↦
                      TwoSquare.mk G₁ L₁ L₂ H₁
                        ((G₁ ⋙ L₂).leftUnitor.inv ≫
                          whiskerRight adj₁.unit (G₁ ⋙ L₂) ≫
                            ((L₁ ⋙ R₁).associator G₁ L₂).inv ≫
                              whiskerRight (L₁.associator R₁ G₁).hom L₂ ≫
                                whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                                  whiskerRight (L₁.associator H₁ R₂).inv L₂ ≫
                                    ((L₁ ⋙ H₁).associator R₂ L₂).hom ≫
                                      (L₁ ⋙ H₁).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H₁).rightUnitor.hom),
                    left_inv := ⋯, right_inv := ⋯ : TwoSquare G₁ L₁ L₂ H₁ ≃ TwoSquare R₁ H₁ G₁ R₂ } :
                  (a : TwoSquare G₁ L₁ L₂ H₁) → TwoSquare R₁ H₁ G₁ R₂)
                α))
            G₂ ≫
          (H₁.associator R₂ G₂).hom ≫
            H₁.whiskerLeft
                (natTrans
                  (({
                        toFun := fun (α : TwoSquare G₂ L₂ L₃ H₂) ↦
                          TwoSquare.mk R₂ H₂ G₂ R₃
                            ((R₂ ⋙ G₂).rightUnitor.inv ≫
                              (R₂ ⋙ G₂).whiskerLeft adj₃.unit ≫
                                (R₂.associator G₂ (L₃ ⋙ R₃)).hom ≫
                                  R₂.whiskerLeft (G₂.associator L₃ R₃).inv ≫
                                    R₂.whiskerLeft (whiskerRight α.natTrans R₃) ≫
                                      R₂.whiskerLeft (L₂.associator H₂ R₃).hom ≫
                                        (R₂.associator L₂ (H₂ ⋙ R₃)).inv ≫
                                          whiskerRight adj₂.counit (H₂ ⋙ R₃) ≫ (H₂ ⋙ R₃).leftUnitor.hom),
                        invFun := fun (β : TwoSquare R₂ H₂ G₂ R₃) ↦
                          TwoSquare.mk G₂ L₂ L₃ H₂
                            ((G₂ ⋙ L₃).leftUnitor.inv ≫
                              whiskerRight adj₂.unit (G₂ ⋙ L₃) ≫
                                ((L₂ ⋙ R₂).associator G₂ L₃).inv ≫
                                  whiskerRight (L₂.associator R₂ G₂).hom L₃ ≫
                                    whiskerRight (L₂.whiskerLeft β.natTrans) L₃ ≫
                                      whiskerRight (L₂.associator H₂ R₃).inv L₃ ≫
                                        ((L₂ ⋙ H₂).associator R₃ L₃).hom ≫
                                          (L₂ ⋙ H₂).whiskerLeft adj₃.counit ≫ (L₂ ⋙ H₂).rightUnitor.hom),
                        left_inv := ⋯, right_inv := ⋯ : TwoSquare G₂ L₂ L₃ H₂ ≃ TwoSquare R₂ H₂ G₂ R₃ } :
                      (a : TwoSquare G₂ L₂ L₃ H₂) → TwoSquare R₂ H₂ G₂ R₃)
                    β)) ≫
              (H₁.associator H₂ R₃).inv)

Tactic:
ext b