J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
f : Fin 0 → C
this : HasColimitsOfShape (Discrete (Fin 0)) C :=
  hasColimitsOfShape_of_equivalence (Discrete.equivalence finZeroEquiv'.symm)
⊢ HasCoproduct f
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
f : Fin 0 → C
⊢ HasCoproduct f
letI : HasColimitsOfShape (Discrete (Fin 0)) C :=
  hasColimitsOfShape_of_equivalence (Discrete.equivalence.{0} finZeroEquiv'.symm)
no goals
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
f : Fin 0 → C
this : HasColimitsOfShape (Discrete (Fin 0)) C :=
  hasColimitsOfShape_of_equivalence (Discrete.equivalence finZeroEquiv'.symm)
⊢ HasCoproduct f
infer_instance
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
f : Fin (n + 1) → C
this : ∀ (f : Fin n → C), HasCoproduct f
⊢ HasCoproduct f
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
f : Fin (n + 1) → C
⊢ HasCoproduct f
haveI := hasCoproduct_fin n
no goals
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
f : Fin (n + 1) → C
this : ∀ (f : Fin n → C), HasCoproduct f
⊢ HasCoproduct f
apply
  HasColimit.mk ⟨_, extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)⟩