Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: 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₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (((𝟭 A).associator G L₃).hom ≫
          (𝟭 A).whiskerLeft β.natTrans ≫
            ((𝟭 A).associator L₂ H).inv ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).inv ≫
        whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
          ((𝟭 B).associator R₂ G).hom ≫
            (𝟭 B).whiskerLeft ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).inv)
vcompb :
  ((mateEquiv adj₁ adj₃)
          (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
            (((𝟭 A).associator G L₃).hom ≫
              (𝟭 A).whiskerLeft β.natTrans ≫
                ((𝟭 A).associator L₂ H).inv ≫
                  whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫
                    (L₁.associator (𝟭 B) H).hom))).app
      b =
    (TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
          ((R₁.associator (𝟭 A) G).inv ≫
            whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
              ((𝟭 B).associator R₂ G).hom ≫
                (𝟭 B).whiskerLeft ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).inv)).app
      b
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b

Tactic:
simp only [comp_obj, id_obj, whiskerRight_comp, assoc, mateEquiv_apply, whiskerLeft_comp,
    whiskerLeft_twice, comp_app, Functor.whiskerLeft_app, Functor.whiskerRight_app,
    associator_hom_app, map_id, associator_inv_app, leftUnitor_hom_app, rightUnitor_inv_app,
    Functor.comp_map, Functor.id_map, id_comp, whiskerRight_twice, Iso.inv_hom_id_assoc,
    comp_id] at vcompb

Goal state after:
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₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (((𝟭 A).associator G L₃).hom ≫
          (𝟭 A).whiskerLeft β.natTrans ≫
            ((𝟭 A).associator L₂ H).inv ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).inv ≫
        whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
          ((𝟭 B).associator R₂ G).hom ≫
            (𝟭 B).whiskerLeft ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).inv)
vcompb :
  adj₃.unit.app (G.obj (R₁.obj b)) ≫
      R₃.map (β.natTrans.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) =
    G.map (adj₂.unit.app (R₁.obj b)) ≫
      G.map (R₂.map (α.app (R₁.obj b))) ≫
        G.map (R₂.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))
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b