awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.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)
have simp : M.δ.app X = M.δ.app X ≫ M.map (f.hom.app X) ≫ M.map (f.inv.app X)
Tactic: simp only [reassoc_of% (f_δ X), Iso.hom_inv_id_app_assoc, NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.map (f.hom.app X) ≫ M.map (f.inv.app X)
have rw : M.δ.app X = M.δ.app X ≫ 𝟙 (M.obj (M.obj X))
Tactic: rw [← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ Functor.mapIso (monadToFunctor C) (MonadIso.mk f f_η f_μ) = f
have w : ∀ (x : C), NatTrans.app (Iso.hom (Functor.mapIso (monadToFunctor C) (MonadIso.mk f f_η f_μ))) x = f.hom.app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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)
⊢ Functor.mapIso (comonadToFunctor C) (ComonadIso.mk f f_ε f_δ) = f
have w : ∀ (x : C), NatTrans.app (Iso.hom (Functor.mapIso (comonadToFunctor C) (ComonadIso.mk f f_ε f_δ))) x = f.hom.app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 (i.hom.app X) ≫ T.map (i.inv.app X)
have a : T.map (i.hom.app X ≫ i.inv.app X)
Tactic: rw [← T.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 (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
have 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
Tactic: slice_lhs 4 5 => rw [← T.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 (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
have 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
Tactic: simp only [hom_inv_id_app, Functor.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 (i.inv.app (F.obj X)) ≫ T.map (T.map (i.inv.app X))
have a : T.map (i.inv.app (F.obj X) ≫ T.map (i.inv.app X))
Tactic: rw [← T.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 (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
have 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
Tactic: slice_lhs 1 2 => rw [← T.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 (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
have 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
Tactic: simp only [Functor.map_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 (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
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 ≫ i.hom.app X =
    T.μ.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X
have 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
Tactic: simp only [← Category.assoc, NatIso.cancel_natIso_hom_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.μ.app (F.obj X) ≫ T.map (i.inv.app X)) ≫ T.μ.app X
have 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
Tactic: rw [← T.μ.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.η ≫ i.hom).app (F.obj X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X = 𝟙 (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (F.obj X))
have simp : T.η.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X = 𝟙 (F.obj X)
Tactic: simp only [Functor.id_obj, NatTrans.comp_app, comp_obj, NatTrans.hcomp_app, Category.assoc,
      hom_inv_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.η.app (F.obj X) ≫ T.map (i.inv.app X)
have a : map (𝟭 C) (i.inv.app X) ≫ T.η.app (T.obj X)
Tactic: rw [← T.η.naturality (i.inv.app X), ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.η.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X = 𝟙 (F.obj X)
have slice_lhs : ((map (𝟭 C) (i.inv.app X) ≫ T.η.app (T.obj X)) ≫ T.μ.app X) ≫ i.hom.app X = 𝟙 (F.obj X)
Tactic: slice_lhs 1 2 => rw [← T.η.naturality (i.inv.app X), ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ 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))
have 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))
Tactic: simp only [NatTrans.comp_app, Functor.map_comp, comp_obj, NatTrans.hcomp_app,
      Category.assoc, NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.η.app X) ≫ T.map (i.hom.app X) ≫ T.map (i.inv.app X)
have a : T.map (T.η.app X ≫ i.hom.app X ≫ i.inv.app X)
Tactic: simp only [← T.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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) ≫ 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))
have 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))
Tactic: slice_lhs 2 4 =>
      simp only [← T.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 ≫ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 X) ≫ F.map (i.inv.app X)
have a : F.map (i.hom.app X ≫ i.inv.app X)
Tactic: rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ 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))
have 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))
Tactic: slice_lhs 3 4 => rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ 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))
have 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))
Tactic: simp only [hom_inv_id_app, Functor.map_id, id_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ 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))
have 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))
Tactic: rw [← i.hom.naturality_assoc, ← T.coassoc_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ 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))
have 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))
Tactic: simp only [NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
⊢ 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))
have 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))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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 ≫ T.δ ≫ i.hom ◫ i.hom).app X ≫ F.map ((i.inv ≫ T.ε).app X) = 𝟙 (F.obj X)
have 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)
Tactic: simp only [comp_obj, NatTrans.comp_app, NatTrans.hcomp_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.δ.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)
have 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)
Tactic: slice_lhs 4 5 => rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.δ.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)
have 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)
Tactic: simp only [hom_inv_id_app, Functor.map_id, id_comp, ← i.hom.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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
| T.δ.app X ≫ T.map (T.ε.app X)
have a : 𝟙 (T.obj X)
Tactic: rw [T.right_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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.δ.app X ≫ T.map (T.ε.app X) ≫ i.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) = 𝟙 (F.obj X)
have slice_lhs : i.inv.app X ≫ 𝟙 (T.obj X) ≫ i.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) = 𝟙 (F.obj X)
Tactic: slice_lhs 2 3 => rw [T.right_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
inst_1 : IsIso T.μ
⊢ IsSplitMono (T.η.app X) ↔ IsIso (T.η.app X)
have refine : ∀ (x : IsSplitMono (T.η.app X)), retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)
Tactic: refine ⟨fun _ ↦ ⟨retraction (T.η.app X), by simp, ?_⟩, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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)
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)
have rw : retraction (T.η.app X) ≫ T.η.app X = T.map (𝟙 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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)
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)
have rw₁ : retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X ≫ retraction (T.η.app 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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))
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)
have rw₂ : retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X) ≫ T.map (retraction (T.η.app 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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))
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)
have rw₃ : retraction (T.η.app X) ≫ T.η.app X = T.η.app (T.obj X) ≫ T.map (retraction (T.η.app 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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))
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)
have rw₄ : retraction (T.η.app X) ≫ T.η.app X = retraction (T.η.app X) ≫ T.η.app 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : C
inst_1 : IsIso T.δ
⊢ IsSplitEpi (T.ε.app X) ↔ IsIso (T.ε.app X)
have refine : ∀ (x : IsSplitEpi (T.ε.app X)), T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)
Tactic: refine ⟨fun _ ↦ ⟨section_ (T.ε.app X), ?_, by simp⟩, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)
have rw : T.ε.app X ≫ section_ (T.ε.app X) = T.map (𝟙 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
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)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)
have rw₁ : T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X) ≫ T.ε.app 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]