awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A A' A'' : T.Algebra
f : A ⟶ A'
g : A' ⟶ A''
⊢ (f ≫ g).f = f.f ≫ g.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A B : T.Algebra
h : A.A ≅ B.A
w : T.map h.hom ≫ B.a = A.a ≫ h.hom
rw : T.map (h.inv ≫ h.hom) ≫ B.a = B.a
⊢ T.map h.inv ≫ A.a = B.a ≫ h.inv

Tactic:
rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A B : T.Algebra
h : A.A ≅ B.A
w : T.map h.hom ≫ B.a = A.a ≫ h.hom
⊢ T.map (h.inv ≫ h.hom) ≫ B.a = B.a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ T.map (T.map f ≫ Y.a) ≫ Y.a = (T.free.obj X).a ≫ T.map f ≫ Y.a

Tactic:
simp [← Y.assoc, ← T.μ.naturality_assoc]

Premises used: CategoryTheory.Monad.Algebra.assoc, CategoryTheory.Monad.μ, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : T.free.obj X ⟶ Y
h :
  Algebra.Hom.f
      ((fun (f : X ⟶ T.forget.obj Y) ↦ { f := T.map f ≫ Y.a, h := ⋯ : (T.free.obj X).Hom Y })
        ((fun (f : T.free.obj X ⟶ Y) ↦ T.η.app X ≫ f.f) f)) =
    f.f
⊢ (fun (f : X ⟶ T.forget.obj Y) ↦ { f := T.map f ≫ Y.a, h := ⋯ : (T.free.obj X).Hom Y })
      ((fun (f : T.free.obj X ⟶ Y) ↦ T.η.app X ≫ f.f) f) =
    f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : T.free.obj X ⟶ Y
⊢ Algebra.Hom.f
      ((fun (f : X ⟶ T.forget.obj Y) ↦ { f := T.map f ≫ Y.a, h := ⋯ : (T.free.obj X).Hom Y })
        ((fun (f : T.free.obj X ⟶ Y) ↦ T.η.app X ≫ f.f) f)) =
    f.f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
dsimp : T.η.app X ≫ T.map f ≫ Y.a = f
⊢ (fun (f : T.free.obj X ⟶ Y) ↦ T.η.app X ≫ f.f)
      ((fun (f : X ⟶ T.forget.obj Y) ↦ { f := T.map f ≫ Y.a, h := ⋯ : (T.free.obj X).Hom Y }) f) =
    f

Tactic:
dsimp only [forget_obj]

Premises used: CategoryTheory.Monad.forget_obj
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
rw : Functor.map (𝟭 C) f ≫ 𝟙 Y.A = f
⊢ T.η.app X ≫ T.map f ≫ Y.a = f

Tactic:
rw [← T.η.naturality_assoc, Y.unit]

Premises used: CategoryTheory.Monad.η, CategoryTheory.Monad.Algebra.unit, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ Functor.map (𝟭 C) f ≫ 𝟙 Y.A = f

Tactic:
apply Category.comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A B : T.Algebra
f : A ⟶ B
inst_1 : IsIso f.f
⊢ T.map (inv f.f) ≫ A.a = B.a ≫ inv f.f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X Y : T.Algebra
f : X ⟶ Y
h : Epi f.f
⊢ Epi f

Tactic:
(forget T).epi_of_epi_map h

Premises used: CategoryTheory.Monad.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X Y : T.Algebra
f : X ⟶ Y
h : Mono f.f
⊢ Mono f

Tactic:
(forget T).mono_of_mono_map h

Premises used: CategoryTheory.Monad.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
⊢ T.forget.IsRightAdjoint

Tactic:
⟨T.free, ⟨T.adj⟩⟩

Premises used: CategoryTheory.Monad.adj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Monad.free
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T T₁ T₂ : Monad.{v₁, u₁} C
h : T₂ ⟶ T₁
A : T₁.Algebra
⊢ T₂.η.app A.A ≫ h.app A.A ≫ A.a = 𝟙 A.A

Tactic:
simp [A.unit]

