awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶ X.left
have refine_1 : obj.{v, v, u, u} (obj (curriedTensor C) X.right)
    (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ⟶
  X.left
Tactic: refine pushout.desc ?_ (ρ_ X.left).hom ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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
refine_1 :
  obj.{v, v, u, u} (obj (curriedTensor C) X.right)
      (Arrow.left.{v, u} (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 ⟶ X.left
have refine_1₁ : Eq (α :=
  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))))) ⟶
    X.left)
  (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))))) ≫
    IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
  (map (obj (curriedTensor C) X.left)
      (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ≫
    Iso.hom (ρ_ X.left))
Tactic: refine pushout.desc ?_ (ρ_ X.left).hom ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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) (Iso.hom ⊗𝟙 )
have 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)
Tactic: convert! coevaluation_evaluation X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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)
⊢ 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 ⊗𝟙 )
have 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))
Tactic: convert! coevaluation_evaluation X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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) (Iso.hom ⊗𝟙 )
have 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)
Tactic: convert! evaluation_coevaluation X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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)
⊢ 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 ⊗𝟙 )
have 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))
Tactic: convert! evaluation_coevaluation X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
⊢ 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)))
have 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)))
Tactic: dsimp only [rightAdjointMate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
⊢ (ᘁ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)))
have 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)))
Tactic: dsimp only [leftAdjointMate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
⊢ 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))) =
    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 _ ≫
        (g ⊗ₘ f) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
          Iso.hom (α_ Z Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
            Z ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫ Iso.hom (ρ_ Z))
have rw : 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 _)
        ((g ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ≫
            Z ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y) ⊗≫
          𝟙 Z))) =
  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 ≫ g ▷ Y) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
        Iso.hom (α_ Z Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
          Z ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫ Iso.hom (ρ_ Z))
Tactic: rw [whisker_exchange, tensorHom_def']
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
inst_4 : HasRightDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := @rightDual.{v₁, u₁} _ inst inst_1 Z _ ⟶ @rightDual.{v₁, u₁} _ inst inst_1 X _) ((f ≫ g)ᘁ)
    (CategoryStruct.comp (Y := @rightDual.{v₁, u₁} _ inst inst_1 Y _) (gᘁ) (fᘁ))
have rw : (f ≫ g)ᘁ =
  CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _)
        (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
      (@rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁ η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
      (@rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁ (g ⊗ₘ fᘁ) ≫
        Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _)) ≫
          ε_ Z (@rightDual.{v₁, u₁} _ inst inst_1 Z _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
            Iso.hom (λ_ (@rightDual.{v₁, u₁} _ inst inst_1 X _))))
Tactic: rw [rightAdjointMate_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
inst_4 : HasRightDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    @rightDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _)
        (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
    (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
        @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁
          (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _))
    (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁ η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
        @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁
          (g ⊗ₘ
            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 _)))))
have e_a : Eq (α :=
  @rightDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _)
      (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
  (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
    @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
        f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _))
  (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
    @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁
      (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
        (g ⊗ₘ
          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 _))))))
Tactic: simp only [← MonoidalCategory.whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
inst_4 : HasRightDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    @rightDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _)
        (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
    (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁
        (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
          f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _))
    (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      @rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁
        (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
          (g ⊗ₘ
            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 _))))))
have e_a : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))
  (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
    f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
  (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
    (g ⊗ₘ
      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 _)))))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
inst_4 : HasRightDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
      f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
    (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
      (g ⊗ₘ
        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 _)))))
have e_a : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))
  (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
    (g ⊗ₘ
      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 _)))))
  (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
    f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
Tactic: symm