-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem comp_leftAdjointMate {X Y Z : C} [HasLeftDual X] [HasLeftDual Y] [HasLeftDual 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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (η_ (ᘁX) X ▷ 𝟙_ C ≫ (ᘁX ⊗ X) ◁ η_ (ᘁY) Y) ⊗≫ ᘁX ◁ f ▷ ᘁY ▷ Y ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g

Tactic:
monoidal

Result:
no goals

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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g =
    η_ (ᘁY) Y ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ g)

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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁY) Y ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ g) =
    η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ᘁf ≫ g) = (ᘁg) ≫ ᘁf

Tactic:
rw [leftAdjointMate_comp]

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

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

Tactic:
monoidal

Result:
no goals

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

Tactic:
congr 3

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

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

Tactic:
monoidal

Result:
no goals

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

Tactic:
monoidal

Result:
no goals

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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ) ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ =
    ((λ_ ᘁZ).inv ≫ η_ (ᘁY) Y ▷ ᘁZ) ≫
      ((((((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY) ≫ (ᘁX ◁ f) ▷ ᘁY) ≫ (α_ (ᘁX) Y ᘁY).hom) ≫ ᘁX ◁ ε_ (ᘁY) Y) ≫ (ρ_ ᘁX).hom ⊗ g) ▷
        ᘁZ

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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ =
    (λ_ ᘁZ).inv ≫
      η_ (ᘁY) Y ▷ ᘁZ ≫
        ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ g) ▷ ᘁZ

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

Tactic:
rw [whisker_exchange]

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

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

Tactic:
simp only [← Category.assoc]

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

Tactic:
calc
  _ = 𝟙 _ ⊗≫ ((𝟙_ C) ◁ η_ (ᘁY) Y ≫ η_ (ᘁX) X ▷ ((ᘁY) ⊗ Y)) ⊗≫ (ᘁX) ◁ f ▷ (ᘁY) ▷ Y ⊗≫
      (ᘁX) ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ (ᘁX) ◁ g := by
    rw [tensorHom_def]; monoidal
  _ = η_ (ᘁX) X ⊗≫ (((ᘁX) ⊗ X) ◁ η_ (ᘁY) Y ≫ ((ᘁX) ◁ f) ▷ ((ᘁY) ⊗ Y)) ⊗≫
      (ᘁX) ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ (ᘁX) ◁ g := by
    rw [whisker_exchange]; monoidal
  _ = η_ (ᘁX) X ⊗≫ ((ᘁX) ◁ f) ⊗≫ (ᘁX) ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ (ᘁX) ◁ g := by
    rw [whisker_exchange]; monoidal
  _ = η_ (ᘁX) X ≫ (ᘁX) ◁ f ≫ (ᘁX) ◁ g := by
    rw [coevaluation_evaluation'']; monoidal

Result:
no goals