awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i ⟶ X i)
    (Iso.hom (ρ_ X) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i ⟶ X i)
    (Iso.hom (ρ_ (X i)) : tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (tensorUnit.{v₁, u₁} (C i) (𝒞 := inst i)) ⟶ X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (Iso.inv (ρ_ X) i : X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (Iso.inv (ρ_ (X i)) : X i ⟶ tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (tensorUnit.{v₁, u₁} (C i) (𝒞 := inst i)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i ≅ X i)
    (isoApp (C := C) (ρ_ X) i) (ρ_ (X i))

Tactic:
rfl

Premises used: CategoryTheory.Pi.isoApp, rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
A B X Y : (i : I) → C i
f : A ⟶ B
g : X ⟶ Y
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
      ((f ⊗ₘ g) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
      ((f ▷ X ≫ B ◁ g) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
⊢ Eq (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y) (f ⊗ₘ g) (f ▷ X ≫ B ◁ g)

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
A B X Y : (i : I) → C i
f : A ⟶ B
g : X ⟶ Y
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
    ((f ⊗ₘ g) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
    ((f ▷ X ≫ B ◁ g) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)

Tactic:
simp [tensorHom_def, whiskerLeft]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
      ((Iso.hom (α_ X Y Z) ≫
            Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z i)) ≫
              Iso.hom (α_ Y Z X))
          i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
      ((Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Y i)) ▷ Z ≫
            Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)))
          i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X))
    (Iso.hom (α_ X Y Z) ≫
      Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z i)) ≫ Iso.hom (α_ Y Z X))
    (Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Y i)) ▷ Z ≫
      Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)))

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
    ((Iso.hom (α_ X Y Z) ≫
          Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z i)) ≫
            Iso.hom (α_ Y Z X))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)
    ((Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Y i)) ▷ Z ≫
          Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) Z i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) i)

Tactic:
apply hexagon_forward

Premises used: CategoryTheory.BraidedCategory.hexagon_forward
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
      ((Iso.inv (α_ X Y Z) ≫
            Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i) (Z i)) ≫
              Iso.inv (α_ Z X Y))
          i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
      ((X ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (Y i) (Z i)) ≫
            Iso.inv (α_ X Z Y) ≫ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)) ▷ Y)
          i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y)
    (Iso.inv (α_ X Y Z) ≫
      Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i) (Z i)) ≫ Iso.inv (α_ Z X Y))
    (X ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (Y i) (Z i)) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)) ▷ Y)

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
    ((Iso.inv (α_ X Y Z) ≫
          Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i) (Z i)) ≫
            Iso.inv (α_ Z X Y))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)
    ((X ◁ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (Y i) (Z i)) ≫
          Iso.inv (α_ X Z Y) ≫ Iso.hom (isoMk (C := C) fun (i : I) ↦ β_ (X i) (Z i)) ▷ Y)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y Z) i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Z X) Y i)

Tactic:
apply hexagon_reverse

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y X i)
    (Iso.hom (β_ X Y) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y X i)
    (Iso.hom (β_ (X i) (Y i)) :
      tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (Y i) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst i) (Y i) (X i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i)
    (Iso.inv (β_ X Y) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i)
    (Iso.inv (β_ (X i) (Y i)) :
      tensorObj.{v₁, u₁} (𝒞 := inst i) (Y i) (X i) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst i) (X i) (Y i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
X Y : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y i ≅ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) Y X i)
    (isoApp (C := C) (β_ X Y) i) (β_ (X i) (Y i))

Tactic:
rfl

Premises used: CategoryTheory.Pi.isoApp, rfl
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → SymmetricCategory.{v₁, u₁} (C i)
X Y : (i : I) → C i
w : ∀ (i : I), Eq.{v₁ + 1} ((Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X)) i) (𝟙 (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) i)
⊢ Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y)

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → SymmetricCategory.{v₁, u₁} (C i)
X Y : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} ((Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X)) i) (𝟙 (tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) X Y) i)

Tactic:
apply symmetry

