awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Finite J
f : J → C
X : C
j : J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (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) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (biproduct.ι f j ▷ X :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
have intro : ∀ (val : Fintype J),
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (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) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (biproduct.ι f j ▷ X :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
Tactic: cases nonempty_fintype J
-- 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 : Finite J
f : J → C
X : C
j : J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (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) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (biproduct.ι f j ▷ X :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
have intro : ∀ (val : Fintype J),
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (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) :
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
    (biproduct.ι f j ▷ X :
      tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X)
Tactic: classical
  cases nonempty_fintype J
  simp [rightDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc,
    dite_comp]
-- 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 : Finite J
f : J → C
X Y : C
val : Fintype J
j : J
⊢ Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) X) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) Y)
    (∑ x : J,
      (biproduct.π f x ▷ 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) (f j) X) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ▷ Y))
    (Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
      biproduct.π f j ▷ tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≫ Iso.inv (α_ (f j) X Y))
have intro : ∑ x : J,
    ((biproduct.π f x ⊗ₘ 𝟙 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) (f j) X) Y)
        (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) x ⊗ₘ 𝟙 Y)
        (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ⊗ₘ 𝟙 Y) =
  Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
    (biproduct.π f j ⊗ₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (f j) X Y)
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 : Finite J
f : J → C
X Y : C
val : Fintype J
j : J
⊢ ∑ x : J,
      ((biproduct.π f x ⊗ₘ 𝟙 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) (f j) X) Y)
          (biproduct.ι.{0, v_1, u_1} (C := C) (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) x ⊗ₘ 𝟙 Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) X) j ⊗ₘ 𝟙 Y) =
    Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
      (biproduct.π f j ⊗ₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (f j) X Y)
have intro : (∑ x : J, if h : x = j then (biproduct.π f x ⊗ₘ 𝟙 X) ≫ eqToHom sorry ⊗ₘ 𝟙 Y else (biproduct.π f x ⊗ₘ 𝟙 X) ≫ 0 ⊗ₘ 𝟙 Y) =
  Iso.hom (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫
    (biproduct.π f j ⊗ₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (f j) X Y)
Tactic: simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
-- 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 : 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,
      (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)))
have 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)))
Tactic: simp_rw [← tensorHom_id, ← 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
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,
      ((𝟙 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)))
have 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 sorry ⊗ₘ 𝟙 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 sorry) ≫ 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 only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite,
    dite_comp, tensor_dite, dite_tensor]
-- 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 : 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
⊢ g = h
have intro : ∀ (val : Fintype J), g = h
Tactic: cases nonempty_fintype J
-- 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 : 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
⊢ g = h
have 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)
Tactic: apply (cancel_epi (leftDistributor X f).inv).mp
-- 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 : 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
⊢ 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)
have 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)
Tactic: ext
-- 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 : 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
⊢ g = h
have intro : ∀ (val : Fintype J), g = h
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_epi (leftDistributor X f).inv).mp
  ext
  simp [w]
-- 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 : 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
have 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)
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_epi (leftDistributor X f).inv).mp
  ext
  simp [w]
-- 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 : 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)
⊢ g = h
have 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)
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_epi (leftDistributor X f).inv).mp
  ext
  simp [w]
-- 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 : 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
⊢ g = h
have intro : ∀ (val : Fintype J), g = h
Tactic: cases nonempty_fintype J
-- 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 : 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
⊢ g = h
have 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))
Tactic: apply (cancel_mono (leftDistributor Y f).hom).mp
-- 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 : 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
⊢ 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))
have 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))
Tactic: ext
-- 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 : 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
⊢ g = h
have intro : ∀ (val : Fintype J), g = h
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_mono (leftDistributor Y f).hom).mp
  ext
  simp [w]