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 : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasColimit K
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
⊢ HasFiniteCoproducts C
refine' ⟨fun n => ⟨fun K => _⟩⟩
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 : ℕ
K : Discrete (Fin n) ⥤ C
this : HasCoproduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasCoproduct_fin n fun n_1 => K.obj { as := n_1 }
⊢ HasColimit K
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 : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasColimit K
letI := hasCoproduct_fin n fun n => K.obj ⟨n⟩
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 : ℕ
K : Discrete (Fin n) ⥤ C
this : HasCoproduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasCoproduct_fin n fun n_1 => K.obj { as := n_1 }
that : K ≅ Discrete.functor fun n_1 => K.obj { as := n_1 } :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl (K.obj { as := i })
⊢ HasColimit K
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 : ℕ
K : Discrete (Fin n) ⥤ C
this : HasCoproduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasCoproduct_fin n fun n_1 => K.obj { as := n_1 }
⊢ HasColimit K
let that : K ≅ Discrete.functor fun n => K.obj ⟨n⟩ := Discrete.natIso fun ⟨i⟩ => Iso.refl _
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 : ℕ
K : Discrete (Fin n) ⥤ C
this : HasCoproduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasCoproduct_fin n fun n_1 => K.obj { as := n_1 }
that : K ≅ Discrete.functor fun n_1 => K.obj { as := n_1 } :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl (K.obj { as := i })
⊢ HasColimit K
apply @hasColimitOfIso _ _ _ _ _ _ this that