Premises used: CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T T₁ T₂ : Monad.{v₁, u₁} C
h : T₂ ⟶ T₁
A : T₁.Algebra
⊢ T₂.μ.app A.A ≫ h.app A.A ≫ A.a = T₂.map (h.app A.A ≫ A.a) ≫ h.app A.A ≫ A.a

Tactic:
simp [A.assoc]

Premises used: CategoryTheory.Monad.Algebra.assoc
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T T₁ T₂ : Monad.{v₁, u₁} C
h : T₁ ≅ T₂
⊢ 𝟙 T₁ = h.hom ≫ h.inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T T₁ T₂ : Monad.{v₁, u₁} C
h : T₁ ≅ T₂
⊢ h.inv ≫ h.hom = 𝟙 T₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T₁ T₂ : Monad.{v₁, u₁} C
h : T₁ ⟶ T₂
⊢ algebraFunctorOfMonadHom h ⋙ T₁.forget = T₂.forget

Tactic:
rfl

Premises used: CategoryTheory.Monad.forget, CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X Y : G.Coalgebra
f g : X ⟶ Y
h : f.f = g.f
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.ext
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A A' A'' : G.Coalgebra
f : A ⟶ A'
g : A' ⟶ A''
⊢ Hom.comp f g = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A : G.Coalgebra
⊢ Hom.id A = 𝟙 A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A : G.Coalgebra
⊢ Hom.f (𝟙 A) = 𝟙 A.A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A A' A'' : G.Coalgebra
f : A ⟶ A'
g : A' ⟶ A''
⊢ (f ≫ g).f = f.f ≫ g.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A B : G.Coalgebra
h : A.A ≅ B.A
w : A.a ≫ G.map h.hom = h.hom ≫ B.a
rw : A.a ≫ G.map (h.hom ≫ h.inv) = A.a
⊢ B.a ≫ G.map h.inv = h.inv ≫ A.a

Tactic:
rw [h.eq_inv_comp, ← reassoc_of% w, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A B : G.Coalgebra
h : A.A ≅ B.A
w : A.a ≫ G.map h.hom = h.hom ≫ B.a
⊢ A.a ≫ G.map (h.hom ≫ h.inv) = A.a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
⊢ X.a ≫ G.map (X.a ≫ G.map f) = (X.a ≫ G.map f) ≫ (G.cofree.obj Y).a

Tactic:
simp [← Coalgebra.coassoc_assoc]

Premises used: CategoryTheory.Comonad.Coalgebra.coassoc_assoc
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
dsimp : (X.a ≫ G.map f) ≫ G.ε.app Y = f
⊢ (fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y)
      ((fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := ⋯ : X.Hom (G.cofree.obj Y) }) f) =
    f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
rw : X.a ≫ G.map f ≫ G.ε.app Y = f
rw₁ : X.a ≫ G.ε.app X.A ≫ Functor.map (𝟭 C) f = f
rw₂ : X.a ≫ G.ε.app X.A ≫ f = f
rw₃ rw₄ : f = f
⊢ (X.a ≫ G.map f) ≫ G.ε.app Y = f

Tactic:
rw [Category.assoc, G.ε.naturality, Functor.id_map, X.counit_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.id_map, CategoryTheory.Comonad.ε, CategoryTheory.NatTrans.naturality, CategoryTheory.Comonad.Coalgebra.counit_assoc
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
h :
  Coalgebra.Hom.f
      ((fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := ⋯ : X.Hom (G.cofree.obj Y) })
        ((fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y) g)) =
    g.f
⊢ (fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := ⋯ : X.Hom (G.cofree.obj Y) })
      ((fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y) g) =
    g

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
h : X.a ≫ G.map (g.f ≫ G.ε.app Y) = g.f
⊢ Coalgebra.Hom.f
      ((fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := ⋯ : X.Hom (G.cofree.obj Y) })
        ((fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y) g)) =
    g.f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
h : g.f ≫ 𝟙 (G.obj Y) = g.f
⊢ X.a ≫ G.map (g.f ≫ G.ε.app Y) = g.f

