[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ ∀ (J : Type) [𝒥 : SmallCategory J] [inst : FinCategory J], HasLimitsOfShape J α
[PROOFSTEP]
intro J 𝒥₁ 𝒥₂
[GOAL]
α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasLimitsOfShape J α
[PROOFSTEP]
exact { has_limit := fun F => HasLimit.mk (finiteLimitCone F) }
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ ∀ (J : Type) [𝒥 : SmallCategory J] [inst : FinCategory J], HasColimitsOfShape J α
[PROOFSTEP]
intro J 𝒥₁ 𝒥₂
[GOAL]
α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasColimitsOfShape J α
[PROOFSTEP]
exact { has_colimit := fun F => HasColimit.mk (finiteColimitCocone F) }
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ f = Finset.inf Fintype.elems f
[PROOFSTEP]
trans
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ f = ?m.27522
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.27522 = Finset.inf Fintype.elems f
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α
[PROOFSTEP]
exact (IsLimit.conePointUniqueUpToIso (limit.isLimit _) (finiteLimitCone (Discrete.functor f)).isLimit).to_eq
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ (finiteLimitCone (Discrete.functor f)).cone.pt = Finset.inf Fintype.elems f
[PROOFSTEP]
change Finset.univ.inf (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.inf f
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.inf Finset.univ (f ∘ ↑(Equiv.toEmbedding discreteEquiv)) = Finset.inf Fintype.elems f
[PROOFSTEP]
simp only [← Finset.inf_map, Finset.univ_map_equiv_to_embedding]
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.inf Finset.univ f = Finset.inf Fintype.elems f
[PROOFSTEP]
rfl
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = Finset.sup Fintype.elems f
[PROOFSTEP]
trans
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = ?m.38444
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.38444 = Finset.sup Fintype.elems f
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α
[PROOFSTEP]
exact
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (finiteColimitCocone (Discrete.functor f)).isColimit).to_eq
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ (finiteColimitCocone (Discrete.functor f)).cocone.pt = Finset.sup Fintype.elems f
[PROOFSTEP]
change Finset.univ.sup (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.sup f
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.sup Finset.univ (f ∘ ↑(Equiv.toEmbedding discreteEquiv)) = Finset.sup Fintype.elems f
[PROOFSTEP]
simp only [← Finset.sup_map, Finset.univ_map_equiv_to_embedding]
[GOAL]
α : Type u
J : Type w
inst✝⁴ : SmallCategory J
inst✝³ : FinCategory J
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.sup Finset.univ f = Finset.sup Fintype.elems f
[PROOFSTEP]
rfl
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ HasBinaryProducts α
[PROOFSTEP]
have : ∀ x y : α, HasLimit (pair x y) :=
  by
  letI := hasFiniteLimits_of_hasFiniteLimits_of_size.{u} α
  infer_instance
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ ∀ (x y : α), HasLimit (pair x y)
[PROOFSTEP]
letI := hasFiniteLimits_of_hasFiniteLimits_of_size.{u} α
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
this : (∀ (J : Type u) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J α) → HasFiniteLimits α :=
  hasFiniteLimits_of_hasFiniteLimits_of_size α
⊢ ∀ (x y : α), HasLimit (pair x y)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
this : ∀ (x y : α), HasLimit (pair x y)
⊢ HasBinaryProducts α
[PROOFSTEP]
apply hasBinaryProducts_of_hasLimit_pair
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y : α
⊢ limit (pair x y) = Finset.inf Finset.univ (pair x y).toPrefunctor.obj
[PROOFSTEP]
rw [finite_limit_eq_finset_univ_inf (pair.{u} x y)]
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y : α
⊢ x ⊓ (y ⊓ ⊤) = x ⊓ y
[PROOFSTEP]
rw [inf_top_eq]
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ HasBinaryCoproducts α
[PROOFSTEP]
have : ∀ x y : α, HasColimit (pair x y) :=
  by
  letI := hasFiniteColimits_of_hasFiniteColimits_of_size.{u} α
  infer_instance
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ ∀ (x y : α), HasColimit (pair x y)
[PROOFSTEP]
letI := hasFiniteColimits_of_hasFiniteColimits_of_size.{u} α
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
this : (∀ (J : Type u) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J α) → HasFiniteColimits α :=
  hasFiniteColimits_of_hasFiniteColimits_of_size α
⊢ ∀ (x y : α), HasColimit (pair x y)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
this : ∀ (x y : α), HasColimit (pair x y)
⊢ HasBinaryCoproducts α
[PROOFSTEP]
apply hasBinaryCoproducts_of_hasColimit_pair
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ colimit (pair x y) = Finset.sup Finset.univ (pair x y).toPrefunctor.obj
[PROOFSTEP]
rw [finite_colimit_eq_finset_univ_sup (pair x y)]
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ x ⊔ (y ⊔ ⊥) = x ⊔ y
[PROOFSTEP]
rw [sup_bot_eq]
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ limit (cospan f g) = Finset.inf Finset.univ (cospan f g).toPrefunctor.obj
[PROOFSTEP]
rw [finite_limit_eq_finset_univ_inf]
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ z ⊓ (x ⊓ (y ⊓ ⊤)) = z ⊓ (x ⊓ y)
[PROOFSTEP]
rw [inf_top_eq]
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ colimit (span f g) = Finset.sup Finset.univ (span f g).toPrefunctor.obj
[PROOFSTEP]
rw [finite_colimit_eq_finset_univ_sup]
[GOAL]
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ z ⊔ (x ⊔ (y ⊔ ⊥)) = z ⊔ (x ⊔ y)
[PROOFSTEP]
rw [sup_bot_eq]
[GOAL]
α : Type u
inst✝¹ : CompleteLattice α
J : Type u
inst✝ : SmallCategory J
F : J ⥤ α
s : Cone F
⊢ ∀ (b : α), b ∈ Set.range F.obj → s.pt ≤ b
[PROOFSTEP]
rintro _ ⟨j, rfl⟩
[GOAL]
case intro
α : Type u
inst✝¹ : CompleteLattice α
J : Type u
inst✝ : SmallCategory J
F : J ⥤ α
s : Cone F
j : J
⊢ s.pt ≤ F.obj j
[PROOFSTEP]
exact (s.π.app j).le
[GOAL]
α : Type u
inst✝¹ : CompleteLattice α
J : Type u
inst✝ : SmallCategory J
F : J ⥤ α
s : Cocone F
⊢ ∀ (b : α), b ∈ Set.range F.obj → b ≤ s.pt
[PROOFSTEP]
rintro _ ⟨j, rfl⟩
[GOAL]
case intro
α : Type u
inst✝¹ : CompleteLattice α
J : Type u
inst✝ : SmallCategory J
F : J ⥤ α
s : Cocone F
j : J
⊢ F.obj j ≤ s.pt
[PROOFSTEP]
exact (s.ι.app j).le
