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)
D : I → Type u₂
inst_2 : (i : I) → Category.{v₂, u₂} (D i)
inst_3 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi (C := D) (D := C) F).obj X) i)
      (Iso.inv (λ_ ((Functor.pi (C := D) (D := C) F).obj X)) i :
        (Functor.pi (C := D) (D := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
            ((Functor.pi (C := D) (D := C) F).obj X) i)
      (CategoryStruct.comp (Y :=
          (Functor.pi (C := D) (D := C) F).obj
            (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)) X))
          ((Functor.pi (C := D) (D := C) F).map (Iso.inv (λ_ X)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := pi.{w₁, v₁, u₁} C)
              ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)))
              ((Functor.pi (C := D) (D := C) F).obj X))
            (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i) (X i))
            ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi (C := D) (D := C) F).obj X))
          i :
        (Functor.pi (C := D) (D := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
            ((Functor.pi (C := D) (D := C) F).obj X) i)
⊢ Eq (α :=
    (Functor.pi (C := D) (D := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi (C := D) (D := C) F).obj X))
    (Iso.inv (λ_ ((Functor.pi (C := D) (D := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi (C := D) (D := C) F).obj
        (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)) X))
      ((Functor.pi (C := D) (D := C) F).map (Iso.inv (λ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C)
          ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)))
          ((Functor.pi (C := D) (D := C) F).obj X))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i) (X i))
        ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi (C := D) (D := 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 : I → Type u₂
inst_2 : (i : I) → Category.{v₂, u₂} (D i)
inst_3 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i : I
⊢ Eq.{v₁ + 1} (α :=
    (Functor.pi (C := D) (D := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
        ((Functor.pi (C := D) (D := C) F).obj X) i)
    (Iso.inv (λ_ ((Functor.pi (C := D) (D := C) F).obj X)) i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi (C := D) (D := C) F).obj X) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi (C := D) (D := C) F).obj
          (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)) X))
        ((Functor.pi (C := D) (D := C) F).map (Iso.inv (λ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C)
            ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D)))
            ((Functor.pi (C := D) (D := C) F).obj X))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i) (X i))
          ((fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi (C := D) (D := C) F).obj X))
        i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C))
          ((Functor.pi (C := D) (D := 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 : I → Type u₂
inst_2 : (i : I) → Category.{v₂, u₂} (D i)
inst_3 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
      (Iso.inv (ρ_ ((Functor.pi (C := D) (D := C) F).obj X)) i :
        (Functor.pi (C := D) (D := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
            ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
      (CategoryStruct.comp (Y :=
          (Functor.pi (C := D) (D := C) F).obj
            (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) X ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
          ((Functor.pi (C := D) (D := C) F).map (Iso.inv (ρ_ X)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
              ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
            (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i))
            ((Functor.pi (C := D) (D := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)))
          i :
        (Functor.pi (C := D) (D := C) F).obj X i ⟶
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
            ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
⊢ Eq (α :=
    (Functor.pi (C := D) (D := C) F).obj X ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)))
    (Iso.inv (ρ_ ((Functor.pi (C := D) (D := C) F).obj X)))
    (CategoryStruct.comp (Y :=
      (Functor.pi (C := D) (D := C) F).obj
        (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) X ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
      ((Functor.pi (C := D) (D := C) F).map (Iso.inv (ρ_ X)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
        (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i))
        ((Functor.pi (C := D) (D := 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 : I → Type u₂
inst_2 : (i : I) → Category.{v₂, u₂} (D i)
inst_3 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_4 : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i : I
⊢ Eq.{v₁ + 1} (α :=
    (Functor.pi (C := D) (D := C) F).obj X i ⟶
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
        ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (Iso.inv (ρ_ ((Functor.pi (C := D) (D := C) F).obj X)) i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C)) i)
    (CategoryStruct.comp (Y :=
        (Functor.pi (C := D) (D := C) F).obj
          (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) X ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
        ((Functor.pi (C := D) (D := C) F).map (Iso.inv (ρ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
            ((Functor.pi (C := D) (D := C) F).obj ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D))))
          (fun (i : I) ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) (𝒞 := pi.{w₁, v₂, u₂} D) i))
          ((Functor.pi (C := D) (D := C) F).obj X ◁ fun (i : I) ↦ Functor.OplaxMonoidal.η (F i)))
        i :
      (Functor.pi (C := D) (D := C) F).obj X i ⟶
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := 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 : I → Type u₂
inst_3 : (i : I) → Category.{v₂, u₂} (D i)
inst_4 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
inst_5 : (i : I) → BraidedCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : (i : I) → D i
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
        (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
      ((Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) X Y ≫
            (Functor.pi (C := D) (D := C) F).map (Iso.hom (β_ X Y)))
          i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
            ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
          (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
      ((Iso.hom (β_ ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)) ≫
            Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) Y X)
          i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
            ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
          (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
⊢ Eq (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
        ((Functor.pi (C := D) (D := C) F).obj Y) ⟶
      (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X))
    (Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) X Y ≫
      (Functor.pi (C := D) (D := C) F).map (Iso.hom (β_ X Y)))
    (Iso.hom (β_ ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)) ≫
      Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := 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 : I → Type u₂
inst_3 : (i : I) → Category.{v₂, u₂} (D i)
inst_4 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
inst_5 : (i : I) → BraidedCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : (i : I) → D i
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)
        i ⟶
      (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
    ((Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) X Y ≫
          (Functor.pi (C := D) (D := C) F).map (Iso.hom (β_ X Y)))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
        (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
    ((Iso.hom (β_ ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)) ≫
          Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) Y X)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
        (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) 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 : I → Type u₂
inst_3 : (i : I) → Category.{v₂, u₂} (D i)
inst_4 : (i : I) → MonoidalCategory.{v₂, u₂} (D i)
inst_5 : (i : I) → BraidedCategory.{v₂, u₂} (D i)
F : (i : I) → Functor.{v₂, v₁, u₂, u₁} (D i) (C i)
inst_6 : (i : I) → (F i).LaxBraided
X Y : (i : I) → D i
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)
        i ⟶
      (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
    ((Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) X Y ≫
          (Functor.pi (C := D) (D := C) F).map (Iso.hom (β_ X Y)))
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
        (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)
    ((Iso.hom (β_ ((Functor.pi (C := D) (D := C) F).obj X) ((Functor.pi (C := D) (D := C) F).obj Y)) ≫
          Functor.LaxMonoidal.μ (Functor.pi (C := D) (D := C) F) Y X)
        i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) ((Functor.pi (C := D) (D := C) F).obj X)
          ((Functor.pi (C := D) (D := C) F).obj Y) i ⟶
        (Functor.pi (C := D) (D := C) F).obj (tensorObj (𝒞 := pi.{w₁, v₂, u₂} D) Y X) i)

Tactic:
exact 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)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F G : D ⥤ ((i : I) → C i)
inst_4 : F.LaxMonoidal
inst_5 : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst_6 : ∀ (i : I), NatTrans.IsMonoidal (τ i)
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α := (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
      ((Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' (C := C) τ).app (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))) i :
        (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
      (Functor.LaxMonoidal.ε G i :
        (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
⊢ Eq (α := (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
    (Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' (C := C) τ).app (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)))
    (Functor.LaxMonoidal.ε 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)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F G : D ⥤ ((i : I) → C i)
inst_4 : F.LaxMonoidal
inst_5 : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst_6 : ∀ (i : I), NatTrans.IsMonoidal (τ i)
i : I
⊢ Eq.{v₁ + 1} (α := (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
    ((Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' (C := C) τ).app (tensorUnit.{v_1, u_1} D (𝒞 := inst_2))) i :
      (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)
    (Functor.LaxMonoidal.ε G i :
      (𝟙_ ((i : I) → C i)) (𝒞 := pi.{w₁, v₁, u₁} C) i ⟶ G.obj (tensorUnit.{v_1, u_1} D (𝒞 := inst_2)) i)

Tactic:
simpa using NatTrans.IsMonoidal.unit (τ := τ i)

Premises used: CategoryTheory.NatTrans.IsMonoidal.unit
-- 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 G : D ⥤ ((i : I) → C i)
inst_4 : F.LaxMonoidal
inst_5 : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst_6 : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
w :
  ∀ (i : I),
    Eq.{v₁ + 1} (α :=
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
      ((Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' (C := C) τ).app (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y)) i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
      ((((NatTrans.pi' (C := C) τ).app X ⊗ₘ (NatTrans.pi' (C := C) τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y) i :
        tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
⊢ Eq (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y))
    (Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' (C := C) τ).app (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y))
    (((NatTrans.pi' (C := C) τ).app X ⊗ₘ (NatTrans.pi' (C := C) τ).app Y) ≫ Functor.LaxMonoidal.μ G 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)
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : MonoidalCategory.{v_1, u_1} D
F G : D ⥤ ((i : I) → C i)
inst_4 : F.LaxMonoidal
inst_5 : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst_6 : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
i : I
⊢ Eq.{v₁ + 1} (α :=
    tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
    ((Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' (C := C) τ).app (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y)) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)
    ((((NatTrans.pi' (C := C) τ).app X ⊗ₘ (NatTrans.pi' (C := C) τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y) i :
      tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) (F.obj X) (F.obj Y) i ⟶ G.obj (tensorObj.{v_1, u_1} (𝒞 := inst_2) X Y) i)

Tactic:
simpa using NatTrans.IsMonoidal.tensor _ _ (τ := τ i)

Premises used: CategoryTheory.NatTrans.IsMonoidal.tensor
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : C
f g : X ⟶ Y
⊢ F.map (f + g) = F.map f + F.map g

Tactic:
Functor.Additive.map_add

Premises used: CategoryTheory.Functor.Additive.map_add
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : C
⊢ Eq (α := (a : X ⟶ Y) → F.obj X ⟶ F.obj Y) (⇑F.mapAddHom : (a : X ⟶ Y) → F.obj X ⟶ F.obj Y) F.map

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : C
f : X ⟶ Y
⊢ F.map (-f) = -F.map f

Tactic:
(F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_neg _

Premises used: AddMonoidHom.map_neg, CategoryTheory.Functor.mapAddHom
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : C
f g : X ⟶ Y
⊢ F.map (f - g) = F.map f - F.map g

Tactic:
(F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_sub _ _

Premises used: CategoryTheory.Functor.mapAddHom, AddMonoidHom.map_sub
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : C
f : X ⟶ Y
n : ℕ
⊢ F.map (n • f) = n • F.map f

Tactic:
(F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_nsmul _ _

Premises used: AddMonoidHom.map_nsmul, CategoryTheory.Functor.mapAddHom
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : C
f : X ⟶ Y
r : ℤ
⊢ F.map (r • f) = r • F.map f

Tactic:
(F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_zsmul _ _

Premises used: AddMonoidHom.map_zsmul, CategoryTheory.Functor.mapAddHom
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
X Y : C
α : Type u_4
f : α → (X ⟶ Y)
s : Finset α
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map (∑ a ∈ s, f a)) (∑ a ∈ s, F.map (f a))

Tactic:
map_sum F.mapAddHom f s

Premises used: map_sum, CategoryTheory.Functor.mapAddHom
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
map_add : autoParam (∀ {X Y : C} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g) Additive.map_add._autoParam
⊢ G.Additive

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
X Y : C
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
simp only [← NatIso.naturality_1 e (f + g), map_add, Preadditive.add_comp,
    NatTrans.naturality, Preadditive.comp_add, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.NatIso.naturality_1, CategoryTheory.Functor.map_add, CategoryTheory.Preadditive.add_comp, HAdd.hAdd, CategoryTheory.NatTrans.naturality, CategoryTheory.Preadditive.comp_add, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
⊢ F.Additive ↔ G.Additive

Tactic:
⟨fun _ => additive_of_iso e, fun _ => additive_of_iso e.symm⟩

Premises used: Iff.intro, CategoryTheory.Functor.additive_of_iso, CategoryTheory.Iso.symm