-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem comp_rightAdjointMate {X Y Z : C} [HasRightDual X] [HasRightDual Y] [HasRightDual Z]
    {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g)ᘁ = gᘁ ≫ fᘁ

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
rw [tensorHom_def']

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ Y ◁ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g ▷ Xᘁ =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Proof state:
case e_a.e_a.e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) =
    (ρ_ Zᘁ).inv ≫
      Zᘁ ◁ η_ Y Yᘁ ≫ Zᘁ ◁ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom)

Tactic:
simp only [← MonoidalCategory.whiskerLeft_comp]

Result:
case e_a.e_a.e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ρ_ Zᘁ).inv ≫ Zᘁ ◁ (η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ) =
    (ρ_ Zᘁ).inv ≫
      Zᘁ ◁ (η_ Y Yᘁ ≫ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom))

Proof state:
case e_a.e_a.e_a.e_a.e_f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ =
    η_ Y Yᘁ ≫ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom)

Tactic:
symm

Result:
case e_a.e_a.e_a.e_a.e_f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) =
    η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ

Proof state:
case e_a.e_a.e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ) ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) =
    ((ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ Y Yᘁ) ≫
      Zᘁ ◁ (g ⊗ (((((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ) ≫ Yᘁ ◁ f ▷ Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv) ≫ ε_ Y Yᘁ ▷ Xᘁ) ≫ (λ_ Xᘁ).hom)

Tactic:
simp only [Category.assoc]

Result:
case e_a.e_a.e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) =
    (ρ_ Zᘁ).inv ≫
      Zᘁ ◁ η_ Y Yᘁ ≫ Zᘁ ◁ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g)ᘁ = (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ Y Yᘁ ≫ Zᘁ ◁ (g ⊗ fᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ ε_ Z Zᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom

Tactic:
simp only [rightAdjointMate, comp_whiskerRight]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ ε_ Z Zᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom =
    (ρ_ Zᘁ).inv ≫
      Zᘁ ◁ η_ Y Yᘁ ≫
        Zᘁ ◁ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫
          (α_ Zᘁ Z Xᘁ).inv ≫ ε_ Z Zᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ Y ◁ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g ▷ Xᘁ =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
monoidal

Result:
no goals