awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
j : J
_ : Membership.mem (γ := Finset J) Finset.univ j → (b.π j ≫ b.ι j) ≫ m = b.π j ≫ s.ι.app { as := j }
⊢ Membership.mem (γ := Finset J) Finset.univ j → (b.π j ≫ b.ι j) ≫ m = b.π j ≫ s.ι.app { as := j }

Tactic:
_
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
j : J
h_1 : Membership.mem (γ := Finset J) Finset.univ j
⊢ (b.π j ≫ b.ι j) ≫ m = b.π j ≫ s.ι.app { as := j }

Tactic:
simpa using b.π j ≫= h ⟨j⟩

Premises used: CategoryTheory.Limits.Bicone.π, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
i : b.IsBilimit
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := b.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
      ((∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (𝟙 b.pt ≫ b.toCone.π.app { as := as })
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
i : b.IsBilimit
as : J
⊢ Eq (α := b.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    ((∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (𝟙 b.pt ≫ b.toCone.π.app { as := as })

Tactic:
simp [sum_comp, b.ι_π, comp_dite]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
i : b.IsBilimit
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := b.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
      ((∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (𝟙 b.pt ≫ b.toCone.π.app { as := as })
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
classical
    cases j
    simp [sum_comp, b.ι_π, comp_dite]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
⊢ HasBiproduct.{u_1, v, u} f

Tactic:
HasBiproduct.mk
    { bicone := b
      isBilimit := isBilimitOfTotal b total }

Premises used: CategoryTheory.Limits.HasBiproduct.mk, CategoryTheory.Limits.isBilimitOfTotal, CategoryTheory.Limits.LimitBicone.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Bicone.{u_1, v, u} f
ht : IsLimit t.toCone
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := t.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
      ((∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app { as := as : Discrete J }) (𝟙 t.pt ≫ t.toCone.π.app { as := as })
⊢ (∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app j = 𝟙 t.pt ≫ t.toCone.π.app j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Bicone.{u_1, v, u} f
ht : IsLimit t.toCone
as : J
⊢ Eq (α := t.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    ((∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app { as := as : Discrete J }) (𝟙 t.pt ≫ t.toCone.π.app { as := as })

Tactic:
simp [sum_comp, t.ι_π, comp_dite]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Bicone.{u_1, v, u} f
ht : IsLimit t.toCone
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := t.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
      ((∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app { as := as : Discrete J }) (𝟙 t.pt ≫ t.toCone.π.app { as := as })
⊢ (∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app j = 𝟙 t.pt ≫ t.toCone.π.app j

Tactic:
classical
      cases j
      simp [sum_comp, t.ι_π, comp_dite]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Cone.{u_1, v, u_1, u} (Discrete.functor f)
ht : IsLimit t
⊢ ∀ (j : Discrete J), t.π.app j = Iso.hom (Iso.refl t.pt) ≫ (Bicone.toCone (Bicone.ofLimitCone ht)).π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Bicone.{u_1, v, u} f
ht : IsColimit t.toCocone
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ t.pt)
      (t.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, t.π j ≫ t.ι j)
      (t.toCocone.ι.app { as := as : Discrete J } ≫ 𝟙 t.pt)
⊢ t.toCocone.ι.app j ≫ ∑ j : J, t.π j ≫ t.ι j = t.toCocone.ι.app j ≫ 𝟙 t.pt

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Bicone.{u_1, v, u} f
ht : IsColimit t.toCocone
as : J
mk : (∑ x : J, if h : as = x then eqToHom ⋯ ≫ t.ι x else 0 ≫ t.ι x) = t.ι as ≫ 𝟙 t.pt
⊢ Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ t.pt)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, t.π j ≫ t.ι j)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ 𝟙 t.pt)

Tactic:
simp_rw [Bicone.toCocone_ι_app, comp_sum, ← Category.assoc, t.ι_π, dite_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Limits.Bicone.toCocone_ι_app, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Bicone.{u_1, v, u} f
ht : IsColimit t.toCocone
as : J
⊢ (∑ x : J, if h : as = x then eqToHom ⋯ ≫ t.ι x else 0 ≫ t.ι x) = t.ι as ≫ 𝟙 t.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Bicone.{u_1, v, u} f
ht : IsColimit t.toCocone
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ t.pt)
      (t.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, t.π j ≫ t.ι j)
      (t.toCocone.ι.app { as := as : Discrete J } ≫ 𝟙 t.pt)
mk₁ : ∀ (as : J), (∑ x : J, if h : as = x then eqToHom ⋯ ≫ t.ι x else 0 ≫ t.ι x) = t.ι as ≫ 𝟙 t.pt
⊢ t.toCocone.ι.app j ≫ ∑ j : J, t.π j ≫ t.ι j = t.toCocone.ι.app j ≫ 𝟙 t.pt

Tactic:
classical
      cases j
      simp_rw [Bicone.toCocone_ι_app, comp_sum, ← Category.assoc, t.ι_π, dite_comp]
      simp

Premises used: CategoryTheory.Category.assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Limits.Bicone.toCocone_ι_app, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
t : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
ht : IsColimit t
⊢ ∀ (j : Discrete J), t.ι.app j ≫ Iso.hom (Iso.refl t.pt) = (Bicone.toCocone (Bicone.ofColimitCocone ht)).ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Finite J
f : J → C
inst_3 : HasProduct.{u_1, v, u} f
intro : ∀ (val : Fintype J), HasBiproduct.{u_1, v, u} f
⊢ HasBiproduct.{u_1, v, u} f

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Finite J
f : J → C
inst_3 : HasProduct.{u_1, v, u} f
val : Fintype J
⊢ HasBiproduct.{u_1, v, u} f

Tactic:
HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.HasBiproduct.mk, CategoryTheory.Limits.Bicone.ofLimitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit, CategoryTheory.Limits.LimitBicone.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Finite J
f : J → C
inst_3 : HasProduct.{u_1, v, u} f
val : Fintype J
⊢ HasBiproduct.{u_1, v, u} f

Tactic:
exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.HasBiproduct.mk, CategoryTheory.Limits.Bicone.ofLimitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit, CategoryTheory.Limits.LimitBicone.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Finite J
f : J → C
inst_3 : HasCoproduct.{u_1, v, u} f
intro : ∀ (val : Fintype J), HasBiproduct.{u_1, v, u} f
⊢ HasBiproduct.{u_1, v, u} f

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Finite J
f : J → C
inst_3 : HasCoproduct.{u_1, v, u} f
val : Fintype J
⊢ HasBiproduct.{u_1, v, u} f

Tactic:
HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.HasBiproduct.mk, CategoryTheory.Limits.LimitBicone.mk, CategoryTheory.Limits.Bicone.ofColimitCocone, CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Finite J
f : J → C
inst_3 : HasCoproduct.{u_1, v, u} f
val : Fintype J
⊢ HasBiproduct.{u_1, v, u} f

Tactic:
exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.HasBiproduct.mk, CategoryTheory.Limits.LimitBicone.mk, CategoryTheory.Limits.Bicone.ofColimitCocone, CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
⊢ HasFiniteBiproducts.{v, u} C

Tactic:
⟨fun _ => { has_biproduct := fun _ => HasBiproduct.of_hasProduct _ }⟩

Premises used: CategoryTheory.Limits.HasBiproduct.of_hasProduct, CategoryTheory.Limits.HasFiniteBiproducts.mk, CategoryTheory.Limits.HasBiproductsOfShape.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
⊢ HasFiniteBiproducts.{v, u} C

Tactic:
⟨fun _ => { has_biproduct := fun _ => HasBiproduct.of_hasCoproduct _ }⟩

Premises used: CategoryTheory.Limits.HasFiniteBiproducts.mk, CategoryTheory.Limits.HasBiproduct.of_hasCoproduct, CategoryTheory.Limits.HasBiproductsOfShape.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
⊢ Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f) (∑ j : J, π f j ≫ ι f j) (𝟙 (biproduct.{0, v, u} f))

Tactic:
IsBilimit.total (biproduct.isBilimit _)

Premises used: CategoryTheory.Limits.biproduct.isBilimit, CategoryTheory.Limits.IsBilimit.total
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → T ⟶ f j
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift g) (π f j) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (∑ j : J, g j ≫ ι f j) (π f j)
⊢ Eq (α := T ⟶ biproduct.{0, v, u} f) (lift g) (∑ j : J, g j ≫ ι f j)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → T ⟶ f j
j : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift g) (π f j) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (∑ j : J, g j ≫ ι f j) (π f j)

Tactic:
simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]

Premises used: Finset.mem_univ, CategoryTheory.Category.assoc, if_true, CategoryTheory.Limits.comp_zero, CategoryTheory.Preadditive.sum_comp, CategoryTheory.eqToHom_refl, Finset.sum_dite_eq', CategoryTheory.Category.comp_id, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.lift_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → T ⟶ f j
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift g) (π f j) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (∑ j : J, g j ≫ ι f j) (π f j)
⊢ Eq (α := T ⟶ biproduct.{0, v, u} f) (lift g) (∑ j : J, g j ≫ ι f j)

Tactic:
classical
  ext j
  simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]

Premises used: Finset.mem_univ, CategoryTheory.Category.assoc, if_true, CategoryTheory.Limits.comp_zero, CategoryTheory.Preadditive.sum_comp, CategoryTheory.eqToHom_refl, Finset.sum_dite_eq', CategoryTheory.Category.comp_id, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.lift_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → f j ⟶ T
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc g) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (∑ j : J, π f j ≫ g j)
⊢ Eq (α := biproduct.{0, v, u} f ⟶ T) (desc g) (∑ j : J, π f j ≫ g j)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → f j ⟶ T
j : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc g) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (∑ j : J, π f j ≫ g j)

Tactic:
simp [comp_sum, biproduct.ι_π_assoc, dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → f j ⟶ T
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc g) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (∑ j : J, π f j ≫ g j)
⊢ Eq (α := biproduct.{0, v, u} f ⟶ T) (desc g) (∑ j : J, π f j ≫ g j)

Tactic:
classical
  ext j
  simp [comp_sum, biproduct.ι_π_assoc, dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift g) (desc h) = ∑ j : J, g j ≫ h j

Tactic:
simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
    dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Limits.biproduct.desc_eq, CategoryTheory.Limits.biproduct.lift_eq, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift g) (desc h) = ∑ j : J, g j ≫ h j

