C : Type u₁
inst✝¹ : Category 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
C : Type u₁
inst✝¹ : Category 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
rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]
no goals
C : Type u₁
inst✝¹ : Category 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
simp
no goals
C : Type u₁
inst✝¹ : Category 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
aesop_cat