Tactic:
rw [Functor.map_comp, g.h_assoc, cofree_obj_a, Comonad.right_counit]

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.h_assoc, CategoryTheory.Comonad.cofree_obj_a, CategoryTheory.Comonad.right_counit, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ g.f ≫ 𝟙 (G.obj Y) = g.f

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A B : G.Coalgebra
f : A ⟶ B
inst_1 : IsIso f.f
rw : A.a ≫ G.map f.f ≫ G.map (inv f.f) = A.a
⊢ B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a

Tactic:
rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]

Premises used: CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.Comonad.Coalgebra.Hom.f, CategoryTheory.Comonad.Coalgebra.Hom.h_assoc
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A B : G.Coalgebra
f : A ⟶ B
inst_1 : IsIso f.f
⊢ A.a ≫ G.map f.f ≫ G.map (inv f.f) = A.a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X Y : G.Coalgebra
f : X ⟶ Y
h : Epi f.f
⊢ Epi f

Tactic:
(forget G).epi_of_epi_map h

Premises used: CategoryTheory.Comonad.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X Y : G.Coalgebra
f : X ⟶ Y
h : Mono f.f
⊢ Mono f

Tactic:
(forget G).mono_of_mono_map h

Premises used: CategoryTheory.Comonad.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
⊢ G.forget.IsLeftAdjoint

Tactic:
⟨_, ⟨G.adj⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Comonad.adj
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ f ≫ T.η.app Y = T.η.app X ≫ T.map f

Tactic:
T.η.naturality _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Monad.η
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ T.map (T.map f) ≫ T.μ.app Y = T.μ.app X ≫ T.map f

Tactic:
T.μ.naturality _

Premises used: CategoryTheory.Monad.μ, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ T.map f ≫ T.ε.app Y = T.ε.app X ≫ f

Tactic:
T.ε.naturality _

Premises used: CategoryTheory.Comonad.ε, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ T.map f ≫ T.δ.app Y = T.δ.app X ≫ T.map (T.map f)

Tactic:
T.δ.naturality _

Premises used: CategoryTheory.Comonad.δ, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T₁ T₂ : Monad.{v₁, u₁} C
f g : T₁ ⟶ T₂
h : f.app = g.app
⊢ f = g

Tactic:
MonadHom.ext h

Premises used: CategoryTheory.MonadHom.ext
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T₁ T₂ : Comonad.{v₁, u₁} C
f g : T₁ ⟶ T₂
h : f.app = g.app
⊢ f = g

Tactic:
ComonadHom.ext h

Premises used: CategoryTheory.ComonadHom.ext
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X_1 Y_1 Z : Monad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
rw₁ : f.app X ≫ Y_1.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
rw₂ rw₃ : f.app X ≫ g.app X ≫ Z.map h = f.app X ≫ g.app X ≫ Z.map h
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h

