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