[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
X✝ Y✝ : Coalgebra (prodComonad X)
f : X✝ ⟶ Y✝
⊢ f.f ≫ ((fun A => Over.mk (A.a ≫ prod.fst)) Y✝).hom = ((fun A => Over.mk (A.a ≫ prod.fst)) X✝).hom
[PROOFSTEP]
rw [Over.mk_hom, ← f.h_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
X✝ Y✝ : Coalgebra (prodComonad X)
f : X✝ ⟶ Y✝
⊢ X✝.a ≫ (prodComonad X).toFunctor.map f.f ≫ prod.fst = ((fun A => Over.mk (A.a ≫ prod.fst)) X✝).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
X✝ Y✝ : Coalgebra (prodComonad X)
f : X✝ ⟶ Y✝
⊢ X✝.a ≫ prod.map (𝟙 X) f.f ≫ prod.fst = X✝.a ≫ prod.fst
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
A : Coalgebra (prodComonad X)
⊢ (((𝟭 (Coalgebra (prodComonad X))).obj A).a ≫
        (prodComonad X).toFunctor.map (Iso.refl ((𝟭 (Coalgebra (prodComonad X))).obj A).A).hom) ≫
      prod.fst =
    ((Iso.refl ((𝟭 (Coalgebra (prodComonad X))).obj A).A).hom ≫ ((coalgebraToOver X ⋙ overToCoalgebra X).obj A).a) ≫
      prod.fst
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
A : Coalgebra (prodComonad X)
⊢ (((𝟭 (Coalgebra (prodComonad X))).obj A).a ≫
        (prodComonad X).toFunctor.map (Iso.refl ((𝟭 (Coalgebra (prodComonad X))).obj A).A).hom) ≫
      prod.snd =
    ((Iso.refl ((𝟭 (Coalgebra (prodComonad X))).obj A).A).hom ≫ ((coalgebraToOver X ⋙ overToCoalgebra X).obj A).a) ≫
      prod.snd
[PROOFSTEP]
simpa using A.counit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
X✝ Y✝ : Algebra (coprodMonad X)
f : X✝ ⟶ Y✝
⊢ ((fun A => Under.mk (coprod.inl ≫ A.a)) X✝).hom ≫ f.f = ((fun A => Under.mk (coprod.inl ≫ A.a)) Y✝).hom
[PROOFSTEP]
rw [Under.mk_hom, Category.assoc, ← f.h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
X✝ Y✝ : Algebra (coprodMonad X)
f : X✝ ⟶ Y✝
⊢ coprod.inl ≫ (coprodMonad X).toFunctor.map f.f ≫ Y✝.a = ((fun A => Under.mk (coprod.inl ≫ A.a)) Y✝).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
X✝ Y✝ : Algebra (coprodMonad X)
f : X✝ ⟶ Y✝
⊢ coprod.inl ≫ coprod.map (𝟙 X) f.f ≫ Y✝.a = coprod.inl ≫ Y✝.a
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
A : Algebra (coprodMonad X)
⊢ coprod.inl ≫
      (coprodMonad X).toFunctor.map (Iso.refl ((𝟭 (Algebra (coprodMonad X))).obj A).A).hom ≫
        ((algebraToUnder X ⋙ underToAlgebra X).obj A).a =
    coprod.inl ≫ ((𝟭 (Algebra (coprodMonad X))).obj A).a ≫ (Iso.refl ((𝟭 (Algebra (coprodMonad X))).obj A).A).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
A : Algebra (coprodMonad X)
⊢ coprod.inr ≫
      (coprodMonad X).toFunctor.map (Iso.refl ((𝟭 (Algebra (coprodMonad X))).obj A).A).hom ≫
        ((algebraToUnder X ⋙ underToAlgebra X).obj A).a =
    coprod.inr ≫ ((𝟭 (Algebra (coprodMonad X))).obj A).a ≫ (Iso.refl ((𝟭 (Algebra (coprodMonad X))).obj A).A).hom
[PROOFSTEP]
simpa using A.unit.symm


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Monad C
⊢ MonoidalCategory.tensorHom (μ M) (𝟙 M.toFunctor) ≫ μ M =
    (MonoidalCategory.associator M.toFunctor M.toFunctor M.toFunctor).hom ≫
      MonoidalCategory.tensorHom (𝟙 M.toFunctor) (μ M) ≫ μ M
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u
inst✝ : Category.{v, u} C
M : Monad C
x✝ : C
⊢ NatTrans.app (MonoidalCategory.tensorHom (μ M) (𝟙 M.toFunctor) ≫ μ M) x✝ =
    NatTrans.app
      ((MonoidalCategory.associator M.toFunctor M.toFunctor M.toFunctor).hom ≫
        MonoidalCategory.tensorHom (𝟙 M.toFunctor) (μ M) ≫ μ M)
      x✝
[PROOFSTEP]
simp [M.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ M.X.map (NatTrans.app M.mul X) ≫ NatTrans.app M.mul X = NatTrans.app M.mul (M.X.obj X) ≫ NatTrans.app M.mul X
[PROOFSTEP]
rw [← NatTrans.hcomp_id_app, ← NatTrans.comp_app]
  -- Porting note: had to add this step:
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app ((M.mul ◫ 𝟙 M.X) ≫ M.mul) X = NatTrans.app M.mul (M.X.obj X) ≫ NatTrans.app M.mul X
[PROOFSTEP]
erw [M.mul_assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app ((MonoidalCategory.associator M.X M.X M.X).hom ≫ MonoidalCategory.tensorHom (𝟙 M.X) M.mul ≫ M.mul) X =
    NatTrans.app M.mul (M.X.obj X) ≫ NatTrans.app M.mul X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app M.one (M.X.obj X) ≫ NatTrans.app M.mul X = 𝟙 ((𝟭 C).obj (M.X.obj X))
[PROOFSTEP]
erw [← NatTrans.id_hcomp_app M.one, ← NatTrans.comp_app, M.mul_one]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app (MonoidalCategory.rightUnitor M.X).hom X = 𝟙 ((𝟭 C).obj (M.X.obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ M.X.map (NatTrans.app M.one X) ≫ NatTrans.app M.mul X = 𝟙 (M.X.obj ((𝟭 C).obj X))
[PROOFSTEP]
erw [← NatTrans.hcomp_id_app M.one, ← NatTrans.comp_app, M.one_mul]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app (MonoidalCategory.leftUnitor M.X).hom X = 𝟙 (M.X.obj ((𝟭 C).obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
⊢ ∀ (X_1 : C), NatTrans.app (η (ofMon X)) X_1 ≫ NatTrans.app (NatTrans.mk src✝.app) X_1 = NatTrans.app (η (ofMon Y)) X_1
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : Mon_ (C ⥤ C)
f : X✝ ⟶ Y
src✝ : X✝.X ⟶ Y.X := f.hom
X : C
⊢ NatTrans.app (η (ofMon X✝)) X ≫ NatTrans.app (NatTrans.mk src✝.app) X = NatTrans.app (η (ofMon Y)) X
[PROOFSTEP]
erw [← NatTrans.comp_app, f.one_hom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : Mon_ (C ⥤ C)
f : X✝ ⟶ Y
src✝ : X✝.X ⟶ Y.X := f.hom
X : C
⊢ NatTrans.app Y.one X = NatTrans.app (η (ofMon Y)) X
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
⊢ ∀ (X_1 : C),
    NatTrans.app (μ (ofMon X)) X_1 ≫ NatTrans.app (NatTrans.mk src✝.app) X_1 =
      ((ofMon X).toFunctor.map (NatTrans.app (NatTrans.mk src✝.app) X_1) ≫
          NatTrans.app (NatTrans.mk src✝.app) ((ofMon Y).toFunctor.obj X_1)) ≫
        NatTrans.app (μ (ofMon Y)) X_1
[PROOFSTEP]
intro Z
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
Z : C
⊢ NatTrans.app (μ (ofMon X)) Z ≫ NatTrans.app (NatTrans.mk src✝.app) Z =
    ((ofMon X).toFunctor.map (NatTrans.app (NatTrans.mk src✝.app) Z) ≫
        NatTrans.app (NatTrans.mk src✝.app) ((ofMon Y).toFunctor.obj Z)) ≫
      NatTrans.app (μ (ofMon Y)) Z
[PROOFSTEP]
erw [← NatTrans.comp_app, f.mul_hom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
Z : C
⊢ NatTrans.app (MonoidalCategory.tensorHom f.hom f.hom ≫ Y.mul) Z =
    ((ofMon X).toFunctor.map (NatTrans.app (NatTrans.mk src✝.app) Z) ≫
        NatTrans.app (NatTrans.mk src✝.app) ((ofMon Y).toFunctor.obj Z)) ≫
      NatTrans.app (μ (ofMon Y)) Z
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
Z : C
⊢ (NatTrans.app f.hom (X.X.obj Z) ≫ Y.X.map (NatTrans.app f.hom Z)) ≫ NatTrans.app Y.mul Z =
    ((ofMon X).toFunctor.map (NatTrans.app f.hom Z) ≫ NatTrans.app f.hom (Y.X.obj Z)) ≫ NatTrans.app Y.mul Z
[PROOFSTEP]
simp only [NatTrans.naturality, NatTrans.hcomp_app, assoc, NatTrans.comp_app, ofMon_μ]


[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


[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ Z✝ : Monad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ X✝.map h ≫ (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) Y =
    (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) X ≫ Z✝.map h
[PROOFSTEP]
rw [assoc, f.1.naturality_assoc, g.1.naturality]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝ : X✝ ⟶ Y✝
⊢ (𝟙 X✝ ≫ x✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (𝟙 X✝ ≫ x✝¹).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, id_comp]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝ : X✝ ⟶ Y✝
⊢ (x✝ ≫ 𝟙 Y✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (x✝¹ ≫ 𝟙 Y✝).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, comp_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
W✝ X✝ Y✝ Z✝ : Monad C
x✝² : W✝ ⟶ X✝
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ((x✝² ≫ x✝¹) ≫ x✝).app = (x✝² ≫ x✝¹ ≫ x✝).app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
W✝ X✝ Y✝ Z✝ : Monad C
x✝³ : W✝ ⟶ X✝
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app ((x✝³ ≫ x✝²) ≫ x✝¹).toNatTrans x✝ = NatTrans.app (x✝³ ≫ x✝² ≫ x✝¹).toNatTrans x✝
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ Z✝ : Comonad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ X✝.map h ≫ (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) Y =
    (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) X ≫ Z✝.map h
[PROOFSTEP]
rw [assoc, f.1.naturality_assoc, g.1.naturality]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝ : X✝ ⟶ Y✝
⊢ (𝟙 X✝ ≫ x✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (𝟙 X✝ ≫ x✝¹).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, id_comp]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝ : X✝ ⟶ Y✝
⊢ (x✝ ≫ 𝟙 Y✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (x✝¹ ≫ 𝟙 Y✝).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, comp_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G W✝ X✝ Y✝ Z✝ : Comonad C
x✝² : W✝ ⟶ X✝
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ((x✝² ≫ x✝¹) ≫ x✝).app = (x✝² ≫ x✝¹ ≫ x✝).app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G W✝ X✝ Y✝ Z✝ : Comonad C
x✝³ : W✝ ⟶ X✝
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app ((x✝³ ≫ x✝²) ≫ x✝¹).toNatTrans x✝ = NatTrans.app (x✝³ ≫ x✝² ≫ x✝¹).toNatTrans x✝
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ NatTrans.app (Monad.η N) X ≫ NatTrans.app f.inv X = NatTrans.app (Monad.η M) X
[PROOFSTEP]
simp [← f_η]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ NatTrans.app (Monad.μ N) X ≫ NatTrans.app f.inv X =
    (N.map (NatTrans.app f.inv X) ≫ NatTrans.app f.inv (M.obj X)) ≫ NatTrans.app (Monad.μ M) X
[PROOFSTEP]
rw [← NatIso.cancel_natIso_hom_right f]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ (NatTrans.app (Monad.μ N) X ≫ NatTrans.app f.inv X) ≫ NatTrans.app f.hom X =
    ((N.map (NatTrans.app f.inv X) ≫ NatTrans.app f.inv (M.obj X)) ≫ NatTrans.app (Monad.μ M) X) ≫ NatTrans.app f.hom X
[PROOFSTEP]
simp only [NatTrans.naturality, Iso.inv_hom_id_app, assoc, comp_id, f_μ, NatTrans.naturality_assoc,
  Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ NatTrans.app (Monad.μ N) X = N.map (𝟙 (N.obj X)) ≫ NatTrans.app (Monad.μ N) X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app f.inv X ≫ NatTrans.app (Comonad.ε M) X = NatTrans.app (Comonad.ε N) X
[PROOFSTEP]
simp [← f_ε]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app f.inv X ≫ NatTrans.app (Comonad.δ M) X =
    NatTrans.app (Comonad.δ N) X ≫ NatTrans.app f.inv (N.obj X) ≫ M.map (NatTrans.app f.inv X)
[PROOFSTEP]
rw [← NatIso.cancel_natIso_hom_left f]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app f.hom X ≫ NatTrans.app f.inv X ≫ NatTrans.app (Comonad.δ M) X =
    NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X ≫ NatTrans.app f.inv (N.obj X) ≫ M.map (NatTrans.app f.inv X)
[PROOFSTEP]
simp only [reassoc_of% (f_δ X), Iso.hom_inv_id_app_assoc, NatTrans.naturality_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app (Comonad.δ M) X =
    NatTrans.app (Comonad.δ M) X ≫ M.map (NatTrans.app f.hom X) ≫ M.map (NatTrans.app f.inv X)
[PROOFSTEP]
rw [← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app (Comonad.δ M) X = NatTrans.app (Comonad.δ M) X ≫ 𝟙 (M.obj (M.obj X))
[PROOFSTEP]
apply (comp_id _).symm
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X
f_μ :
  ∀ (X : C),
    NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
      (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X
⊢ (monadToFunctor C).mapIso (MonadIso.mk f) = f
[PROOFSTEP]
ext
[GOAL]
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X
f_μ :
  ∀ (X : C),
    NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
      (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X
x✝ : C
⊢ NatTrans.app ((monadToFunctor C).mapIso (MonadIso.mk f)).hom x✝ = NatTrans.app f.hom x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X
f_δ :
  ∀ (X : C),
    NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
      NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X)
⊢ (comonadToFunctor C).mapIso (ComonadIso.mk f) = f
[PROOFSTEP]
ext
[GOAL]
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X
f_δ :
  ∀ (X : C),
    NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
      NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X)
x✝ : C
⊢ NatTrans.app ((comonadToFunctor C).mapIso (ComonadIso.mk f)).hom x✝ = NatTrans.app f.hom x✝
[PROOFSTEP]
rfl


[GOAL]
J : Type v
inst✝ : Category.{v', v} J
F : J ⥤ Discrete PUnit
c s : Cone F
⊢ s.pt = c.pt
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝ : Category.{v', v} J
F : J ⥤ Discrete PUnit
c s : Cocone F
⊢ c.pt = s.pt
[PROOFSTEP]
simp