awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
⊢ Eq.{v + 1} (α := X.left ⟶ X.left)
    (CategoryStruct.comp (Y :=
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X.left (tensorUnit.{v, u} C (𝒞 := inst)))
          (Iso.inv (ρ_ X.left))
          (pushout.inr
            (NatTrans.app (map (curriedTensor C) X.hom)
              (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
            (map (obj (curriedTensor C) X.left)
              (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))) :
        X.left ⟶ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
      (pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
          (Iso.hom (ρ_ X.left)) ⋯ :
        pushout (X :=
            obj.{v, v, u, u} (obj (curriedTensor C) X.left)
              (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
            (NatTrans.app (map (curriedTensor C) X.hom)
              (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
            (map (obj (curriedTensor C) X.left)
              (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))) ⟶
          X.left))
    (𝟙 X.left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
X : Arrow.{v, u} C
T : C
t : IsTerminal.{v, u} T
W : C
this_1 : IsIso (X := X.right ⟹ T) (Y := X.left ⟹ T) (NatTrans.app (MonoidalClosed.pre X.hom) T)
this :
  IsPullback (Y := X.right ⟹ T) (𝟙 (X.left ⟹ W))
    (IsTerminal.from (IsTerminal.isTerminalObj (ihom X.right) T t) (X.left ⟹ W)) (map (ihom X.left) (t.from W))
    (NatTrans.app (MonoidalClosed.pre X.hom) T)
⊢ CategoryStruct.comp (Y :=
      pullback (X := X.left ⟹ W) (Y := X.right ⟹ T) (map (ihom X.left) (t.from W))
        (NatTrans.app (MonoidalClosed.pre X.hom) T))
      ((Iso.hom
            (Iso.refl
              (obj.{v, v, u, u} (obj MonoidalClosed.internalHom (Opposite.op (Opposite.unop (Opposite.op X)).right))
                (Arrow.mk (t.from W)).left)) ≫
          NatTrans.app (MonoidalClosed.pre X.hom) W) ≫
        Iso.hom this.isoPullback)
      (pullback.fst (map (ihom X.left) (t.from W)) (NatTrans.app (MonoidalClosed.pre X.hom) T)) =
    CategoryStruct.comp (Y :=
      pullback (X := X.left ⟹ W) (Y := X.right ⟹ T) (map (ihom X.left) (t.from W))
        (NatTrans.app (MonoidalClosed.pre X.hom) T))
      (PullbackObjObj.π
          (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom (Opposite.unop (Opposite.op X)).hom
            (Arrow.mk (t.from W)).hom) :
        obj.{v, v, u, u} (obj MonoidalClosed.internalHom (Opposite.op (Opposite.unop (Opposite.op X)).right))
            (Arrow.mk (t.from W)).left ⟶
          PullbackObjObj.pt (G := MonoidalClosed.internalHom)
            (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom (Opposite.unop (Opposite.op X)).hom
              (Arrow.mk (t.from W)).hom))
      (pullback.fst (map (ihom X.left) (t.from W)) (NatTrans.app (MonoidalClosed.pre X.hom) T))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : BraidedCategory.{v, u} C
X : Arrow.{v, u} C
I : C
i : IsInitial.{v, u} I
W : C
this_1 : IsIso (X := I ⟹ X.left) (map (ihom I) X.hom)
this :
  IsPullback (X := I ⟹ X.left)
    (IsTerminal.from (IsTerminal.ofIso isTerminalTensorUnit (Iso.symm (powZero i))) (W ⟹ X.right)) (𝟙 (W ⟹ X.right))
    (map (ihom I) X.hom) (NatTrans.app (MonoidalClosed.pre (i.to W)) X.right)
⊢ CategoryStruct.comp (Y :=
      pullback (X := I ⟹ X.left) (Y := W ⟹ X.right) (map (ihom I) X.hom)
        (NatTrans.app (MonoidalClosed.pre (i.to W)) X.right))
      ((Iso.hom
            (Iso.refl
              (obj.{v, v, u, u}
                (obj MonoidalClosed.internalHom (Opposite.op (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).right))
                X.left)) ≫
          map (ihom W) X.hom) ≫
        Iso.hom this.isoPullback)
      (pullback.snd (map (ihom I) X.hom) (NatTrans.app (MonoidalClosed.pre (i.to W)) X.right)) =
    CategoryStruct.comp (Y :=
      pullback (X := I ⟹ X.left) (Y := W ⟹ X.right) (map (ihom I) X.hom)
        (NatTrans.app (MonoidalClosed.pre (i.to W)) X.right))
      (PullbackObjObj.π
          (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).hom
            X.hom) :
        obj.{v, v, u, u}
            (obj MonoidalClosed.internalHom (Opposite.op (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).right))
            X.left ⟶
          PullbackObjObj.pt (G := MonoidalClosed.internalHom)
            (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom
              (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).hom X.hom))
      (pullback.snd (map (ihom I) X.hom) (NatTrans.app (MonoidalClosed.pre (i.to W)) X.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ η_ X Y ≫ Iso.inv (α_ Y X Y) ≫ ε_ X Y ▷ Y) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))

Tactic:
coevaluation_evaluation'

Premises used: CategoryTheory.ExactPairing.coevaluation_evaluation', CategoryTheory.ExactPairing.evaluation, CategoryTheory.ExactPairing.coevaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ ε_ X Y) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
evaluation_coevaluation'

Premises used: CategoryTheory.ExactPairing.evaluation_coevaluation', CategoryTheory.ExactPairing.evaluation, CategoryTheory.ExactPairing.coevaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ η_ X Y ≫ Iso.inv (α_ Y X Y) ≫ ε_ X Y ▷ Y) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))

Tactic:
coevaluation_evaluation X Y

Premises used: CategoryTheory.ExactPairing.coevaluation_evaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
h :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y) (Y ◁ η_ X Y ≫ Iso.inv (α_ Y X Y) ≫ ε_ X Y ▷ Y)
h₁ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Iso.hom ⊗𝟙 ) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y) (Iso.hom ⊗𝟙 )

Tactic:
convert! coevaluation_evaluation X Y

Premises used: CategoryTheory.ExactPairing.coevaluation_evaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y) (Y ◁ η_ X Y ≫ Iso.inv (α_ Y X Y) ≫ ε_ X Y ▷ Y)

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Iso.hom ⊗𝟙 ) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ ε_ X Y) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
evaluation_coevaluation X Y

