Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
d : D
⊢ (𝟙 (R₁.obj d) ≫
        (𝟙 (R₁.obj d) ≫
            adj₂.unit.app (R₁.obj d) ≫
              𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                  R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫
                      𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d) ≫ 𝟙 (R₂.obj d)) ≫
          𝟙 (R₂.obj d)) ≫
      𝟙 (R₂.obj d) ≫
        (𝟙 (R₂.obj d) ≫
            adj₃.unit.app (R₂.obj d) ≫
              𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                  R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫
                    𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫
                      𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
          𝟙 (R₃.obj d) =
    𝟙 (R₁.obj d) ≫
      (𝟙 (R₁.obj d) ≫
          adj₃.unit.app (R₁.obj d) ≫
            𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
              𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
                R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                  𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
        𝟙 (R₃.obj d)

Tactic:
have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃
    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)
    (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
d : D
vcomp :
  (mateEquiv adj₁ adj₃) ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) =
    (mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ᵥ
      (mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
⊢ (𝟙 (R₁.obj d) ≫
        (𝟙 (R₁.obj d) ≫
            adj₂.unit.app (R₁.obj d) ≫
              𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                  R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫
                      𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d) ≫ 𝟙 (R₂.obj d)) ≫
          𝟙 (R₂.obj d)) ≫
      𝟙 (R₂.obj d) ≫
        (𝟙 (R₂.obj d) ≫
            adj₃.unit.app (R₂.obj d) ≫
              𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                  R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫
                    𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫
                      𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
          𝟙 (R₃.obj d) =
    𝟙 (R₁.obj d) ≫
      (𝟙 (R₁.obj d) ≫
          adj₃.unit.app (R₁.obj d) ≫
            𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
              𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
                R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                  𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
        𝟙 (R₃.obj d)