no goals
α : 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
rw [finite_colimit_eq_finset_univ_sup (pair x y)]
no goals
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ x ⊔ (y ⊔ ⊥) = x ⊔ y
rw [sup_bot_eq]