[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
⊢ HasLimitsOfShape (Discrete ι) C
[PROOFSTEP]
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasLimitsOfShape (Discrete ι) C
[PROOFSTEP]
haveI : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasLimitsOfShape (Discrete (Fin n)) C
⊢ HasLimitsOfShape (Discrete ι) C
[PROOFSTEP]
exact hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
⊢ HasColimitsOfShape (Discrete ι) C
[PROOFSTEP]
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape (Discrete ι) C
[PROOFSTEP]
haveI : HasColimitsOfShape (Discrete (Fin n)) C := HasFiniteCoproducts.out n
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasColimitsOfShape (Discrete (Fin n)) C
⊢ HasColimitsOfShape (Discrete ι) C
[PROOFSTEP]
exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
J : ℕ
⊢ HasColimitsOfShape (Discrete (Fin J)) C
[PROOFSTEP]
infer_instance
