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 ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ ({
              toFun := fun α ↦
                TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
                  (((R₃ ⋙ R₁) ⋙ G).rightUnitor.inv ≫
                    ((R₃ ⋙ R₁) ⋙ G).whiskerLeft
                        (Adjunction.mk'
                            {
                              homEquiv := fun x x_1 ↦
                                (adj₄.homEquiv (L₂.obj x) x_1).trans (adj₂.homEquiv x (R₄.obj x_1)),
                              unit :=
                                adj₂.unit ≫
                                  whiskerRight
                                      (L₂.rightUnitor.inv ≫ L₂.whiskerLeft adj₄.unit ≫ (L₂.associator L₄ R₄).inv) R₂ ≫
                                    ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                              counit :=
                                ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                                  whiskerRight
                                      ((R₄.associator R₂ L₂).hom ≫ R₄.whiskerLeft adj₂.counit ≫ R₄.rightUnitor.hom) L₄ ≫
                                    adj₄.counit,
                              homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit ≫
                      ((R₃ ⋙ R₁).associator G ((L₂ ⋙ L₄) ⋙ R₄ ⋙ R₂)).hom ≫
                        (R₃ ⋙ R₁).whiskerLeft (G.associator (L₂ ⋙ L₄) (R₄ ⋙ R₂)).inv ≫
                          (R₃ ⋙ R₁).whiskerLeft (whiskerRight α.natTrans (R₄ ⋙ R₂)) ≫
                            (R₃ ⋙ R₁).whiskerLeft ((L₁ ⋙ L₃).associator K (R₄ ⋙ R₂)).hom ≫
                              ((R₃ ⋙ R₁).associator (L₁ ⋙ L₃) (K ⋙ R₄ ⋙ R₂)).inv ≫
                                whiskerRight
                                    (Adjunction.mk'
                                        {
                                          homEquiv := fun x x_1 ↦
                                            (adj₃.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (R₃.obj x_1)),
                                          unit :=
                                            adj₁.unit ≫
                                              whiskerRight
                                                  (L₁.rightUnitor.inv ≫
                                                    L₁.whiskerLeft adj₃.unit ≫ (L₁.associator L₃ R₃).inv)
                                                  R₁ ≫
                                                ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                                          counit :=
                                            ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                                              whiskerRight
                                                  ((R₃.associator R₁ L₁).hom ≫
                                                    R₃.whiskerLeft adj₁.counit ≫ R₃.rightUnitor.hom)
                                                  L₃ ≫
                                                adj₃.counit,
                                          homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit
                                    (K ⋙ R₄ ⋙ R₂) ≫
                                  (K ⋙ R₄ ⋙ R₂).leftUnitor.hom),
              invFun := fun β ↦
                TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
                  ((G ⋙ L₂ ⋙ L₄).leftUnitor.inv ≫
                    whiskerRight
                        (Adjunction.mk'
                            {
                              homEquiv := fun x x_1 ↦
                                (adj₃.homEquiv (L₁.obj x) x_1).trans (adj₁.homEquiv x (R₃.obj x_1)),
                              unit :=
                                adj₁.unit ≫
                                  whiskerRight
                                      (L₁.rightUnitor.inv ≫ L₁.whiskerLeft adj₃.unit ≫ (L₁.associator L₃ R₃).inv) R₁ ≫
                                    ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                              counit :=
                                ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                                  whiskerRight
                                      ((R₃.associator R₁ L₁).hom ≫ R₃.whiskerLeft adj₁.counit ≫ R₃.rightUnitor.hom) L₃ ≫
                                    adj₃.counit,
                              homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).unit
                        (G ⋙ L₂ ⋙ L₄) ≫
                      (((L₁ ⋙ L₃) ⋙ R₃ ⋙ R₁).associator G (L₂ ⋙ L₄)).inv ≫
                        whiskerRight ((L₁ ⋙ L₃).associator (R₃ ⋙ R₁) G).hom (L₂ ⋙ L₄) ≫
                          whiskerRight ((L₁ ⋙ L₃).whiskerLeft β.natTrans) (L₂ ⋙ L₄) ≫
                            whiskerRight ((L₁ ⋙ L₃).associator K (R₄ ⋙ R₂)).inv (L₂ ⋙ L₄) ≫
                              (((L₁ ⋙ L₃) ⋙ K).associator (R₄ ⋙ R₂) (L₂ ⋙ L₄)).hom ≫
                                ((L₁ ⋙ L₃) ⋙ K).whiskerLeft
                                    (Adjunction.mk'
                                        {
                                          homEquiv := fun x x_1 ↦
                                            (adj₄.homEquiv (L₂.obj x) x_1).trans (adj₂.homEquiv x (R₄.obj x_1)),
                                          unit :=
                                            adj₂.unit ≫
                                              whiskerRight
                                                  (L₂.rightUnitor.inv ≫
                                                    L₂.whiskerLeft adj₄.unit ≫ (L₂.associator L₄ R₄).inv)
                                                  R₂ ≫
                                                ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                                          counit :=
                                            ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                                              whiskerRight
                                                  ((R₄.associator R₂ L₂).hom ≫
                                                    R₄.whiskerLeft adj₂.counit ≫ R₄.rightUnitor.hom)
                                                  L₄ ≫
                                                adj₄.counit,
                                          homEquiv_unit := ⋯, homEquiv_counit := ⋯ }).counit ≫
                                  ((L₁ ⋙ L₃) ⋙ K).rightUnitor.hom),
              left_inv := ⋯, right_inv := ⋯ }
            (TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
              ((G.associator L₂ L₄).inv ≫
                whiskerRight α.natTrans L₄ ≫
                  (L₁.associator H L₄).hom ≫ L₁.whiskerLeft β.natTrans ≫ (L₁.associator L₃ K).inv))).natTrans.app
      c =
    (TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
            ((R₃.associator R₁ G).hom ≫
              R₃.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 ≫
                (R₃.associator H R₂).inv ≫
                  whiskerRight
                      ({
                            toFun := fun α ↦
                              TwoSquare.mk R₃ K H R₄
                                ((R₃ ⋙ H).rightUnitor.inv ≫
                                  (R₃ ⋙ H).whiskerLeft adj₄.unit ≫
                                    (R₃.associator H (L₄ ⋙ R₄)).hom ≫
                                      R₃.whiskerLeft (H.associator L₄ R₄).inv ≫
                                        R₃.whiskerLeft (whiskerRight α.natTrans R₄) ≫
                                          R₃.whiskerLeft (L₃.associator K R₄).hom ≫
                                            (R₃.associator L₃ (K ⋙ R₄)).inv ≫
                                              whiskerRight adj₃.counit (K ⋙ R₄) ≫ (K ⋙ R₄).leftUnitor.hom),
                            invFun := fun β ↦
                              TwoSquare.mk H L₃ L₄ K
                                ((H ⋙ L₄).leftUnitor.inv ≫
                                  whiskerRight adj₃.unit (H ⋙ L₄) ≫
                                    ((L₃ ⋙ R₃).associator H L₄).inv ≫
                                      whiskerRight (L₃.associator R₃ H).hom L₄ ≫
                                        whiskerRight (L₃.whiskerLeft β.natTrans) L₄ ≫
                                          whiskerRight (L₃.associator K R₄).inv L₄ ≫
                                            ((L₃ ⋙ K).associator R₄ L₄).hom ≫
                                              (L₃ ⋙ K).whiskerLeft adj₄.counit ≫ (L₃ ⋙ K).rightUnitor.hom),
                            left_inv := ⋯, right_inv := ⋯ }
                          β).natTrans
                      R₂ ≫
                    (K.associator R₄ R₂).hom)).natTrans.app
      c

Tactic:
simp only [comp_obj, whiskerRight_comp, assoc, mk'_unit, whiskerLeft_comp, mk'_counit,
    whiskerRight_twice, Iso.inv_hom_id_assoc, Equiv.coe_fn_mk, comp_app, id_obj,
    rightUnitor_inv_app, Functor.whiskerLeft_app, Functor.whiskerRight_app, map_id,
    associator_inv_app, associator_hom_app, Functor.comp_map, rightUnitor_hom_app,
    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 ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (α.natTrans.app (R₁.obj (R₃.obj c))) ≫
        R₂.map (H.map (adj₁.counit.app (R₃.obj c))) ≫
          R₂.map (adj₄.unit.app (H.obj (R₃.obj c))) ≫
            R₂.map (R₄.map (β.natTrans.app (R₃.obj c))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))