Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ ({
              toFun := fun α ↦
                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.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 := ⋯ }
            (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))).natTrans.app
      b =
    (TwoSquare.mk R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃
            ((R₁.associator G₁ G₂).inv ≫
              whiskerRight
                  ({
                        toFun := fun α ↦
                          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.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 := ⋯ }
                      α).natTrans
                  G₂ ≫
                (H₁.associator R₂ G₂).hom ≫
                  H₁.whiskerLeft
                      ({
                            toFun := fun α ↦
                              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.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 := ⋯ }
                          β).natTrans ≫
                    (H₁.associator H₂ R₃).inv)).natTrans.app
      b

Tactic:
simp only [comp_obj, Equiv.coe_fn_mk, whiskerRight_comp, whiskerRight_twice, assoc,
    whiskerLeft_comp, comp_app, id_obj, rightUnitor_inv_app, Functor.whiskerLeft_app,
    associator_hom_app, associator_inv_app, Functor.whiskerRight_app, map_id, Functor.comp_map,
    leftUnitor_hom_app, comp_id, id_comp, whiskerLeft_twice, Iso.hom_inv_id_assoc]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫
      G₂.map (R₂.map (α.natTrans.app (R₁.obj b))) ≫
        G₂.map (R₂.map (H₁.map (adj₁.counit.app b))) ≫
          adj₃.unit.app (G₂.obj (R₂.obj (H₁.obj b))) ≫
            R₃.map (β.natTrans.app (R₂.obj (H₁.obj b))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))