Premises used: CategoryTheory.ExactPairing.evaluation_coevaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
h :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y) (η_ X Y ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ ε_ X Y)
h₁ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom ⊗𝟙 ) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y) (Iso.hom ⊗𝟙 )

Tactic:
convert! evaluation_coevaluation X Y

Premises used: CategoryTheory.ExactPairing.evaluation_coevaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y) (η_ X Y ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ ε_ X Y)

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : ExactPairing X Y
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom ⊗𝟙 ) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.inv
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) =
    Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ Iso.inv (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
      Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
inst_2 : HasRightDual.{v₁, u₁} X
⊢ @leftDual.{v₁, u₁} _ inst inst_1 (@rightDual.{v₁, u₁} _ inst inst_1 X _) _ = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
inst_2 : HasLeftDual.{v₁, u₁} X
⊢ @rightDual.{v₁, u₁} _ inst inst_1 (@leftDual.{v₁, u₁} _ inst inst_1 X _) _ = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
inst_2 : HasRightDual.{v₁, u₁} X
⊢ 𝟙 Xᘁ = 𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 X _)

Tactic:
simp [rightAdjointMate]

Premises used: CategoryTheory.rightAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
inst_2 : HasLeftDual.{v₁, u₁} X
⊢ (ᘁ𝟙 X) = 𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 X _)

Tactic:
simp [leftAdjointMate]

Premises used: CategoryTheory.leftAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
f : X ⟶ Y
g : @rightDual.{v₁, u₁} _ inst inst_1 X _ ⟶ Z
dsimp :
  CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
          @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
            Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _)) ≫
              ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
                Iso.hom (λ_ (@rightDual.{v₁, u₁} _ inst inst_1 X _))) ≫
      g =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          ((ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ g) ⊗≫
            𝟙 Z)))
⊢ fᘁ ≫ g =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          ((ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ g) ⊗≫
            𝟙 Z)))

Tactic:
dsimp only [rightAdjointMate]

Premises used: CategoryTheory.rightAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
f : X ⟶ Y
g : @rightDual.{v₁, u₁} _ inst inst_1 X _ ⟶ Z
⊢ CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
          @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
            Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _)) ≫
              ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
                Iso.hom (λ_ (@rightDual.{v₁, u₁} _ inst inst_1 X _))) ≫
      g =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          ((ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ g) ⊗≫
            𝟙 Z)))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
f : X ⟶ Y
g : @rightDual.{v₁, u₁} _ inst inst_1 X _ ⟶ Z
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          ((tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y ◁ g ≫
              ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Z) ⊗≫
            𝟙 Z))) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
      (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
        @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ Y ◁ g) ≫
          Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y Z) ≫
            ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Z ≫ Iso.hom (λ_ Z))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
f : X ⟶ Y
g : @leftDual.{v₁, u₁} _ inst inst_1 X _ ⟶ Z
dsimp :
  CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
        (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
        (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
            Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
              @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫
                Iso.hom (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _))) ≫
      g =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
        (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
          ((@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫
              g ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗≫
            𝟙 Z)))
⊢ (ᘁf) ≫ g =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
        (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
          ((@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫
              g ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗≫
            𝟙 Z)))

Tactic:
dsimp only [leftAdjointMate]

Premises used: CategoryTheory.leftAdjointMate