Tactic:
classical
  simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
    dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Limits.biproduct.desc_eq, CategoryTheory.Limits.biproduct.lift_eq, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
inst_3 : HasFiniteBiproducts.{v, u} C
f g : J → C
h : (j : J) → f j ⟶ g j
w :
  ∀ (j j_1 : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map h) (π g j)) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (∑ j : J, π f j ≫ h j ≫ ι g j) (π g j))
⊢ Eq (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) (map h) (∑ j : J, π f j ≫ h j ≫ ι g j)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
inst_3 : HasFiniteBiproducts.{v, u} C
f g : J → C
h : (j : J) → f j ⟶ g j
j j_1 : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map h) (π g j)) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (∑ j : J, π f j ≫ h j ≫ ι g j) (π g j))

Tactic:
simp [biproduct.ι_π, biproduct.ι_π_assoc, sum_comp, comp_dite, dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.dite_comp, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
inst_3 : HasFiniteBiproducts.{v, u} C
f g : J → C
h : (j : J) → f j ⟶ g j
w :
  ∀ (j j_1 : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map h) (π g j)) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (∑ j : J, π f j ≫ h j ≫ ι g j) (π g j))
⊢ Eq (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) (map h) (∑ j : J, π f j ≫ h j ≫ ι g j)

Tactic:
classical
  ext
  simp [biproduct.ι_π, biproduct.ι_π_assoc, sum_comp, comp_dite, dite_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.dite_comp, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
K : Type
inst_3 : Finite K
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
w :
  ∀ (j : K),
    CategoryStruct.comp (Y := biproduct.{0, v, u} g)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift x : P ⟶ biproduct.{0, v, u} f)
            (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) :
          P ⟶ biproduct.{0, v, u} g)
        (π g j : biproduct.{0, v, u} g ⟶ g j) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} g) (lift fun (k : K) ↦ ∑ j : J, x j ≫ m j k) (π g j)
