[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ X.left = Y.left
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.left = X.left
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).left = eqToHom (_ : X.left = Y.left)
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom (_ : X = X)).left = eqToHom (_ : X.left = X.left)
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ X.right = Y.right
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.right = X.right
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).right = eqToHom (_ : X.right = Y.right)
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom (_ : X = X)).right = eqToHom (_ : X.right = X.right)
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : autoParam (L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) _auto✝
⊢ L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv
[PROOFSTEP]
rw [← L₁.mapIso_inv l, Iso.inv_comp_eq, L₁.mapIso_hom, ← Category.assoc, h, Category.assoc, ← R₁.map_comp]
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : autoParam (L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) _auto✝
⊢ X.hom = X.hom ≫ R₁.map (r.hom ≫ r.inv)
[PROOFSTEP]
simp
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
l l' : L₁ ⟶ L₂
h : l = l'
X : Comma L₂ R
⊢ L₁.map (Iso.refl ((mapLeft R l).obj X).left).hom ≫ ((mapLeft R l').obj X).hom =
    ((mapLeft R l).obj X).hom ≫ R.map (Iso.refl ((mapLeft R l).obj X).right).hom
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
l l' : L₁ ⟶ L₂
h : l = l'
⊢ ∀ {X Y : Comma L₂ R} (f : X ⟶ Y),
    (mapLeft R l).map f ≫
        ((fun X => isoMk (Iso.refl ((mapLeft R l).obj X).left) (Iso.refl ((mapLeft R l).obj X).right)) Y).hom =
      ((fun X => isoMk (Iso.refl ((mapLeft R l).obj X).left) (Iso.refl ((mapLeft R l).obj X).right)) X).hom ≫
        (mapLeft R l').map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
r r' : R₁ ⟶ R₂
h : r = r'
X : Comma L R₁
⊢ L.map (Iso.refl ((mapRight L r).obj X).left).hom ≫ ((mapRight L r').obj X).hom =
    ((mapRight L r).obj X).hom ≫ R₂.map (Iso.refl ((mapRight L r).obj X).right).hom
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
r r' : R₁ ⟶ R₂
h : r = r'
⊢ ∀ {X Y : Comma L R₁} (f : X ⟶ Y),
    (mapRight L r).map f ≫
        ((fun X => isoMk (Iso.refl ((mapRight L r).obj X).left) (Iso.refl ((mapRight L r).obj X).right)) Y).hom =
      ((fun X => isoMk (Iso.refl ((mapRight L r).obj X).left) (Iso.refl ((mapRight L r).obj X).right)) X).hom ≫
        (mapRight L r').map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝¹ : Category.{v₄, u₄} C
D : Type u₅
inst✝ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma (F ⋙ L) R
f : X✝ ⟶ Y✝
⊢ L.map (F.map f.left) ≫ ((fun X => { left := F.obj X.left, right := X.right, hom := X.hom }) Y✝).hom =
    ((fun X => { left := F.obj X.left, right := X.right, hom := X.hom }) X✝).hom ≫ R.map f.right
[PROOFSTEP]
simpa using f.w
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
inst✝ : Faithful F
X Y : Comma (F ⋙ L) R
f g : X ⟶ Y
h : (preLeft F L R).map f = (preLeft F L R).map g
⊢ f.right = g.right
[PROOFSTEP]
apply congrArg CommaMorphism.right h
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
inst✝ : Full F
X Y : Comma (F ⋙ L) R
f : (preLeft F L R).obj X ⟶ (preLeft F L R).obj Y
⊢ (F ⋙ L).map (F.preimage f.left) ≫ Y.hom = X.hom ≫ R.map f.right
[PROOFSTEP]
simpa using f.w
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
inst✝ : EssSurj F
Y : Comma L R
⊢ L.map (Functor.objObjPreimageIso F Y.left).hom ≫ Y.hom =
    ((preLeft F L R).obj
          { left := Functor.objPreimage F Y.left, right := Y.right,
            hom := (L.mapIso (Functor.objObjPreimageIso F Y.left)).hom ≫ Y.hom }).hom ≫
      R.map
        (Iso.refl
            ((preLeft F L R).obj
                { left := Functor.objPreimage F Y.left, right := Y.right,
                  hom := (L.mapIso (Functor.objObjPreimageIso F Y.left)).hom ≫ Y.hom }).right).hom
[PROOFSTEP]
simp
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
L : A ⥤ T
F : C ⥤ B
R : B ⥤ T
inst✝ : Faithful F
X Y : Comma L (F ⋙ R)
f g : X ⟶ Y
h : (preRight L F R).map f = (preRight L F R).map g
⊢ f.left = g.left
[PROOFSTEP]
apply congrArg CommaMorphism.left h
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
L : A ⥤ T
F : C ⥤ B
R : B ⥤ T
inst✝ : Full F
X Y : Comma L (F ⋙ R)
f : (preRight L F R).obj X ⟶ (preRight L F R).obj Y
⊢ L.map f.left ≫ Y.hom = X.hom ≫ (F ⋙ R).map (F.preimage f.right)
[PROOFSTEP]
simpa using f.w
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
L : A ⥤ T
F : C ⥤ B
R : B ⥤ T
inst✝ : EssSurj F
Y : Comma L R
⊢ L.map
        (Iso.refl
            ((preRight L F R).obj
                { left := Y.left, right := Functor.objPreimage F Y.right,
                  hom := Y.hom ≫ (R.mapIso (Functor.objObjPreimageIso F Y.right)).inv }).left).hom ≫
      Y.hom =
    ((preRight L F R).obj
          { left := Y.left, right := Functor.objPreimage F Y.right,
            hom := Y.hom ≫ (R.mapIso (Functor.objObjPreimageIso F Y.right)).inv }).hom ≫
      R.map (Functor.objObjPreimageIso F Y.right).hom
[PROOFSTEP]
simp [← R.map_comp]
[GOAL]
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝¹ : Category.{v₄, u₄} C
D : Type u₅
inst✝ : Category.{v₅, u₅} D
L : A ⥤ T
R : B ⥤ T
F : T ⥤ C
X✝ Y✝ : Comma L R
f : X✝ ⟶ Y✝
⊢ (L ⋙ F).map f.left ≫ ((fun X => { left := X.left, right := X.right, hom := F.map X.hom }) Y✝).hom =
    ((fun X => { left := X.left, right := X.right, hom := F.map X.hom }) X✝).hom ≫ (R ⋙ F).map f.right
[PROOFSTEP]
simp only [Functor.comp_map, ← F.map_comp, f.w]


[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
A B : Algebra T
h : A.A ≅ B.A
w : autoParam (T.map h.hom ≫ B.a = A.a ≫ h.hom) _auto✝
⊢ T.map h.inv ≫ A.a = B.a ≫ h.inv
[PROOFSTEP]
rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
A B : Algebra T
h : A.A ≅ B.A
w : autoParam (T.map h.hom ≫ B.a = A.a ≫ h.hom) _auto✝
⊢ T.map (h.inv ≫ h.hom) ≫ B.a = B.a
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : X ⟶ (forget T).obj Y
⊢ T.map (T.map f ≫ Y.a) ≫ Y.a = ((free T).obj X).a ≫ T.map f ≫ Y.a
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : X ⟶ (forget T).obj Y
⊢ T.map (T.map f ≫ Y.a) ≫ Y.a = NatTrans.app (μ T) X ≫ T.map f ≫ Y.a
[PROOFSTEP]
simp [← Y.assoc, ← T.μ.naturality_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : (free T).obj X ⟶ Y
⊢ (fun f => Algebra.Hom.mk (T.map f ≫ Y.a)) ((fun f => NatTrans.app (η T) X ≫ f.f) f) = f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : (free T).obj X ⟶ Y
⊢ ((fun f => Algebra.Hom.mk (T.map f ≫ Y.a)) ((fun f => NatTrans.app (η T) X ≫ f.f) f)).f = f.f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : (free T).obj X ⟶ Y
⊢ T.map (NatTrans.app (η T) X ≫ f.f) ≫ Y.a = f.f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : X ⟶ (forget T).obj Y
⊢ (fun f => NatTrans.app (η T) X ≫ f.f) ((fun f => Algebra.Hom.mk (T.map f ≫ Y.a)) f) = f
[PROOFSTEP]
dsimp only [forget_obj]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : X ⟶ (forget T).obj Y
⊢ NatTrans.app (η T) X ≫ T.map f ≫ Y.a = f
[PROOFSTEP]
rw [← T.η.naturality_assoc, Y.unit]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : Algebra T
f : X ⟶ (forget T).obj Y
⊢ (𝟭 C).map f ≫ 𝟙 Y.A = f
[PROOFSTEP]
apply Category.comp_id
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : Algebra T
f : A ⟶ B
inst✝ : IsIso f.f
⊢ T.map (inv f.f) ≫ A.a = B.a ≫ inv f.f
[PROOFSTEP]
rw [IsIso.eq_comp_inv f.f, Category.assoc, ← f.h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : Algebra T
f : A ⟶ B
inst✝ : IsIso f.f
⊢ T.map (inv f.f) ≫ T.map f.f ≫ B.a = B.a
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : Algebra T
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ Algebra.Hom.mk (inv f.f) = 𝟙 A ∧ Algebra.Hom.mk (inv f.f) ≫ f = 𝟙 B
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₂ ⟶ T₁
A : Algebra T₁
⊢ NatTrans.app (η T₂) A.A ≫ NatTrans.app h.toNatTrans A.A ≫ A.a = 𝟙 A.A
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₂ ⟶ T₁
A : Algebra T₁
⊢ NatTrans.app (η T₂) A.A ≫ NatTrans.app h.toNatTrans A.A ≫ A.a = 𝟙 A.A
[PROOFSTEP]
simp [A.unit]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₂ ⟶ T₁
A : Algebra T₁
⊢ NatTrans.app (μ T₂) A.A ≫ NatTrans.app h.toNatTrans A.A ≫ A.a =
    T₂.map (NatTrans.app h.toNatTrans A.A ≫ A.a) ≫ NatTrans.app h.toNatTrans A.A ≫ A.a
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₂ ⟶ T₁
A : Algebra T₁
⊢ NatTrans.app (μ T₂) A.A ≫ NatTrans.app h.toNatTrans A.A ≫ A.a =
    T₂.map (NatTrans.app h.toNatTrans A.A ≫ A.a) ≫ NatTrans.app h.toNatTrans A.A ≫ A.a
[PROOFSTEP]
simp [A.assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₁ ≅ T₂
⊢ 𝟙 T₁ = h.hom ≫ h.inv
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₁ ≅ T₂
⊢ h.inv ≫ h.hom = 𝟙 T₂
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
A B : Coalgebra G
h : A.A ≅ B.A
w : autoParam (A.a ≫ G.map h.hom = h.hom ≫ B.a) _auto✝
⊢ B.a ≫ G.map h.inv = h.inv ≫ A.a
[PROOFSTEP]
rw [h.eq_inv_comp, ← reassoc_of% w, ← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
A B : Coalgebra G
h : A.A ≅ B.A
w : autoParam (A.a ≫ G.map h.hom = h.hom ≫ B.a) _auto✝
⊢ A.a ≫ G.map (h.hom ≫ h.inv) = A.a
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
f : (forget G).obj X ⟶ Y
⊢ X.a ≫ G.map (X.a ≫ G.map f) = (X.a ≫ G.map f) ≫ ((cofree G).obj Y).a
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
f : (forget G).obj X ⟶ Y
⊢ X.a ≫ G.map (X.a ≫ G.map f) = (X.a ≫ G.map f) ≫ NatTrans.app (δ G) Y
[PROOFSTEP]
simp [← Coalgebra.coassoc_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
f : (forget G).obj X ⟶ Y
⊢ (fun g => g.f ≫ NatTrans.app (ε G) Y) ((fun f => Coalgebra.Hom.mk (X.a ≫ G.map f)) f) = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
f : (forget G).obj X ⟶ Y
⊢ (X.a ≫ G.map f) ≫ NatTrans.app (ε G) Y = f
[PROOFSTEP]
rw [Category.assoc, G.ε.naturality, Functor.id_map, X.counit_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
g : X ⟶ (cofree G).obj Y
⊢ (fun f => Coalgebra.Hom.mk (X.a ≫ G.map f)) ((fun g => g.f ≫ NatTrans.app (ε G) Y) g) = g
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
g : X ⟶ (cofree G).obj Y
⊢ ((fun f => Coalgebra.Hom.mk (X.a ≫ G.map f)) ((fun g => g.f ≫ NatTrans.app (ε G) Y) g)).f = g.f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
g : X ⟶ (cofree G).obj Y
⊢ X.a ≫ G.map (g.f ≫ NatTrans.app (ε G) Y) = g.f
[PROOFSTEP]
rw [Functor.map_comp, g.h_assoc, cofree_obj_a, Comonad.right_counit]
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : Coalgebra G
Y : C
g : X ⟶ (cofree G).obj Y
⊢ g.f ≫ 𝟙 (G.obj Y) = g.f
[PROOFSTEP]
apply comp_id
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : Coalgebra G
f : A ⟶ B
inst✝ : IsIso f.f
⊢ B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a
[PROOFSTEP]
rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : Coalgebra G
f : A ⟶ B
inst✝ : IsIso f.f
⊢ A.a ≫ G.map f.f ≫ G.map (inv f.f) = A.a
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : Coalgebra G
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ Coalgebra.Hom.mk (inv f.f) = 𝟙 A ∧ Coalgebra.Hom.mk (inv f.f) ≫ f = 𝟙 B
[PROOFSTEP]
aesop_cat