J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasLimit K
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
⊢ HasFiniteProducts 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✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasProduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasProduct_fin n fun n_1 => K.obj { as := n_1 }
⊢ HasLimit K
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasLimit K
letI := hasProduct_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✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasProduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasProduct_fin n fun n_1 => K.obj { as := n_1 }
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ HasLimit K
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasProduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasProduct_fin n fun n_1 => K.obj { as := n_1 }
⊢ HasLimit K
let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := 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✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
this : HasProduct fun n_1 => K.obj { as := n_1 } := CategoryTheory.hasProduct_fin n fun n_1 => K.obj { as := n_1 }
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ HasLimit K
apply @hasLimitOfIso  _ _ _ _ _ _ this that