J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
f : Fin 0 → C
this : HasLimitsOfShape (Discrete (Fin 0)) C :=
  hasLimitsOfShape_of_equivalence (Discrete.equivalence finZeroEquiv'.symm)
⊢ HasProduct f
J : Type v
inst✝⁴ : SmallCategory J
C : Type u
inst✝³ : Category C
D : Type u'
inst✝² : Category D
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
f : Fin 0 → C
⊢ HasProduct f
letI : HasLimitsOfShape (Discrete (Fin 0)) C :=
  hasLimitsOfShape_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✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
f : Fin 0 → C
this : HasLimitsOfShape (Discrete (Fin 0)) C :=
  hasLimitsOfShape_of_equivalence (Discrete.equivalence finZeroEquiv'.symm)
⊢ HasProduct f
infer_instance
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 : ℕ
f : Fin (n + 1) → C
this : ∀ (f : Fin n → C), HasProduct f
⊢ HasProduct f
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 : ℕ
f : Fin (n + 1) → C
⊢ HasProduct f
haveI := hasProduct_fin n
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 : ℕ
f : Fin (n + 1) → C
this : ∀ (f : Fin n → C), HasProduct f
⊢ HasProduct f
apply HasLimit.mk ⟨_, extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)⟩