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 : C
f : J → C
Y : C
val : Fintype J
j : J
intro :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (∑ x : J,
      ((𝟙 X ⊗ₘ biproduct.π f x) ⊗ₘ 𝟙 Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst)
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ⊗ₘ 𝟙 Y))
    (∑ x : J,
      Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst) X
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
          (𝟙 X ⊗ₘ
            (biproduct.π f x ⊗ₘ 𝟙 Y) ≫
              biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) x)
          ((𝟙 X ⊗ₘ biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j) ≫ Iso.inv (α_ X (f j) Y)))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (∑ x : J,
      (X ◁ biproduct.π f x ⊗ₘ 𝟙 Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst)
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ▷ Y))
    (∑ x : J,
      Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst) X
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
          (𝟙 X ⊗ₘ
            biproduct.π f x ▷ Y ≫
              biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) x)
          (X ◁ biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j ≫ Iso.inv (α_ X (f j) Y)))

Tactic:
simp_rw [← tensorHom_id, ← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.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
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
X : C
f : J → C
Y : C
val : Fintype J
j : J
intro :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (∑ x : J, if h : x = j then (𝟙 X ⊗ₘ biproduct.π f x) ≫ eqToHom ⋯ ⊗ₘ 𝟙 Y else (𝟙 X ⊗ₘ biproduct.π f x) ≫ 0 ⊗ₘ 𝟙 Y)
    (∑ x : J,
      if h : x = j then
        Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫
          (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ eqToHom ⋯) ≫ Iso.inv (α_ X (f j) Y)
      else
        Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫ (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ 0) ≫ Iso.inv (α_ X (f j) Y))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (∑ x : J,
      ((𝟙 X ⊗ₘ biproduct.π f x) ⊗ₘ 𝟙 Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst)
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ⊗ₘ 𝟙 Y))
    (∑ x : J,
      Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst) X
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
          (𝟙 X ⊗ₘ
            (biproduct.π f x ⊗ₘ 𝟙 Y) ≫
              biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) x)
          ((𝟙 X ⊗ₘ biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) j) ≫ Iso.inv (α_ X (f j) Y)))

Tactic:
simp only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite,
    dite_comp, tensor_dite, dite_tensor]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_tensor_comp_assoc, CategoryTheory.dite_comp, CategoryTheory.MonoidalCategory.dite_tensor, CategoryTheory.MonoidalCategory.comp_tensor_id, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite, CategoryTheory.MonoidalCategory.tensor_dite
-- 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 : C
f : J → C
Y : C
val : Fintype J
j : J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (∑ x : J, if h : x = j then (𝟙 X ⊗ₘ biproduct.π f x) ≫ eqToHom ⋯ ⊗ₘ 𝟙 Y else (𝟙 X ⊗ₘ biproduct.π f x) ≫ 0 ⊗ₘ 𝟙 Y)
    (∑ x : J,
      if h : x = j then
        Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫
          (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ eqToHom ⋯) ≫ Iso.inv (α_ X (f j) Y)
      else
        Iso.hom (α_ X (biproduct.{0, v_1, u_1} f) Y) ≫ (𝟙 X ⊗ₘ (biproduct.π f x ⊗ₘ 𝟙 Y) ≫ 0) ≫ Iso.inv (α_ X (f j) Y))

Tactic:
simp
-- 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 : C
f : J → C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ Y
w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ 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
X Y : C
f : J → C
g h : tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f) ⟶ Y
w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h
val : Fintype J
intro :
  Eq (α := (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶ Y)
    (Iso.inv (leftDistributor X f) ≫ g :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶ Y)
    (Iso.inv (leftDistributor X f) ≫ h :
      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) ⟶ Y)
⊢ g = h

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

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

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

Premises used: nonempty_fintype, Iff.mp, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.leftDistributor
-- 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 : C
f : J → C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
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
X Y : C
f : J → C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
val : Fintype J
intro :
  Eq (α := X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
    (g ≫ Iso.hom (leftDistributor Y f) :
      X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
    (h ≫ Iso.hom (leftDistributor Y f) :
      X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
⊢ g = h

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

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

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
X Y : C
f : J → C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
val : Fintype J
j : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
      (g ≫ Iso.hom (leftDistributor Y f) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) =
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
      (h ≫ Iso.hom (leftDistributor Y f) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
      (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) j :
        (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) Y (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
X Y : C
f : J → C
g h : X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) Y (biproduct.{0, v_1, u_1} f)
w : ∀ (j : J), g ≫ Y ◁ biproduct.π f j = h ≫ Y ◁ biproduct.π f j
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) Y (f j))
      (g ≫ Iso.hom (leftDistributor Y f) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
      (h ≫ Iso.hom (leftDistributor Y f) :
        X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
intro₂ :
  ∀ (val : Fintype J) (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
        (g ≫ Iso.hom (leftDistributor Y f) :
          X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) =
      CategoryStruct.comp (Y := biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
        (h ≫ Iso.hom (leftDistributor Y f) :
          X ⟶ biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) j :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j)) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) Y (f j))
⊢ g = h

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

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

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

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

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

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, 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
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
w₁ :
  ∀ (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
⊢ g ≫ Iso.inv (α_ Y Z (biproduct.{0, v_1, u_1} f)) = h ≫ Iso.inv (α_ Y Z (biproduct.{0, v_1, u_1} f))

Tactic:
ext