⊢ Eq (α := P ⟶ biproduct.{0, v, u} g)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift x : P ⟶ biproduct.{0, v, u} f)
        (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) :
      P ⟶ biproduct.{0, v, u} g)
    (lift fun (k : K) ↦ ∑ j : J, x j ≫ m j k : P ⟶ biproduct.{0, v, u} g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type
inst_2 : Fintype J
K : Type
inst_3 : Finite K
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
j : K
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} g)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift x : P ⟶ biproduct.{0, v, u} f)
          (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) :
        P ⟶ biproduct.{0, v, u} g)
      (π g j : biproduct.{0, v, u} g ⟶ g j) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} g) (lift fun (k : K) ↦ ∑ j : J, x j ≫ m j k) (π g j)

Tactic:
simp [biproduct.lift_desc]

Premises used: CategoryTheory.Limits.biproduct.lift_desc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J K : Type
inst_2 : Finite J
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : Fintype K
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j : f j ⟶ biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
            (desc x : biproduct.{0, v, u} g ⟶ P) :
          biproduct.{0, v, u} f ⟶ P) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc fun (j : J) ↦ ∑ k : K, m j k ≫ x k)
⊢ Eq (α := biproduct.{0, v, u} f ⟶ P)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
        (desc x : biproduct.{0, v, u} g ⟶ P) :
      biproduct.{0, v, u} f ⟶ P)
    (desc fun (j : J) ↦ ∑ k : K, m j k ≫ x k : biproduct.{0, v, u} f ⟶ P)

Tactic:
ext