[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
