awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    X.unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))
          X).unmop)
    (Quiver.Hom.unmop (Iso.inv (λ_ X))) (Iso.inv (ρ_ X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) : Cᴹᵒᵖ } ≅ { unmop := X })
    (Iso.mop (ρ_ X)) (λ_ { unmop := X })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X
          (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))).unmop ≅
      X.unmop)
    (Iso.unmop (ρ_ X)) (λ_ X.unmop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, CategoryTheory.Functor.mapIso, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) : Cᴹᵒᵖ } ⟶ { unmop := X })
    (Quiver.Hom.mop (Iso.hom (ρ_ X))) (Iso.hom (λ_ { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X
          (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))).unmop ⟶
      X.unmop)
    (Quiver.Hom.unmop (Iso.hom (ρ_ X))) (Iso.hom (λ_ X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := X : Cᴹᵒᵖ } ⟶ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) })
    (Quiver.Hom.mop (Iso.inv (ρ_ X))) (Iso.inv (λ_ { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    X.unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X
          (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))).unmop)
    (Quiver.Hom.unmop (Iso.inv (ρ_ X))) (Iso.inv (λ_ X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} Cᴹᵒᵖᴹᵒᵖ (𝒞 := monoidalOppositeCategory) ⟶
      obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (Equivalence.inverse (mopMopEquivalence C)))
    (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction (mopMopEquivalence C)))
        (tensorUnit.{v₁, u₁} Cᴹᵒᵖᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) ≫
      map (Equivalence.inverse (mopMopEquivalence C)) (η (Equivalence.functor (mopMopEquivalence C))))

Tactic:
simp [ε, η, mopMopEquivalence, Equivalence.trans, unmopEquiv, ε]

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.MonoidalOpposite.unmopEquiv, CategoryTheory.Equivalence.trans, CategoryTheory.MonoidalOpposite.mopMopEquivalence, CategoryTheory.Functor.OplaxMonoidal.η
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory)
        (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) X)
        (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) Y) ⟶
      obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (Equivalence.inverse (mopMopEquivalence C)) X Y)
    (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction (mopMopEquivalence C)))
        (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory)
          (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) X)
          (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) Y)) ≫
      map (Equivalence.inverse (mopMopEquivalence C))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst)
            (obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (mopMopEquivalence C))
              (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) X))
            (obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (mopMopEquivalence C))
              (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) Y)))
          (δ (Equivalence.functor (mopMopEquivalence C))
            (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) X)
            (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (mopMopEquivalence C)) Y))
          (NatTrans.app (Adjunction.counit (Equivalence.toAdjunction (mopMopEquivalence C))) X ⊗ₘ
            NatTrans.app (Adjunction.counit (Equivalence.toAdjunction (mopMopEquivalence C))) Y)))

Tactic:
simp [μ, δ, mopMopEquivalence, Equivalence.trans, unmopEquiv, μ]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ, CategoryTheory.Functor.LaxMonoidal.μ, CategoryTheory.MonoidalOpposite.unmopEquiv, CategoryTheory.Equivalence.trans, CategoryTheory.MonoidalOpposite.mopMopEquivalence
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} Cᵒᵖᵒᵖ (𝒞 := Category.opposite) ⟶
      obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (Equivalence.inverse (opOpEquivalence C)))
    (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction (opOpEquivalence C)))
        (tensorUnit.{v₁, u₁} Cᵒᵖᵒᵖ (𝒞 := Category.opposite)) ≫
      map (Equivalence.inverse (opOpEquivalence C)) (η (Equivalence.functor (opOpEquivalence C))))

Tactic:
simp [opOpEquivalence]

Premises used: CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ ∀ (X Y : C),
    Eq.{v₁ + 1} (α :=
      tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) X)
          (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) Y) ⟶
        obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ (Equivalence.inverse (opOpEquivalence C)) X Y)
      (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction (opOpEquivalence C)))
          (tensorObj.{v₁, u₁} (𝒞 := Category.opposite)
            (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) X)
            (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) Y)) ≫
        map (Equivalence.inverse (opOpEquivalence C))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst)
              (obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (opOpEquivalence C))
                (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) X))
              (obj.{v₁, v₁, u₁, u₁} (Equivalence.functor (opOpEquivalence C))
                (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) Y)))
            (δ (Equivalence.functor (opOpEquivalence C))
              (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) X)
              (obj.{v₁, v₁, u₁, u₁} (Equivalence.inverse (opOpEquivalence C)) Y))
            (NatTrans.app (Adjunction.counit (Equivalence.toAdjunction (opOpEquivalence C))) X ⊗ₘ
              NatTrans.app (Adjunction.counit (Equivalence.toAdjunction (opOpEquivalence C))) Y)))

