C : Type u₁
inst✝⁴ : Category 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
C : Type u₁
inst✝⁴ : Category 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)ᘁ = gᘁ ≫ fᘁ
rw [rightAdjointMate_comp]
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 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
C : Type u₁
inst✝⁴ : Category 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
simp only [rightAdjointMate, comp_tensor_id, Iso.cancel_iso_inv_left, id_tensor_comp,
  Category.assoc]
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 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 =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 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
symm
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)) ≫
        (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 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 =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
iterate 5
  trans
  rw [← Category.id_comp g, tensor_comp]
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)) ≫
        (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
rw [← Category.assoc]
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
symm
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ)) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
iterate 2
  trans
  rw [← Category.assoc]
case w
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) =
    (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
        (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ)) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
apply eq_whisker
case w
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 Zᘁ ⊗ (η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ)) ≫ (g ⊗ 𝟙 Xᘁ) =
    𝟙 Zᘁ ⊗
      η_ Y Yᘁ ≫
        (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)
case w
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) =
    (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
        (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))
repeat'
  rw [← @id_tensor_comp C]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ ≫
      (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
        (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)
case w
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 Zᘁ ⊗ (η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ)) ≫ (g ⊗ 𝟙 Xᘁ) =
    𝟙 Zᘁ ⊗
      η_ Y Yᘁ ≫
        (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)
