-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem mateEquiv_vcomp (α : TwoSquare G₁ L₁ L₂ H₁) (β : TwoSquare G₂ L₂ L₃ H₂) :
    (mateEquiv adj₁ adj₃) (α ≫ₕ β) = (mateEquiv adj₁ adj₂ α) ≫ᵥ (mateEquiv adj₂ adj₃ β)

Proof state:
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₂
⊢ (mateEquiv adj₁ adj₃) (α ≫ₕ β) = (mateEquiv adj₁ adj₂) α ≫ᵥ (mateEquiv adj₂ adj₃) β

Tactic:
unfold hComp vComp mateEquiv

Result:
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₂
⊢ {
        toFun := fun α =>
          TwoSquare.mk R₁ (H₁ ⋙ H₂) (G₁ ⋙ G₂) R₃
            (whiskerLeft (R₁ ⋙ G₁ ⋙ G₂) adj₃.unit ≫
              whiskerRight (whiskerLeft R₁ α.natTrans) R₃ ≫ whiskerRight adj₁.counit ((H₁ ⋙ H₂) ⋙ R₃)),
        invFun := fun β =>
          TwoSquare.mk (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)
            (whiskerRight adj₁.unit ((G₁ ⋙ G₂) ⋙ L₃) ≫
              whiskerRight (whiskerLeft L₁ β.natTrans) L₃ ≫ whiskerLeft (L₁ ⋙ H₁ ⋙ H₂) adj₃.counit),
        left_inv := ⋯, right_inv := ⋯ }
      (TwoSquare.mk (G₁ ⋙ G₂) L₁ L₃ (H₁ ⋙ H₂)
        ((G₁.associator G₂ L₃).hom ≫
          whiskerLeft G₁ β.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₂).hom ≫
        whiskerRight
            ({
                  toFun := fun α =>
                    TwoSquare.mk R₁ H₁ G₁ R₂
                      (whiskerLeft (R₁ ⋙ G₁) adj₂.unit ≫
                        whiskerRight (whiskerLeft R₁ α.natTrans) R₂ ≫ whiskerRight adj₁.counit (H₁ ⋙ R₂)),
                  invFun := fun β =>
                    TwoSquare.mk G₁ L₁ L₂ H₁
                      (whiskerRight adj₁.unit (G₁ ⋙ L₂) ≫
                        whiskerRight (whiskerLeft L₁ β.natTrans) L₂ ≫ whiskerLeft (L₁ ⋙ H₁) adj₂.counit),
                  left_inv := ⋯, right_inv := ⋯ }
                α).natTrans
            G₂ ≫
          (H₁.associator R₂ G₂).inv ≫
            whiskerLeft H₁
                ({
                      toFun := fun α =>
                        TwoSquare.mk R₂ H₂ G₂ R₃
                          (whiskerLeft (R₂ ⋙ G₂) adj₃.unit ≫
                            whiskerRight (whiskerLeft R₂ α.natTrans) R₃ ≫ whiskerRight adj₂.counit (H₂ ⋙ R₃)),
                      invFun := fun β =>
                        TwoSquare.mk G₂ L₂ L₃ H₂
                          (whiskerRight adj₂.unit (G₂ ⋙ L₃) ≫
                            whiskerRight (whiskerLeft L₂ β.natTrans) L₃ ≫ whiskerLeft (L₂ ⋙ H₂) adj₃.counit),
                      left_inv := ⋯, right_inv := ⋯ }
                    β).natTrans ≫
              (H₁.associator H₂ R₃).hom)

Proof state:
case h
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))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
          R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
            R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
slice_rhs 4 5 =>
  rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
  rw [adj₂.counit.naturality]

Result:
case h
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))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
          R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))) ≫ (𝟭 D).map (H₁.map (adj₁.counit.app b))))

Proof state:
case h
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))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
          R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))))) ≫
            R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))

Tactic:
slice_rhs 3 4 =>
  rw [← R₃.map_comp, ← H₂.map_comp, left_triangle_components]

Result:
case h
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))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        (R₃.map (H₂.map (𝟙 (L₂.obj (G₁.obj (R₁.obj b))))) ≫ R₃.map (H₂.map (α.natTrans.app (R₁.obj b)))) ≫
          R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))