Tactic:
simp [opOpEquivalence]

Premises used: CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) W Y ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X Z) (f ⊗ₘ 0) 0

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
W X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) W Y ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X Z) (0 ⊗ₘ f) 0

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g h : Y ⟶ Z
⊢ f ⊗ₘ (g + h) =
    HAdd.hAdd (α := tensorObj.{v_1, u_1} (𝒞 := inst) W Y ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X Z) (f ⊗ₘ g) (f ⊗ₘ h)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
W X Y Z : C
f g : W ⟶ X
h : Y ⟶ Z
⊢ (f + g) ⊗ₘ h =
    HAdd.hAdd (α := tensorObj.{v_1, u_1} (𝒞 := inst) W Y ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X Z) (f ⊗ₘ h) (g ⊗ₘ h)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
a :
  Eq (α := F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) X Y) ⟶ F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) X Z))
    (F.map (X ◁ 0)) (F.map 0)
⊢ Eq.{v_2 + 1} (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) X Y ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) X Z) (X ◁ 0) 0

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
⊢ Eq (α := F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) X Y) ⟶ F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) X Z))
    (F.map (X ◁ 0)) (F.map 0)

Tactic:
simp [Functor.Monoidal.map_whiskerLeft]

Premises used: CategoryTheory.Functor.Monoidal.map_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
a :
  Eq (α := F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) Y X) ⟶ F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) Z X))
    (F.map (0 ▷ X)) (F.map 0)
⊢ Eq.{v_2 + 1} (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) Y X ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) Z X) (0 ▷ X) 0

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
⊢ Eq (α := F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) Y X) ⟶ F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_4) Z X))
    (F.map (0 ▷ X)) (F.map 0)

Tactic:
simp [Functor.Monoidal.map_whiskerRight]

Premises used: CategoryTheory.Functor.Monoidal.map_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
f g : Y ⟶ Z
a :
  F.map (X ◁ (f + g)) =
    F.map
      (HAdd.hAdd (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) X Y ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) X Z) (X ◁ f) (X ◁ g))
⊢ X ◁ (f + g) =
    HAdd.hAdd (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) X Y ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) X Z) (X ◁ f) (X ◁ g)

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
f g : Y ⟶ Z
⊢ F.map (X ◁ (f + g)) =
    F.map
      (HAdd.hAdd (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) X Y ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) X Z) (X ◁ f) (X ◁ g))

Tactic:
simp only [Functor.Monoidal.map_whiskerLeft, Functor.map_add, Preadditive.comp_add,
        Preadditive.add_comp, MonoidalPreadditive.whiskerLeft_add]

Premises used: CategoryTheory.MonoidalPreadditive.whiskerLeft_add, CategoryTheory.Functor.map_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, CategoryTheory.Functor.Monoidal.map_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
f g : Y ⟶ Z
a :
  F.map ((f + g) ▷ X) =
    F.map
      (HAdd.hAdd (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) Y X ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) Z X) (f ▷ X) (g ▷ X))
⊢ (f + g) ▷ X =
    HAdd.hAdd (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) Y X ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) Z X) (f ▷ X) (g ▷ X)

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_7 : F.Monoidal
inst_8 : F.Faithful
inst_9 : F.Additive
X Y Z : D
f g : Y ⟶ Z
⊢ F.map ((f + g) ▷ X) =
    F.map
      (HAdd.hAdd (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) Y X ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) Z X) (f ▷ X) (g ▷ X))

Tactic:
simp only [Functor.Monoidal.map_whiskerRight, Functor.map_add, Preadditive.comp_add,
        Preadditive.add_comp, MonoidalPreadditive.add_whiskerRight]

Premises used: CategoryTheory.MonoidalPreadditive.add_whiskerRight, CategoryTheory.Functor.Monoidal.map_whiskerRight, CategoryTheory.Functor.map_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
P Q R : C
J : Type u_2
s : Finset J
g : J → (Q ⟶ R)
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) P Q ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) P R) (P ◁ ∑ j ∈ s, g j)
    (∑ j ∈ s, P ◁ g j)

Tactic:
map_sum ((tensoringLeft C).obj P).mapAddHom g s

Premises used: CategoryTheory.MonoidalCategory.tensoringLeft, map_sum, CategoryTheory.Functor.mapAddHom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
Q R : C
J : Type u_2
s : Finset J
g : J → (Q ⟶ R)
P : C
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) Q P ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) R P) ((∑ j ∈ s, g j) ▷ P)
    (∑ j ∈ s, g j ▷ P)

