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
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
have 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))
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_mono (leftDistributor Y f).hom).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
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))
⊢ 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) 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: classical
  cases nonempty_fintype J
  apply (cancel_mono (leftDistributor Y f).hom).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 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
⊢ g = h
have 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
Tactic: apply (cancel_epi (α_ _ _ _).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 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
⊢ Iso.hom (α_ X Y (biproduct.{0, v_1, u_1} f)) ≫ g = Iso.hom (α_ X Y (biproduct.{0, v_1, u_1} f)) ≫ h
have 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
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 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
⊢ g = h
have 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))
Tactic: apply (cancel_mono (α_ _ _ _).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 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
⊢ g ≫ Iso.inv (α_ Y Z (biproduct.{0, v_1, u_1} f)) = h ≫ Iso.inv (α_ Y Z (biproduct.{0, v_1, u_1} f))
have 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
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
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
⊢ 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
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
⊢ g = h
have 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)
Tactic: apply (cancel_epi (rightDistributor f X).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
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
⊢ 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)
have 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)
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
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
⊢ g = h
have intro : ∀ (val : Fintype J), g = h
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_epi (rightDistributor f X).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
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
have 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)
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_epi (rightDistributor f X).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
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)
⊢ 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) (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: classical
  cases nonempty_fintype J
  apply (cancel_epi (rightDistributor f X).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
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
⊢ 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
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
⊢ g = h
have 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)
Tactic: apply (cancel_mono (rightDistributor f Y).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
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
⊢ 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)
have 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)
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
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
⊢ g = h
have intro : ∀ (val : Fintype J), g = h
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_mono (rightDistributor f Y).hom).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
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
have 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)
Tactic: classical
  cases nonempty_fintype J
  apply (cancel_mono (rightDistributor f Y).hom).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
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)
⊢ 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) (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: classical
  cases nonempty_fintype J
  apply (cancel_mono (rightDistributor f Y).hom).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
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
⊢ g = h
have 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
Tactic: apply (cancel_epi (α_ _ _ _).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
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
⊢ Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ g = Iso.inv (α_ (biproduct.{0, v_1, u_1} f) X Y) ≫ h
have 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
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
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
⊢ g = h
have 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)
Tactic: apply (cancel_mono (α_ _ _ _).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
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
⊢ g ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z) = h ≫ Iso.hom (α_ (biproduct.{0, v_1, u_1} f) Y Z)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
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 X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
⊢ ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃
have refine_1 : ((X₁ □ X₂) □ X₃).left ≅ (X₁ □ X₂ □ X₃).left
Tactic: refine Arrow.isoMk ?_ (α_ _ _ _) ?_