congr 1
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (η_ Y Yᘁ ⊗ η_ X Xᘁ) ≫
        ((𝟙 Y ⊗ 𝟙 Yᘁ) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ ≫
      (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
        (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)
rw [← id_tensor_comp_tensor_id (λ_ (Xᘁ)).hom g, id_tensor_rightUnitor_inv, Category.assoc,
  Category.assoc, rightUnitor_inv_naturality_assoc, ← associator_naturality_assoc, tensor_id,
  tensor_id_comp_id_tensor_assoc, ← associator_naturality_assoc]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      ((((((𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫ (η_ Y Yᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv)) ≫
            (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ)) ≫
          (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫
        (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (η_ Y Yᘁ ⊗ η_ X Xᘁ) ≫
        ((𝟙 Y ⊗ 𝟙 Yᘁ) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
slice_rhs 2 3 =>
  rw [← tensor_comp, tensor_id, Category.comp_id, ← Category.id_comp (η_ Y (Yᘁ)), tensor_comp]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      ((((((𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫ (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫ (η_ Y Yᘁ ⊗ 𝟙 Y ⊗ 𝟙 Xᘁ)) ≫ (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom) ≫
              (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv)) ≫
            (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ)) ≫
          (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫
        (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      ((((((𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫ (η_ Y Yᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv)) ≫
            (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ)) ≫
          (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫
        (g ⊗ 𝟙 Xᘁ)
rw [← id_tensor_comp_tensor_id _ (η_ Y (Yᘁ)), ← tensor_id]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (η_ Y Yᘁ ⊗ 𝟙 Y ⊗ 𝟙 Xᘁ) ≫
            (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom ≫
              (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      ((((((𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫ (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫ (η_ Y Yᘁ ⊗ 𝟙 Y ⊗ 𝟙 Xᘁ)) ≫ (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom) ≫
              (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv)) ≫
            (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ)) ≫
          (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫
        (g ⊗ 𝟙 Xᘁ)
repeat' rw [@Category.assoc C]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (α_ (𝟙_ C) Y Xᘁ).inv ≫
            ((η_ Y Yᘁ ⊗ 𝟙 Y) ⊗ 𝟙 Xᘁ) ≫
              ((α_ Y Yᘁ Y).hom ⊗ 𝟙 Xᘁ) ≫
                ((𝟙 Y ⊗ ε_ Y Yᘁ) ⊗ 𝟙 Xᘁ) ≫ (α_ Y (𝟙_ C) Xᘁ).hom ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (η_ Y Yᘁ ⊗ 𝟙 Y ⊗ 𝟙 Xᘁ) ≫
            (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom ≫
              (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
rw [pentagon_hom_inv_assoc, ← associator_naturality_assoc, associator_inv_naturality_assoc]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (α_ (𝟙_ C) Y Xᘁ).inv ≫
            (((((λ_ Y).hom ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ)) ≫ (α_ Y (𝟙_ C) Xᘁ).hom) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (α_ (𝟙_ C) Y Xᘁ).inv ≫
            ((η_ Y Yᘁ ⊗ 𝟙 Y) ⊗ 𝟙 Xᘁ) ≫
              ((α_ Y Yᘁ Y).hom ⊗ 𝟙 Xᘁ) ≫
                ((𝟙 Y ⊗ ε_ Y Yᘁ) ⊗ 𝟙 Xᘁ) ≫ (α_ Y (𝟙_ C) Xᘁ).hom ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
slice_rhs 5 7 => rw [← comp_tensor_id, ← comp_tensor_id, evaluation_coevaluation, comp_tensor_id]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((𝟙 (𝟙_ C) ⊗ f) ⊗ 𝟙 Xᘁ) ≫
            (((((λ_ Y).hom ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ)) ≫ (α_ Y (𝟙_ C) Xᘁ).hom) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (α_ (𝟙_ C) Y Xᘁ).inv ≫
            (((((λ_ Y).hom ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ)) ≫ (α_ Y (𝟙_ C) Xᘁ).hom) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫ (g ⊗ 𝟙 Xᘁ)
rw [associator_inv_naturality_assoc]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((((((λ_ X).hom ⊗ 𝟙 Xᘁ) ≫ (f ⊗ 𝟙 Xᘁ)) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ)) ≫ (α_ Y (𝟙_ C) Xᘁ).hom) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫
            (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((𝟙 (𝟙_ C) ⊗ f) ⊗ 𝟙 Xᘁ) ≫
            (((((λ_ Y).hom ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ)) ≫ (α_ Y (𝟙_ C) Xᘁ).hom) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫ (g ⊗ 𝟙 Xᘁ)
slice_rhs 4 5 => rw [← tensor_comp, leftUnitor_naturality, tensor_comp]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((λ_ X).hom ⊗ 𝟙 Xᘁ) ≫
            (f ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ) ≫ (α_ Y (𝟙_ C) Xᘁ).hom ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((((((λ_ X).hom ⊗ 𝟙 Xᘁ) ≫ (f ⊗ 𝟙 Xᘁ)) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ)) ≫ (α_ Y (𝟙_ C) Xᘁ).hom) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom)) ≫
            (g ⊗ 𝟙 Xᘁ)
repeat' rw [@Category.assoc C]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    ((ρ_ tensorUnit').inv ≫ (ρ_ (𝟙_ C)).hom) ≫
      η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).inv) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((λ_ X).hom ⊗ 𝟙 Xᘁ) ≫
            (f ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ) ≫ (α_ Y (𝟙_ C) Xᘁ).hom ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
rw [triangle_assoc_comp_right_inv_assoc, ← leftUnitor_tensor_assoc, leftUnitor_naturality_assoc,
  unitors_equal, ← Category.assoc, ← Category.assoc]
no goals
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    ((ρ_ tensorUnit').inv ≫ (ρ_ (𝟙_ C)).hom) ≫
      η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).inv) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
simp
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (g ⊗ (ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom)) ≫
        (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ?m.258965

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ?m.258965 =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Zᘁ ⊗ tensorUnit' ⟶ Xᘁ
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (g ⊗ (ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom)) ≫
        (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
trans
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)) ≫
        (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
      (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (g ⊗ (ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom)) ≫
        (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ?m.258965

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ?m.258965 =
    (𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Zᘁ ⊗ tensorUnit' ⟶ Xᘁ
rw [← Category.id_comp g, tensor_comp]
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ?m.259767

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ?m.259767 =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Zᘁ ⊗ tensorUnit' ⟶ Xᘁ
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
trans
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ)) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((𝟙 Zᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Zᘁ ⊗ f ⊗ 𝟙 Xᘁ)) ≫ (𝟙 Zᘁ ⊗ g ⊗ 𝟙 Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom =
    ?m.259767

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ?m.259767 =
    ((𝟙 Zᘁ ⊗ η_ Y Yᘁ) ≫
        (𝟙 Zᘁ ⊗
          (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
              (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom))) ≫
      (α_ Zᘁ Z Xᘁ).inv ≫ (ε_ Z Zᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom

C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Zᘁ ⊗ tensorUnit' ⟶ Xᘁ
rw [← Category.assoc]
case w
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 Zᘁ ⊗ (η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ)) ≫ (g ⊗ 𝟙 Xᘁ) =
    𝟙 Zᘁ ⊗
      η_ Y Yᘁ ≫
        (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)
case w
C : Type u₁
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 Zᘁ ⊗ (η_ X Xᘁ ≫ (f ⊗ 𝟙 Xᘁ)) ≫ (g ⊗ 𝟙 Xᘁ) =
    𝟙 Zᘁ ⊗
      η_ Y Yᘁ ≫
        (𝟙 Y ⊗ (ρ_ Yᘁ).inv) ≫
          (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫
            (𝟙 Y ⊗ 𝟙 Yᘁ ⊗ f ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (g ⊗ (λ_ Xᘁ).hom)
rw [← @id_tensor_comp C]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (η_ Y Yᘁ ⊗ 𝟙 Y ⊗ 𝟙 Xᘁ) ≫
            (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom ≫
              (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (𝟙 (𝟙_ C) ⊗ f ⊗ 𝟙 Xᘁ) ≫
          (η_ Y Yᘁ ⊗ 𝟙 Y ⊗ 𝟙 Xᘁ) ≫
            (α_ Y Yᘁ (Y ⊗ Xᘁ)).hom ≫
              (𝟙 Y ⊗ (α_ Yᘁ Y Xᘁ).inv) ≫ (𝟙 Y ⊗ ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
rw [@Category.assoc C]
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((λ_ X).hom ⊗ 𝟙 Xᘁ) ≫
            (f ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ) ≫ (α_ Y (𝟙_ C) Xᘁ).hom ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
case w.e_a
C : Type u₁
inst✝⁴ : Category 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ᘁ) =
    (ρ_ tensorUnit').inv ≫
      (𝟙 (𝟙_ C) ⊗ η_ X Xᘁ) ≫
        (α_ (𝟙_ C) X Xᘁ).inv ≫
          ((λ_ X).hom ⊗ 𝟙 Xᘁ) ≫
            (f ⊗ 𝟙 Xᘁ) ≫ ((ρ_ Y).inv ⊗ 𝟙 Xᘁ) ≫ (α_ Y (𝟙_ C) Xᘁ).hom ≫ (𝟙 Y ⊗ (λ_ Xᘁ).hom) ≫ (g ⊗ 𝟙 Xᘁ)
rw [@Category.assoc C]