[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