Tactic:
rw [assoc, f.1.naturality_assoc, g.1.naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.MonadHom.toNatTrans, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G X_1 Y_1 Z : Comonad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
rw₁ : f.app X ≫ Y_1.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
rw₂ rw₃ : f.app X ≫ g.app X ≫ Z.map h = f.app X ≫ g.app X ≫ Z.map h
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h

Tactic:
rw [assoc, f.1.naturality_assoc, g.1.naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.ComonadHom.toNatTrans, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
⊢ toNatTrans (𝟙 T) = 𝟙 T.toFunctor

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T₁ T₂ T₃ : Monad.{v₁, u₁} C
f : T₁ ⟶ T₂
g : T₂ ⟶ T₃
⊢ (f ≫ g).toNatTrans = f.toNatTrans ≫ g.toNatTrans

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, rfl
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
⊢ toNatTrans (𝟙 T) = 𝟙 T.toFunctor

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T₁ T₂ T₃ : Comonad.{v₁, u₁} C
f : T₁ ⟶ T₂
g : T₂ ⟶ T₃
⊢ (f ≫ g).toNatTrans = f.toNatTrans ≫ g.toNatTrans

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, rfl
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
⊢ N.η.app X ≫ f.inv.app X = M.η.app X

Tactic:
simp [← f_η]
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
rw : (N.μ.app X ≫ f.inv.app X) ≫ f.hom.app X = ((N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X) ≫ f.hom.app X
⊢ N.μ.app X ≫ f.inv.app X = (N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X

Tactic:
rw [← NatIso.cancel_natIso_hom_right f]

Premises used: CategoryTheory.NatIso.cancel_natIso_hom_right
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
simp : N.μ.app X = N.map (𝟙 (N.obj X)) ≫ N.μ.app X
⊢ (N.μ.app X ≫ f.inv.app X) ≫ f.hom.app X = ((N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X) ≫ f.hom.app X

Tactic:
simp only [NatTrans.naturality, Iso.inv_hom_id_app, assoc, comp_id, f_μ,
          NatTrans.naturality_assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
⊢ N.μ.app X = N.map (𝟙 (N.obj X)) ≫ N.μ.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ f.inv.app X ≫ M.ε.app X = N.ε.app X

Tactic:
simp [← f_ε]
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
rw : f.hom.app X ≫ f.inv.app X ≫ M.δ.app X = f.hom.app X ≫ N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)
⊢ f.inv.app X ≫ M.δ.app X = N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)

Tactic:
rw [← NatIso.cancel_natIso_hom_left f]

Premises used: CategoryTheory.NatIso.cancel_natIso_hom_left
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
simp : M.δ.app X = M.δ.app X ≫ M.map (f.hom.app X) ≫ M.map (f.inv.app X)
⊢ f.hom.app X ≫ f.inv.app X ≫ M.δ.app X = f.hom.app X ≫ N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)

Tactic:
simp only [reassoc_of% (f_δ X), Iso.hom_inv_id_app_assoc, NatTrans.naturality_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
rw : M.δ.app X = M.δ.app X ≫ 𝟙 (M.obj (M.obj X))
⊢ M.δ.app X = M.δ.app X ≫ M.map (f.hom.app X) ≫ M.map (f.inv.app X)

Tactic:
rw [← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ M.δ.app X = M.δ.app X ≫ 𝟙 (M.obj (M.obj X))

Tactic:
apply (comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
w : ∀ (x : C), NatTrans.app (Iso.hom (Functor.mapIso (monadToFunctor C) (MonadIso.mk f f_η f_μ))) x = f.hom.app x
⊢ Functor.mapIso (monadToFunctor C) (MonadIso.mk f f_η f_μ) = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
x : C
⊢ NatTrans.app (Iso.hom (Functor.mapIso (monadToFunctor C) (MonadIso.mk f f_η f_μ))) x = f.hom.app x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
w : ∀ (x : C), NatTrans.app (Iso.hom (Functor.mapIso (comonadToFunctor C) (ComonadIso.mk f f_ε f_δ))) x = f.hom.app x
⊢ Functor.mapIso (comonadToFunctor C) (ComonadIso.mk f f_ε f_δ) = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
x : C
⊢ NatTrans.app (Iso.hom (Functor.mapIso (comonadToFunctor C) (ComonadIso.mk f f_ε f_δ))) x = f.hom.app x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T_1 : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
T : Monad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
simp :
  T.map (i.inv.app (F.obj X)) ≫
      T.map (T.map (i.inv.app X)) ≫
        T.map (T.μ.app X) ≫ T.map (i.hom.app X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X =
    T.map (i.inv.app (F.obj X)) ≫ T.μ.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X
⊢ F.map (((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X =
    ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app (F.obj X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X

Tactic:
simp only [comp_obj, NatTrans.comp_app, NatTrans.hcomp_app, Category.assoc, Functor.map_comp,
      NatTrans.naturality_assoc, hom_inv_id_app_assoc, NatIso.cancel_natIso_inv_left]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.hcomp_app, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.NatIso.cancel_natIso_inv_left
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T_1 : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
T : Monad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
a : T.map (i.hom.app X ≫ i.inv.app X)
| T.map (i.hom.app X) ≫ T.map (i.inv.app X)

Tactic:
rw [← T.map_comp]

Premises used: CategoryTheory.Monad.toFunctor, CategoryTheory.Functor.map_comp