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 : Fintype J
X : C
f : J → C
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))
have w : 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))
      (biproduct.lift fun (j : J) ↦ X ◁ biproduct.π f 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))
  (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: dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
-- 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
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))
        (biproduct.lift fun (j : J) ↦ X ◁ biproduct.π f 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))
    (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))
have w : 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))
  (X ◁ biproduct.π 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))
Tactic: erw [biproduct.lift_π]
-- 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: classical
  ext
  dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
  erw [biproduct.lift_π]
  simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_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} (α :=
    (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 (biproduct.{0, v_1, u_1} f))
    (Iso.inv (leftDistributor X f) :
      (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 (biproduct.{0, v_1, u_1} f))
    (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ≫ X ◁ biproduct.ι f 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 (biproduct.{0, v_1, u_1} f))
have w : ∀ (j : J),
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (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) :
          (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 (biproduct.{0, v_1, u_1} f)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (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)
        (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ≫ X ◁ biproduct.ι 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))
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 : Fintype J
X : C
f : J → C
j : J
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (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) :
          (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 (biproduct.{0, v_1, u_1} f)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (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)
        (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ≫ X ◁ biproduct.ι 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))
have w : Eq.{v_1 + 1} (α :=
  tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
  (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)
      (biproduct.desc fun (j : J) ↦ X ◁ biproduct.ι 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))
  (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)
      (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ≫ X ◁ biproduct.ι 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))
Tactic: dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
-- 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} (α :=
    (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 (biproduct.{0, v_1, u_1} f))
    (Iso.inv (leftDistributor X f) :
      (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 (biproduct.{0, v_1, u_1} f))
    (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ≫ X ◁ biproduct.ι f 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 (biproduct.{0, v_1, u_1} f))
have w : ∀ (j : J),
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (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) :
          (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 (biproduct.{0, v_1, u_1} f)) :
      tensorObj.{v_1, u_1} (𝒞 := inst) X (f j) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
    (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)
        (∑ j : J, biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) j ≫ X ◁ biproduct.ι 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))
Tactic: classical
  ext
  dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
  simp only [Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp,
    Finset.sum_dite_eq, Finset.mem_univ, ite_true, eqToHom_refl, Category.id_comp,
    biproduct.ι_desc]
-- 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
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))
    (X ◁ biproduct.π 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))
have intro : ∀ (val : Fintype 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))
    (X ◁ biproduct.π 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))
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 : C
f : J → C
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))
    (X ◁ biproduct.π 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))
have intro : ∀ (val : Fintype 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))
    (X ◁ biproduct.π 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))
Tactic: classical
  cases nonempty_fintype J
  simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, 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
j : J
⊢ Eq.{v_1 + 1} (α :=
    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))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.ι 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))
        (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)) :
      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))
    (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))
have intro : ∀ (val : Fintype J),
  Eq.{v_1 + 1} (α :=
    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))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.ι 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))
        (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)) :
      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))
    (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))
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 : C
f : J → C
j : J
⊢ Eq.{v_1 + 1} (α :=
    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))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.ι 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))
        (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)) :
      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))
    (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))
have intro : ∀ (val : Fintype J),
  Eq.{v_1 + 1} (α :=
    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))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f))
        (X ◁ biproduct.ι 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))
        (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)) :
      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))
    (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))
Tactic: classical
  cases nonempty_fintype J
  simp [leftDistributor_hom, Preadditive.comp_sum, ← whiskerLeft_comp_assoc,
    biproduct.ι_π, whiskerLeft_dite, dite_comp]