Premises used: CategoryTheory.SymmetricCategory.symmetry
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : D
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi' (C := C) F).obj X) i)
      (Iso.inv (λ_ ((Functor.pi' (C := C) F).obj X)) i :
        (Functor.pi' (C := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
            ((Functor.pi' (C := C) F).obj X) i)
      (CategoryStruct.comp (Y :=
          (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X))
          ((Functor.pi' (C := C) F).map (Iso.inv (λ_ X)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
              ((Functor.pi' (C := C) F).obj X))
            (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X)
            ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' (C := C) F).obj X))
          i :
        (Functor.pi' (C := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
            ((Functor.pi' (C := C) F).obj X) i)
⊢ Eq (α :=
    (Functor.pi' (C := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi' (C := C) F).obj X))
    (Iso.inv (λ_ ((Functor.pi' (C := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X))
      ((Functor.pi' (C := C) F).map (Iso.inv (λ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
          ((Functor.pi' (C := C) F).obj X))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X)
        ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' (C := C) F).obj X)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : D
i : I
⊢ Eq.{v₁ + 1} (α :=
    (Functor.pi' (C := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi' (C := C) F).obj X) i)
    (Iso.inv (λ_ ((Functor.pi' (C := C) F).obj X)) i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi' (C := C) F).obj X) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X))
        ((Functor.pi' (C := C) F).map (Iso.inv (λ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
            ((Functor.pi' (C := C) F).obj X))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) X)
          ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' (C := C) F).obj X))
        i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi' (C := C) F).obj X) i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : D
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
      (Iso.inv (ρ_ ((Functor.pi' (C := C) F).obj X)) i :
        (Functor.pi' (C := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
            ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
      (CategoryStruct.comp (Y :=
          (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
          ((Functor.pi' (C := C) F).map (Iso.inv (ρ_ X)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
              ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
            (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
            ((Functor.pi' (C := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)))
          i :
        (Functor.pi' (C := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
            ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
⊢ Eq (α :=
    (Functor.pi' (C := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)))
    (Iso.inv (ρ_ ((Functor.pi' (C := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
      ((Functor.pi' (C := C) F).map (Iso.inv (ρ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
          ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
        ((Functor.pi' (C := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : D
i : I
⊢ Eq.{v₁ + 1} (α :=
    (Functor.pi' (C := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (Iso.inv (ρ_ ((Functor.pi' (C := C) F).obj X)) i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
        ((Functor.pi' (C := C) F).map (Iso.inv (ρ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
            ((Functor.pi' (C := C) F).obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) X (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
          ((Functor.pi' (C := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)))
        i :
      (Functor.pi' (C := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : MonoidalCategory.{v_1, u_1} D
inst_5 : BraidedCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : D
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
      ((Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) X Y ≫ (Functor.pi' (C := C) F).map (Iso.hom (β_ X Y))) i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
          (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
      ((Iso.hom (β_ ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y)) ≫
            Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) Y X)
          i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
          (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) ⟶
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X))
    (Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) X Y ≫ (Functor.pi' (C := C) F).map (Iso.hom (β_ X Y)))
    (Iso.hom (β_ ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y)) ≫
      Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) Y X)

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : MonoidalCategory.{v_1, u_1} D
inst_5 : BraidedCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : D
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
    ((Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) X Y ≫ (Functor.pi' (C := C) F).map (Iso.hom (β_ X Y))) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
    ((Iso.hom (β_ ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y)) ≫
          Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) Y X)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)

Tactic:
Functor.LaxBraided.braided _ _

Premises used: CategoryTheory.Functor.LaxBraided.braided
-- Module: Mathlib.CategoryTheory.Pi.Monoidal
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
inst_2 : (i : I) → BraidedCategory.{v₁, u₁} (C i)
D : Type u_1
inst_3 : Category.{v_1, u_1} D
inst_4 : MonoidalCategory.{v_1, u_1} D
inst_5 : BraidedCategory.{v_1, u_1} D
F : (i : I) → Functor.{v_1, v₁, u_1, u₁} D (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : D
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
      (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
    ((Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) X Y ≫ (Functor.pi' (C := C) F).map (Iso.hom (β_ X Y))) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)
    ((Iso.hom (β_ ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y)) ≫
          Functor.LaxMonoidal.μ (Functor.pi' (C := C) F) Y X)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi' (C := C) F).obj X) ((Functor.pi' (C := C) F).obj Y) i ⟶
        (Functor.pi' (C := C) F).obj (tensorObj.{v_1, u_1} (𝒞 := inst_3) Y X) i)

Tactic:
exact Functor.LaxBraided.braided _ _

Premises used: CategoryTheory.Functor.LaxBraided.braided