awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
X Y Z : C
f : J → C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) Y (tensorObj.{v_1, u_1} (𝒞 := inst) Z (biproduct.{0, v_1, u_1} f))
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
j : J
⊢ (g ≫ Iso.inv (α_ Y Z (biproduct.{0, v_1, u_1} f))) ≫ tensorObj.{v_1, u_1} (𝒞 := inst) Y Z ◁ biproduct.π f j =
    (h ≫ Iso.inv (α_ Y Z (biproduct.{0, v_1, u_1} f))) ≫ tensorObj.{v_1, u_1} (𝒞 := inst) Y Z ◁ biproduct.π f j

Tactic:
simp [w]
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
intro : ∀ (val : Fintype J), g = h
⊢ g = h

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
val : Fintype J
intro :
  Eq (α := (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
    (Iso.inv (rightDistributor f X) ≫ g :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
    (Iso.inv (rightDistributor f X) ≫ h :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
⊢ g = h

Tactic:
apply (cancel_epi (rightDistributor f X).inv).mp

Premises used: CategoryTheory.rightDistributor, Iff.mp, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
val : Fintype J
intro :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (Iso.inv (rightDistributor f X) ≫ g :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y) =
      CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (Iso.inv (rightDistributor f X) ≫ h :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
⊢ Eq (α := (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
    (Iso.inv (rightDistributor f X) ≫ g :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
    (Iso.inv (rightDistributor f X) ≫ h :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)

Tactic:
ext
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
val : Fintype J
j : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (Iso.inv (rightDistributor f X) ≫ g :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y) =
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
        tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
          biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
      (Iso.inv (rightDistributor f X) ≫ h :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)

Tactic:
simp [w]
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
intro : ∀ (val : Fintype J), g = h
intro₁ :
  ∀ (val : Fintype J),
    Eq (α := (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
      (Iso.inv (rightDistributor f X) ≫ g :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
      (Iso.inv (rightDistributor f X) ≫ h :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
intro₂ :
  ∀ (val : Fintype J) (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (Iso.inv (rightDistributor f X) ≫ g :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y) =
      CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j :
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶
            biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X)
        (Iso.inv (rightDistributor f X) ≫ h :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶ Y)
⊢ g = h

Tactic:
classical
  cases nonempty_fintype J
  apply (cancel_epi (rightDistributor f X).inv).mp
  ext
  simp [w]

Premises used: CategoryTheory.rightDistributor, nonempty_fintype, Iff.mp, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
intro : ∀ (val : Fintype J), g = h
⊢ g = h

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
val : Fintype J
intro :
  Eq (α := X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
    (g ≫ Iso.hom (rightDistributor f Y) :
      X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
    (h ≫ Iso.hom (rightDistributor f Y) :
      X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
⊢ g = h

Tactic:
apply (cancel_mono (rightDistributor f Y).hom).mp

Premises used: CategoryTheory.rightDistributor, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
val : Fintype J
intro :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (g ≫ Iso.hom (rightDistributor f Y) :
          X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) =
      CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (h ≫ Iso.hom (rightDistributor f Y) :
          X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
⊢ Eq (α := X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
    (g ≫ Iso.hom (rightDistributor f Y) :
      X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
    (h ≫ Iso.hom (rightDistributor f Y) :
      X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)

Tactic:
ext
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
val : Fintype J
j : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
      (g ≫ Iso.hom (rightDistributor f Y) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) =
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
      (h ≫ Iso.hom (rightDistributor f Y) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)

Tactic:
simp [w]
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
intro : ∀ (val : Fintype J), g = h
intro₁ :
  ∀ (val : Fintype J),
    Eq (α := X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
      (g ≫ Iso.hom (rightDistributor f Y) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
      (h ≫ Iso.hom (rightDistributor f Y) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
intro₂ :
  ∀ (val : Fintype J) (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (g ≫ Iso.hom (rightDistributor f Y) :
          X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) =
      CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (h ≫ Iso.hom (rightDistributor f Y) :
          X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y)
⊢ g = h

Tactic:
classical
  cases nonempty_fintype J
  apply (cancel_mono (rightDistributor f Y).hom).mp
  ext
  simp [w]

Premises used: CategoryTheory.rightDistributor, CategoryTheory.cancel_mono, nonempty_fintype, Iff.mp, CategoryTheory.Iso.hom
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y Z : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
apply : Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ g = Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ h
⊢ g = h

Tactic:
apply (cancel_epi (α_ _ _ _).inv).mp

Premises used: Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y Z : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
w₁ :
  ∀ (j : J),
    biproduct.ι f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≫ Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ g =
      biproduct.ι f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≫ Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ h
⊢ Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ g = Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ h

Tactic:
ext
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y Z : C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) Y ⟶ Z
w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h
j : J
⊢ biproduct.ι f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≫ Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ g =
    biproduct.ι f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≫ Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ h

Tactic:
simp [w]
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y Z : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y) Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
apply : g ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z) = h ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z)
⊢ g = h

Tactic:
apply (cancel_mono (α_ _ _ _).hom).mp

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y Z : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y) Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
w₁ :
  ∀ (j : J),
    (g ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z)) ≫ biproduct.π f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) Y Z =
      (h ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z)) ≫ biproduct.π f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) Y Z
⊢ g ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z) = h ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z)

Tactic:
ext
-- 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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
f : J → C
X Y Z : C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y) Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
j : J
⊢ (g ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z)) ≫ biproduct.π f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) Y Z =
    (h ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z)) ≫ biproduct.π f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) Y Z

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorLeft W)
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorLeft W) (tensorObj.{v, u} (𝒞 := inst) X₁.right X₂.left) ⟶
      (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) W X₁.left) (W ◁ X₁.hom) □ X₂).right)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorLeft W)
        (pushout (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (map (tensorLeft W) (pushout.inl (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (Iso.hom
          (Iso.trans (Y :=
            pushout (X := obj.{v, v, u, u} (tensorLeft W) (tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left))
              (map (tensorLeft W) (X₁.hom ▷ X₂.left)) (map (tensorLeft W) (X₁.left ◁ X₂.hom)))
            (IsPushout.isoPushout ⋯)
            (HasColimit.isoOfNatIso
              (spanExt (Iso.symm (α_ W X₁.left X₂.left)) (Iso.symm (α_ W X₁.right X₂.left))
                (Iso.symm (α_ W X₁.left X₂.right)) ⋯ ⋯))) ≫
        (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) W X₁.left) (W ◁ X₁.hom) □ X₂).hom))
    (map (tensorLeft W) (pushout.inl (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) W (X₁ □ X₂).left) (W ◁ (X₁ □ X₂).hom)).hom ≫
        Iso.hom (Iso.symm (α_ W X₁.right X₂.right)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorLeft W)
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorLeft W) (tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.right) ⟶
      (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) W X₁.left) (W ◁ X₁.hom) □ X₂).right)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorLeft W)
        (pushout (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (map (tensorLeft W) (pushout.inr (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (Iso.hom
          (Iso.trans (Y :=
            pushout (X := obj.{v, v, u, u} (tensorLeft W) (tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left))
              (map (tensorLeft W) (X₁.hom ▷ X₂.left)) (map (tensorLeft W) (X₁.left ◁ X₂.hom)))
            (IsPushout.isoPushout ⋯)
            (HasColimit.isoOfNatIso
              (spanExt (Iso.symm (α_ W X₁.left X₂.left)) (Iso.symm (α_ W X₁.right X₂.left))
                (Iso.symm (α_ W X₁.left X₂.right)) ⋯ ⋯))) ≫
        (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) W X₁.left) (W ◁ X₁.hom) □ X₂).hom))
    (map (tensorLeft W) (pushout.inr (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) W (X₁ □ X₂).left) (W ◁ (X₁ □ X₂).hom)).hom ≫
        Iso.hom (Iso.symm (α_ W X₁.right X₂.right)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight W)
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorRight W) (tensorObj.{v, u} (𝒞 := inst) X₁.right X₂.left) ⟶
      (X₁ □ Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₂.left W) (X₂.hom ▷ W)).right)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight W)
        (pushout (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (map (tensorRight W) (pushout.inl (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)))
      (Iso.hom
          (Iso.trans (Y :=
            pushout (X := obj.{v, v, u, u} (tensorRight W) (tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left))
              (map (tensorRight W) (X₁.hom ▷ X₂.left)) (map (tensorRight W) (X₁.left ◁ X₂.hom)))
            (IsPushout.isoPushout ⋯)
            (HasColimit.isoOfNatIso
              (spanExt (α_ X₁.left X₂.left W) (α_ X₁.right X₂.left W) (α_ X₁.left X₂.right W) ⋯ ⋯))) ≫
        (X₁ □ Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) X₂.left W) (X₂.hom ▷ W)).hom))
    (map (tensorRight W) (pushout.inl (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (Arrow.mk (X := tensorObj.{v, u} (𝒞 := inst) (X₁ □ X₂).left W) ((X₁ □ X₂).hom ▷ W)).hom ≫
        Iso.hom (α_ X₁.right X₂.right W))

Tactic:
simp