case intro
C : Type u
inst✝⁴ : Category C
inst✝³ : Preadditive C
J✝ : Type
inst✝² : Fintype J✝
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
val✝ : Fintype J
⊢ HasBiproduct f
C : Type u
inst✝⁴ : Category C
inst✝³ : Preadditive C
J✝ : Type
inst✝² : Fintype J✝
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
⊢ HasBiproduct f
cases nonempty_fintype J
no goals
case intro
C : Type u
inst✝⁴ : Category C
inst✝³ : Preadditive C
J✝ : Type
inst✝² : Fintype J✝
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
val✝ : Fintype J
⊢ HasBiproduct f
apply HasBiproduct.mk
  { bicone := _
    isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }