awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : C
inst_2 : MonObj M
N : C
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
⊢ Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ } ⟶ { unmop := N })
    (MonObj.mul ≫ f.mop) ((f.mop ⊗ₘ f.mop) ≫ MonObj.mul)
have apply : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := N : Cᴹᵒᵖ })
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (MonObj.mul ≫ f.mop))
  (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) ((f.mop ⊗ₘ f.mop) ≫ MonObj.mul))
Tactic: apply mopEquiv C |>.fullyFaithfulInverse.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : Cᴹᵒᵖ
inst_2 : MonObj M
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶ M.unmop)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.one ▷ M.unmop :
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶ M.unmop)
    (Iso.hom (λ_ M.unmop) : tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶ M.unmop)
have apply : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C))
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.one ▷ M.unmop :
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop)) :
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (Iso.hom (λ_ M.unmop)) :
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
Tactic: apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : Cᴹᵒᵖ
inst_2 : MonObj M
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ M.unmop)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (M.unmop ◁ Quiver.Hom.unmop MonObj.one :
          tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop) :
      tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ M.unmop)
    (Iso.hom (ρ_ M.unmop) : tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ M.unmop)
have apply : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C))
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (M.unmop ◁ Quiver.Hom.unmop MonObj.one :
          tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop)) :
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (Iso.hom (ρ_ M.unmop)) :
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
Tactic: apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : Cᴹᵒᵖ
inst_2 : MonObj M
N : Cᴹᵒᵖ
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
⊢ Eq (α := tensorUnit.{v_1, u_1} C (𝒞 := inst) ⟶ N.unmop) (MonObj.one ≫ f.unmop) MonObj.one
have apply : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) N.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (MonObj.one ≫ f.unmop))
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) MonObj.one)
Tactic: apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : Cᴹᵒᵖ
inst_2 : MonObj M
N : Cᴹᵒᵖ
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop ⟶ N.unmop) (MonObj.mul ≫ f.unmop)
    ((f.unmop ⊗ₘ f.unmop) ≫ MonObj.mul)
have apply : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) N.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (MonObj.mul ≫ f.unmop))
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) ((f.unmop ⊗ₘ f.unmop) ≫ MonObj.mul))
Tactic: apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
W X Y Z : Cᵒᵖ
⊢ Eq (α :=
    unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W)
            (unop
              (op
                (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X)
                  (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))))))))) ⟶
      unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (unop
              (op
                (tensorObj.{v₁, u₁} (𝒞 := inst) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X))))
                  (unop Y))))
            (unop Z))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (α_ (unop W) (unop X) (unop Y))))) ▷ unop Z) ≫
        Iso.hom
            (Iso.op (Iso.symm (α_ (unop W) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y)))) (unop Z)))) ≫
          Quiver.Hom.op (unop W ◁ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (α_ (unop X) (unop Y) (unop Z))))))))
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (α_ (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)))) (unop Y) (unop Z)))) ≫
        Iso.hom
          (Iso.op (Iso.symm (α_ (unop W) (unop X) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z)))))))))
have dsimp : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (unop W)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)) (unop Y)) (unop Z))
  ((unop W ◁ Iso.inv (α_ (unop X) (unop Y) (unop Z)) ≫
      Iso.inv (α_ (unop W) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y)) (unop Z))) ≫
    Iso.inv (α_ (unop W) (unop X) (unop Y)) ▷ unop Z)
  (Iso.inv (α_ (unop W) (unop X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))) ≫
    Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)) (unop Y) (unop Z)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y))) ⟶
      unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))))
            (unop Y))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (α_ (unop X) (unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (unop Y)))) ≫
        Quiver.Hom.op (unop X ◁ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (λ_ (unop Y))))))))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρ_ (unop X))))) ▷ unop Y)))
