awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
slice_lhs :
  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 ≫ 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
⊢ 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

Tactic:
slice_lhs 4 5 => rw [← T.map_comp]

Premises used: CategoryTheory.Monad.toFunctor, CategoryTheory.Functor.map_comp
-- 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.μ.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
⊢ 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 ≫ 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

Tactic:
simp only [hom_inv_id_app, Functor.map_id, id_comp]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- 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.inv.app (F.obj X) ≫ T.map (i.inv.app X))
| T.map (i.inv.app (F.obj X)) ≫ T.map (T.map (i.inv.app X))

Tactic:
rw [← T.map_comp]

Premises used: CategoryTheory.Monad.toFunctor, CategoryTheory.Functor.map_comp
-- 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
slice_lhs :
  ((T.map (i.inv.app (F.obj X) ≫ T.map (i.inv.app X)) ≫ T.map (T.μ.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
⊢ T.map (i.inv.app (F.obj X)) ≫ T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.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

Tactic:
slice_lhs 1 2 => rw [← T.map_comp]

Premises used: CategoryTheory.Monad.toFunctor, CategoryTheory.Functor.map_comp
-- 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.μ.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
⊢ ((T.map (i.inv.app (F.obj X) ≫ T.map (i.inv.app X)) ≫ T.map (T.μ.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

Tactic:
simp only [Functor.map_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- 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
e_a :
  T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X) ≫ T.μ.app X ≫ i.hom.app X =
    T.μ.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X
⊢ T.map (i.inv.app (F.obj X)) ≫ T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.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

Tactic:
congr 1
-- 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
e_a :
  (T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X)) ≫ T.μ.app X = (T.μ.app (F.obj X) ≫ T.map (i.inv.app X)) ≫ T.μ.app X
⊢ T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X) ≫ T.μ.app X ≫ i.hom.app X =
    T.μ.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X

Tactic:
simp only [← Category.assoc, NatIso.cancel_natIso_hom_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatIso.cancel_natIso_hom_right
-- 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
e_a :
  (T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X)) ≫ T.μ.app X =
    ((T.toFunctor ⋙ T.toFunctor).map (i.inv.app X) ≫ T.μ.app (T.obj X)) ≫ T.μ.app X
⊢ (T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X)) ≫ T.μ.app X = (T.μ.app (F.obj X) ≫ T.map (i.inv.app X)) ≫ T.μ.app X

Tactic:
rw [← T.μ.naturality]

Premises used: CategoryTheory.Monad.μ, CategoryTheory.NatTrans.naturality
-- 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
⊢ (T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X)) ≫ T.μ.app X =
    ((T.toFunctor ⋙ T.toFunctor).map (i.inv.app X) ≫ T.μ.app (T.obj X)) ≫ T.μ.app X

Tactic:
simp [T.assoc X]

Premises used: CategoryTheory.Monad.assoc
-- 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.η.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X = 𝟙 (F.obj X)
⊢ (T.η ≫ i.hom).app (F.obj X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X = 𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (F.obj X))

Tactic:
simp only [Functor.id_obj, NatTrans.comp_app, comp_obj, NatTrans.hcomp_app, Category.assoc,
      hom_inv_id_app_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.hcomp_app, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.id_obj, CategoryTheory.NatTrans.comp_app
-- 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 : map (𝟭 C) (i.inv.app X) ≫ T.η.app (T.obj X)
| T.η.app (F.obj X) ≫ T.map (i.inv.app X)

Tactic:
rw [← T.η.naturality (i.inv.app X), ]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Monad.η, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- 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
slice_lhs : ((map (𝟭 C) (i.inv.app X) ≫ T.η.app (T.obj X)) ≫ T.μ.app X) ≫ i.hom.app X = 𝟙 (F.obj X)
⊢ T.η.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X = 𝟙 (F.obj X)

Tactic:
slice_lhs 1 2 => rw [← T.η.naturality (i.inv.app X), ]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Monad.η, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- 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
⊢ ((map (𝟭 C) (i.inv.app X) ≫ T.η.app (T.obj X)) ≫ T.μ.app X) ≫ i.hom.app X = 𝟙 (F.obj X)

Tactic:
simp
-- 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 :
  i.inv.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) 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 =
    𝟙 (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))
⊢ F.map ((T.η ≫ i.hom).app X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X = 𝟙 (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))

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

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.hcomp_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.NatTrans.naturality_assoc
-- 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 (T.η.app X ≫ i.hom.app X ≫ i.inv.app X)
| T.map (T.η.app X) ≫ T.map (i.hom.app X) ≫ T.map (i.inv.app X)

Tactic:
simp only [← T.map_comp]

Premises used: CategoryTheory.Monad.toFunctor, CategoryTheory.Functor.map_comp
-- 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
slice_lhs :
  i.inv.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ≫ (T.map (T.η.app X ≫ i.hom.app X ≫ i.inv.app X) ≫ T.μ.app X) ≫ i.hom.app X =
    𝟙 (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))