Tactic:
map_sum ((tensoringRight C).obj P).mapAddHom g s

Premises used: CategoryTheory.MonoidalCategory.tensoringRight, map_sum, CategoryTheory.Functor.mapAddHom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) P R ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) Q S) (f ⊗ₘ ∑ j ∈ s, g j)
    (∑ j ∈ s, f ⊗ₘ g j)

Tactic:
simp only [tensorHom_def, whiskerLeft_sum, Preadditive.comp_sum]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Preadditive.comp_sum, CategoryTheory.whiskerLeft_sum
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) R P ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) S Q) ((∑ j ∈ s, g j) ⊗ₘ f)
    (∑ j ∈ s, g j ⊗ₘ f)

Tactic:
simp only [tensorHom_def, sum_whiskerRight, Preadditive.sum_comp]

Premises used: CategoryTheory.sum_whiskerRight, CategoryTheory.Preadditive.sum_comp, CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X : C
J : Type
inst_4 : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v_1, u_1} f
i : b.IsBilimit
dsimp :
  Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt)
    (∑ j : J, X ◁ b.π j ≫ X ◁ b.ι j) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt))
⊢ Eq.{v_1 + 1} (α :=
    Bicone.pt (F := Functor.obj.{v_1, v_1, u_1, u_1} (tensorLeft X) ∘ f) (Functor.mapBicone (tensorLeft X) b) ⟶
      Bicone.pt (F := Functor.obj.{v_1, v_1, u_1, u_1} (tensorLeft X) ∘ f) (Functor.mapBicone (tensorLeft X) b))
    (∑ j : J, Bicone.π (Functor.mapBicone (tensorLeft X) b) j ≫ Bicone.ι (Functor.mapBicone (tensorLeft X) b) j)
    (𝟙 (Bicone.pt (F := Functor.obj.{v_1, v_1, u_1, u_1} (tensorLeft X) ∘ f) (Functor.mapBicone (tensorLeft X) b)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X : C
J : Type
inst_4 : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v_1, u_1} f
i : b.IsBilimit
simp_rw :
  Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt)
    (∑ x : J, (𝟙 X ⊗ₘ b.π x) ≫ (𝟙 X ⊗ₘ b.ι x)) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt))
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt)
    (∑ j : J, X ◁ b.π j ≫ X ◁ b.ι j) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt))

Tactic:
simp_rw [← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X : C
J : Type
inst_4 : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v_1, u_1} f
i : b.IsBilimit
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt)
    (∑ x : J, (𝟙 X ⊗ₘ b.π x) ≫ (𝟙 X ⊗ₘ b.ι x)) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt))

Tactic:
simp only [tensorHom_comp_tensorHom, Category.comp_id, ← tensor_sum, ← id_tensorHom_id,
              IsBilimit.total i]

Premises used: CategoryTheory.Limits.IsBilimit.total, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.tensor_sum, CategoryTheory.MonoidalCategory.id_tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X : C
J : Type
inst_4 : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v_1, u_1} f
i : b.IsBilimit
dsimp :
  Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X)
    (∑ j : J, b.π j ▷ X ≫ b.ι j ▷ X) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X))
⊢ Eq.{v_1 + 1} (α :=
    Bicone.pt (F := Functor.obj.{v_1, v_1, u_1, u_1} (tensorRight X) ∘ f) (Functor.mapBicone (tensorRight X) b) ⟶
      Bicone.pt (F := Functor.obj.{v_1, v_1, u_1, u_1} (tensorRight X) ∘ f) (Functor.mapBicone (tensorRight X) b))
    (∑ j : J, Bicone.π (Functor.mapBicone (tensorRight X) b) j ≫ Bicone.ι (Functor.mapBicone (tensorRight X) b) j)
    (𝟙 (Bicone.pt (F := Functor.obj.{v_1, v_1, u_1, u_1} (tensorRight X) ∘ f) (Functor.mapBicone (tensorRight X) b)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X : C
J : Type
inst_4 : Finite J
val : Fintype J
f : J → C
b : Bicone.{0, v_1, u_1} f
i : b.IsBilimit
simp_rw :
  Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X)
    (∑ x : J, (b.π x ⊗ₘ 𝟙 X) ≫ (b.ι x ⊗ₘ 𝟙 X)) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X))
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X)
    (∑ j : J, b.π j ▷ X ≫ b.ι j ▷ X) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) b.pt X))

Tactic:
simp_rw [← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_id