have dsimp : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (unop Y))
  (unop X ◁ Iso.inv (λ_ (unop Y)) ≫ Iso.inv (α_ (unop X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (unop Y)))
  (Iso.inv (ρ_ (unop X)) ▷ unop Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
W X Y Z : Cᴹᵒᵖ
⊢ Eq (α :=
    {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop
              {
                  unmop :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop
                      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop : Cᴹᵒᵖ }.unmop :
                  Cᴹᵒᵖ }.unmop :
          Cᴹᵒᵖ }.unmop ⟶
      {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst)
              {
                  unmop :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop }.unmop
                      X.unmop }.unmop
              W.unmop }.unmop)
    (Quiver.Hom.unmop
      (Quiver.Hom.mop (Z.unmop ◁ Quiver.Hom.unmop (Iso.hom (Iso.mop (Iso.symm (α_ Y.unmop X.unmop W.unmop))))) ≫
        Iso.hom
            (Iso.mop
              (Iso.symm
                (α_ Z.unmop { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop : Cᴹᵒᵖ }.unmop W.unmop))) ≫
          Quiver.Hom.mop (Quiver.Hom.unmop (Iso.hom (Iso.mop (Iso.symm (α_ Z.unmop Y.unmop X.unmop)))) ▷ W.unmop)))
    (Quiver.Hom.unmop
      (Iso.hom
          (Iso.mop
            (Iso.symm (α_ Z.unmop Y.unmop { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop : Cᴹᵒᵖ }.unmop))) ≫
        Iso.hom
          (Iso.mop (Iso.symm (α_ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop }.unmop X.unmop W.unmop)))))
have dsimp : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop
      (tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop) X.unmop) W.unmop)
  (Z.unmop ◁ Iso.inv (α_ Y.unmop X.unmop W.unmop) ≫
    Iso.inv (α_ Z.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop) W.unmop) ≫
      Iso.inv (α_ Z.unmop Y.unmop X.unmop) ▷ W.unmop)
  (Iso.inv (α_ Z.unmop Y.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop)) ≫
    Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop) X.unmop W.unmop))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop
              {
                  unmop :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) { unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ }.unmop X.unmop :
                  Cᴹᵒᵖ }.unmop :
          Cᴹᵒᵖ }.unmop ⟶
      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop }.unmop)
    (Quiver.Hom.unmop
      (Iso.hom (Iso.mop (Iso.symm (α_ Y.unmop { unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ }.unmop X.unmop))) ≫
        Quiver.Hom.mop (Quiver.Hom.unmop (Iso.hom (Iso.mop (ρ_ Y.unmop))) ▷ X.unmop)))
    (Quiver.Hom.unmop (Quiver.Hom.mop (Y.unmop ◁ Quiver.Hom.unmop (Iso.hom (Iso.mop (λ_ X.unmop))))))
have dsimp : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.unmop) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop)
  (Iso.inv (α_ Y.unmop (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.unmop) ≫ Iso.hom (ρ_ Y.unmop) ▷ X.unmop)
  (Y.unmop ◁ Iso.hom (λ_ X.unmop))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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.{v_2 + 1} (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) X Y ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) X Z) (X ◁ 0) 0
have 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)
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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.{v_2 + 1} (α := tensorObj.{v_2, u_2} (𝒞 := inst_4) Y X ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_4) Z X) (0 ▷ X) 0
have 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)
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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
⊢ 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)
have 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))
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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 + 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)
have 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))
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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} (α :=
    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)))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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)
    (∑ j : J, X ◁ b.π j ≫ X ◁ b.ι j) (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X b.pt))
have 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))
Tactic: simp_rw [← id_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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} (α :=
    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)))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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) 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))
have 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))
Tactic: simp_rw [← tensorHom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Preadditive (goal)
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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Fintype J
X : C
f : J → C
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
      biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (Iso.hom (leftDistributor X f) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (∑ j : J,
        X ◁ biproduct.π f j ≫
          biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
        biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
have w : ∀ (j : J),
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (Iso.hom (leftDistributor X f) :
          tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
    (CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
        (∑ j : J,
          X ◁ biproduct.π f j ≫
            biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j)
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j))
Tactic: ext