⊢ i.inv.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) 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 =
    𝟙 (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))

Tactic:
slice_lhs 2 4 =>
      simp only [← T.map_comp]

Premises used: CategoryTheory.Monad.toFunctor, CategoryTheory.Functor.map_comp
-- 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
⊢ i.inv.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ≫ (T.map (T.η.app X ≫ i.hom.app X ≫ i.inv.app X) ≫ T.μ.app X) ≫ i.hom.app X =
    𝟙 (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))

Tactic:
simp
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
simp :
  T.δ.app X ≫
      i.hom.app (T.obj X) ≫
        F.map (i.hom.app X) ≫
          F.map (i.inv.app X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
⊢ (i.inv ≫ T.δ ≫ i.hom ◫ i.hom).app X ≫ F.map ((i.inv ≫ T.δ ≫ i.hom ◫ i.hom).app X) =
    (i.inv ≫ T.δ ≫ i.hom ◫ i.hom).app X ≫ (i.inv ≫ T.δ ≫ i.hom ◫ i.hom).app (F.obj X)

Tactic:
simp only [comp_obj, NatTrans.comp_app, NatTrans.hcomp_app, Functor.map_comp, assoc,
      NatTrans.naturality_assoc, Functor.comp_map, 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.Functor.comp_map, 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
a : F.map (i.hom.app X ≫ i.inv.app X)
| F.map (i.hom.app X) ≫ F.map (i.inv.app X)

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
slice_lhs :
  T.δ.app X ≫
      i.hom.app (T.obj X) ≫
        ((F.map (i.hom.app X ≫ i.inv.app X) ≫ F.map (T.δ.app X)) ≫ F.map (i.hom.app (T.obj X))) ≫
          F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
⊢ T.δ.app X ≫
      i.hom.app (T.obj X) ≫
        F.map (i.hom.app X) ≫
          F.map (i.inv.app X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
slice_lhs 3 4 => rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
simp :
  T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
⊢ T.δ.app X ≫
      i.hom.app (T.obj X) ≫
        ((F.map (i.hom.app X ≫ i.inv.app X) ≫ F.map (T.δ.app X)) ≫ F.map (i.hom.app (T.obj X))) ≫
          F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
simp only [hom_inv_id_app, Functor.map_id, id_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
rw :
  T.δ.app X ≫
      T.map (T.δ.app X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.map (T.δ.app X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
⊢ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
rw [← i.hom.naturality_assoc, ← T.coassoc_assoc]

Premises used: CategoryTheory.Comonad.coassoc_assoc, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
simp :
  T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
⊢ T.δ.app X ≫
      T.map (T.δ.app X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.map (T.δ.app X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
simp only [NatTrans.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_assoc
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
e_a :
  F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) = F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
⊢ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
congr 3
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
⊢ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) = F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
simp only [← Functor.map_comp, i.hom.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
simp :
  i.inv.app X ≫ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (i.hom.app X) ≫ F.map (i.inv.app X) ≫ F.map (T.ε.app X) =
    𝟙 (F.obj X)
⊢ (i.inv ≫ T.δ ≫ i.hom ◫ i.hom).app X ≫ F.map ((i.inv ≫ T.ε).app X) = 𝟙 (F.obj X)

Tactic:
simp only [comp_obj, NatTrans.comp_app, NatTrans.hcomp_app, Functor.map_comp, assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.hcomp_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
slice_lhs :
  i.inv.app X ≫ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (i.hom.app X ≫ i.inv.app X) ≫ F.map (T.ε.app X) = 𝟙 (F.obj X)
⊢ i.inv.app X ≫ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (i.hom.app X) ≫ F.map (i.inv.app X) ≫ F.map (T.ε.app X) =
    𝟙 (F.obj X)

Tactic:
slice_lhs 4 5 => rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
simp : i.inv.app X ≫ T.δ.app X ≫ T.map (T.ε.app X) ≫ i.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) = 𝟙 (F.obj X)
⊢ i.inv.app X ≫ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (i.hom.app X ≫ i.inv.app X) ≫ F.map (T.ε.app X) = 𝟙 (F.obj X)

Tactic:
simp only [hom_inv_id_app, Functor.map_id, id_comp, ← i.hom.naturality]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
a : 𝟙 (T.obj X)
| T.δ.app X ≫ T.map (T.ε.app X)

Tactic:
rw [T.right_counit]

Premises used: CategoryTheory.Comonad.right_counit
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
slice_lhs : i.inv.app X ≫ 𝟙 (T.obj X) ≫ i.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) = 𝟙 (F.obj X)
⊢ i.inv.app X ≫ T.δ.app X ≫ T.map (T.ε.app X) ≫ i.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) = 𝟙 (F.obj X)

Tactic:
slice_lhs 2 3 => rw [T.right_counit]

Premises used: CategoryTheory.Comonad.right_counit
-- 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 : Comonad.{v₁, u₁} C
i : T.toFunctor ≅ F
X : C
⊢ i.inv.app X ≫ 𝟙 (T.obj X) ≫ i.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) = 𝟙 (F.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
inst_1 : IsIso T.μ
⊢ T.map (T.η.app X) = T.η.app (T.obj X)

Tactic:
simp [← cancel_mono (T.μ.app _)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Monad.μ, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
inst_1 : IsIso T.μ
h : IsSplitMono (T.η.app X)
⊢ T.η.app X ≫ retraction (T.η.app X) = 𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
inst_1 : IsIso T.μ
refine : ∀ (x : IsSplitMono (T.η.app X)), retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)
⊢ IsSplitMono (T.η.app X) ↔ IsIso (T.η.app X)

Tactic:
refine ⟨fun _ ↦ ⟨retraction (T.η.app X), by simp, ?_⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
inst_1 : IsIso T.μ
h : IsSplitMono (T.η.app X)
rw : retraction (T.η.app X) ≫ T.η.app X = T.map (𝟙 X)
rw₁ : retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X ≫ retraction (T.η.app X))
rw₂ : retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X) ≫ T.map (retraction (T.η.app X))
rw₃ : retraction (T.η.app X) ≫ T.η.app X = T.η.app (T.obj X) ≫ T.map (retraction (T.η.app X))
rw₄ rw₅ : retraction (T.η.app X) ≫ T.η.app X = retraction (T.η.app X) ≫ T.η.app X
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)

Tactic:
rw [← map_id, ← show T.η.app X ≫ retraction (T.η.app X) = 𝟙 X from IsSplitMono.id _,
    map_comp, T.map_unit_app X, ← T.unit_naturality]

Premises used: CategoryTheory.Monad.unit_naturality, CategoryTheory.Monad.map_unit_app, CategoryTheory.Functor.map_id, CategoryTheory.Monad.η, CategoryTheory.IsSplitMono.id, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
⊢ T.map (T.ε.app X) = T.ε.app (T.obj X)

Tactic:
simp [← cancel_epi (T.δ.app _)]

Premises used: CategoryTheory.Comonad.δ, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
h : IsSplitEpi (T.ε.app X)
⊢ section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
refine : ∀ (x : IsSplitEpi (T.ε.app X)), T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)
⊢ IsSplitEpi (T.ε.app X) ↔ IsIso (T.ε.app X)

Tactic:
refine ⟨fun _ ↦ ⟨section_ (T.ε.app X), ?_, by simp⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Monad.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
h : IsSplitEpi (T.ε.app X)
rw : T.ε.app X ≫ section_ (T.ε.app X) = T.map (𝟙 X)
rw₁ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X) ≫ T.ε.app X)
rw₂ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.map (T.ε.app X)
rw₃ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.ε.app (T.obj X)
rw₄ rw₅ : T.ε.app X ≫ section_ (T.ε.app X) = T.ε.app X ≫ section_ (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)

Tactic:
rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X),
    map_comp, T.map_counit_app X, T.counit_naturality]

Premises used: CategoryTheory.Comonad.counit_naturality, CategoryTheory.IsSplitEpi.id, CategoryTheory.Comonad.map_counit_app, CategoryTheory.Comonad.ε, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ topMap X ≫ π X = bottomMap X ≫ π X

Tactic:
Algebra.Hom.ext X.assoc.symm

Premises used: CategoryTheory.Monad.Algebra.assoc, CategoryTheory.Monad.Algebra.Hom.ext, Eq.symm