awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
⊢ s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A

Tactic:
have h₂ : s.pt.a ≫ (T : C ⥤ C).map s.ι.f = s.ι.f ≫ T.δ.app X.A := s.ι.h
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
refine_1 : s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ (beckCoalgebraFork X).pt.a
refine_2 : { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ : s.pt.Hom (beckCoalgebraFork X).pt } ≫ (beckCoalgebraFork X).ι = s.ι
refine_3 :
  ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }
⊢ { l : s.pt ⟶ (beckCoalgebraFork X).pt //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }

Tactic:
refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
refine_1 : s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
⊢ s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ (beckCoalgebraFork X).pt.a

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
refine_1 : s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
⊢ s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
rw [Functor.map_comp, reassoc_of% h₂, Comonad.right_counit]

Premises used: CategoryTheory.Comonad.right_counit, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
refine_1 : s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
refine_1 : s.ι.f = s.ι.f ≫ 𝟙 (T.obj X.A)
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
rw [Category.comp_id, Category.assoc, ← T.counit_naturality,
        reassoc_of% h₁, Comonad.left_counit]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comonad.counit_naturality, CategoryTheory.Comonad.left_counit, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = s.ι.f ≫ 𝟙 (T.obj X.A)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
refine_2 :
  Coalgebra.Hom.f ({ f := s.ι.f ≫ T.ε.app X.A, h := ⋯ : s.pt.Hom (beckCoalgebraFork X).pt } ≫ (beckCoalgebraFork X).ι) =
    s.ι.f
⊢ { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ : s.pt.Hom (beckCoalgebraFork X).pt } ≫ (beckCoalgebraFork X).ι = s.ι

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ Coalgebra.Hom.f ({ f := s.ι.f ≫ T.ε.app X.A, h := ⋯ : s.pt.Hom (beckCoalgebraFork X).pt } ≫ (beckCoalgebraFork X).ι) =
    s.ι.f

Tactic:
simpa [← T.ε.naturality_assoc, T.left_counit_assoc] using h₁ =≫ T.ε.app ((T : C ⥤ C).obj X.A)

Premises used: CategoryTheory.Comonad.toFunctor, CategoryTheory.Comonad.ε, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.Comonad.left_counit_assoc, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
refine_3 : m.f = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }.f
⊢ m = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
refine_3 : m.f = s.ι.f ≫ T.ε.app X.A
⊢ m.f = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }.f

Tactic:
dsimp only
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
refine_3 : m.f = (m ≫ (beckCoalgebraFork X).ι).f ≫ T.ε.app X.A
⊢ m.f = s.ι.f ≫ T.ε.app X.A

Tactic:
rw [← hm]
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = (m ≫ (beckCoalgebraFork X).ι).f ≫ T.ε.app X.A

Tactic:
simp [beckCoalgebraFork, X.counit]

Premises used: CategoryTheory.Comonad.Coalgebra.counit, CategoryTheory.Comonad.beckCoalgebraFork
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ (beckFork X).ι = X.a

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (T.map X.a) (T.δ.app X.A)
⊢ (beckEqualizer X).lift s = s.ι ≫ T.ε.app X.A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
M : Monad.{v, u} C
w :
  ∀ (x : C),
    (MonoidalCategoryStruct.whiskerRight M.μ M.toFunctor ≫ M.μ).app x =
      (Iso.hom (MonoidalCategoryStruct.associator M.toFunctor M.toFunctor M.toFunctor) ≫
            MonoidalCategoryStruct.whiskerLeft M.toFunctor M.μ ≫ M.μ).app
        x
⊢ MonoidalCategoryStruct.whiskerRight M.μ M.toFunctor ≫ M.μ =
    Iso.hom (MonoidalCategoryStruct.associator M.toFunctor M.toFunctor M.toFunctor) ≫
      MonoidalCategoryStruct.whiskerLeft M.toFunctor M.μ ≫ M.μ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
M : Monad.{v, u} C
x : C
⊢ (MonoidalCategoryStruct.whiskerRight M.μ M.toFunctor ≫ M.μ).app x =
    (Iso.hom (MonoidalCategoryStruct.associator M.toFunctor M.toFunctor M.toFunctor) ≫
          MonoidalCategoryStruct.whiskerLeft M.toFunctor M.μ ≫ M.μ).app
      x

Tactic:
simp [M.assoc]

Premises used: CategoryTheory.Monad.assoc
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
M : Mon (Functor.{v, v, u, u} C C)
X : C
⊢ Eq (α := M.X.obj ((M.X ⋙ M.X).obj X) ⟶ M.X.obj X)
    (CategoryStruct.comp (Y := M.X.obj (M.X.obj X)) (M.X.map (NatTrans.app μ X)) (NatTrans.app μ X) :
      M.X.obj ((M.X ⋙ M.X).obj X) ⟶ M.X.obj X)
    (CategoryStruct.comp (Y := M.X.obj (M.X.obj X)) (NatTrans.app μ (M.X.obj X)) (NatTrans.app μ X) :
      (M.X ⋙ M.X).obj (M.X.obj X) ⟶ M.X.obj X)

Tactic:
simpa [-MonObj.mul_assoc] using congrArg (fun t ↦ t.app X) (mul_assoc M.X)

Premises used: CategoryTheory.MonObj.mul_assoc, congrArg, CategoryTheory.Mon.X
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
M : Mon (Functor.{v, v, u, u} C C)
X : C
⊢ CategoryStruct.comp (Y := M.X.obj (M.X.obj X)) (NatTrans.app η (M.X.obj X)) (NatTrans.app μ X) =
    𝟙 (Functor.obj.{v, v, u, u} (𝟭 C) (M.X.obj X))

Tactic:
simpa [-MonObj.mul_one] using congrArg (fun t ↦ t.app X) (mul_one M.X)

Premises used: congrArg, CategoryTheory.MonObj.mul_one, CategoryTheory.Mon.X
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
M : Mon (Functor.{v, v, u, u} C C)
X : C
⊢ CategoryStruct.comp (Y := M.X.obj (M.X.obj X)) (M.X.map (NatTrans.app η X)) (NatTrans.app μ X) =
    𝟙 (M.X.obj (Functor.obj.{v, v, u, u} (𝟭 C) X))

Tactic:
simpa [-MonObj.one_mul] using congrArg (fun t ↦ t.app X) (one_mul M.X)

Premises used: congrArg, CategoryTheory.Mon.X, CategoryTheory.MonObj.one_mul
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
M : Mon (Functor.{v, v, u, u} C C)
X : C
⊢ (ofMon M).obj X = M.X.obj X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : Mon (Functor.{v, v, u, u} C C)
f : X_1 ⟶ Y
X : C
⊢ (ofMon X_1).η.app X ≫ f.hom.app X = (ofMon Y).η.app X

Tactic:
simpa [-IsMonHom.one_hom] using congrArg (fun t ↦ t.app X) (IsMonHom.one_hom f.hom)

Premises used: congrArg, CategoryTheory.Mon.Hom.hom, CategoryTheory.IsMonHom.one_hom
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Mon (Functor.{v, v, u, u} C C)
f : X ⟶ Y
Z : C
⊢ (ofMon X).μ.app Z ≫ f.hom.app Z = ((ofMon X).map (f.hom.app Z) ≫ f.hom.app ((ofMon Y).obj Z)) ≫ (ofMon Y).μ.app Z

Tactic:
simpa [-IsMonHom.mul_hom] using congrArg (fun t ↦ t.app Z) (IsMonHom.mul_hom f.hom)

Premises used: congrArg, CategoryTheory.Mon.Hom.hom, CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monad.EquivMon
Goal:
C : Type u
inst : Category.{v, u} C
A : Monad.{v, u} C
X : C
⊢ Eq (α :=
    (Functor.obj (𝟭 (Monad.{v, u} C)) A).obj X ⟶
      (Functor.obj (Equivalence.functor (monadMonEquiv C) ⋙ Equivalence.inverse (monadMonEquiv C)) A).obj X)
    (NatTrans.app (MonadHom.toNatTrans (Iso.hom (Iso.app (Equivalence.unitIso (monadMonEquiv C)) A))) X)
    (𝟙 ((Functor.obj (𝟭 (Monad.{v, u} C)) A).obj X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
c : Kleisli T
⊢ { of := c.of : Kleisli T } = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
c : C
⊢ { of := c : Kleisli T }.of = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : Kleisli T
f : X.Hom Y
of : { of := Hom.of { of := T.η.app X.of : X.Hom X } ≫ T.map f.of ≫ T.μ.app Y.of : X.Hom Y }.of = f.of
⊢ { of := Hom.of { of := T.η.app X.of : X.Hom X } ≫ T.map f.of ≫ T.μ.app Y.of : X.Hom Y } = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : Kleisli T
f : X.Hom Y
of : T.η.app X.of ≫ T.map f.of ≫ T.μ.app Y.of = f.of
⊢ { of := Hom.of { of := T.η.app X.of : X.Hom X } ≫ T.map f.of ≫ T.μ.app Y.of : X.Hom Y }.of = f.of

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : Kleisli T
f : X.Hom Y
of : Functor.map (𝟭 C) f.of ≫ 𝟙 (Functor.obj.{v, v, u, u} (𝟭 C) (T.obj Y.of)) = f.of
⊢ T.η.app X.of ≫ T.map f.of ≫ T.μ.app Y.of = f.of

Tactic:
rw [← T.η.naturality_assoc f.of, T.left_unit]

Premises used: CategoryTheory.Kleisli.Hom.of, CategoryTheory.Monad.left_unit, CategoryTheory.Monad.η, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : Kleisli T
f : X.Hom Y
⊢ Functor.map (𝟭 C) f.of ≫ 𝟙 (Functor.obj.{v, v, u, u} (𝟭 C) (T.obj Y.of)) = f.of

Tactic:
apply Category.comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
W X Y Z : Kleisli T
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ { of := { of := f.of ≫ T.map g.of ≫ T.μ.app Y.of : W.Hom Y }.of ≫ T.map h.of ≫ T.μ.app Z.of : W.Hom Z } =
    { of := f.of ≫ T.map { of := g.of ≫ T.map h.of ≫ T.μ.app Z.of : X.Hom Z }.of ≫ T.μ.app Z.of }

Tactic:
simp [Monad.assoc, T.mu_naturality_assoc]

Premises used: CategoryTheory.Monad.assoc, CategoryTheory.Monad.mu_naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
x y : Kleisli T
f g : x ⟶ y
h : f.of = g.of
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.Kleisli.Hom.ext
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { of := (f ≫ g) ≫ T.η.app Z : { of := X : Kleisli T }.Hom { of := Z : Kleisli T } } =
    {
      of :=
        { of := f ≫ T.η.app Y : { of := X : Kleisli T }.Hom { of := Y : Kleisli T } }.of ≫
          T.map { of := g ≫ T.η.app Z : { of := Y : Kleisli T }.Hom { of := Z : Kleisli T } }.of ≫
            T.μ.app { of := Z : Kleisli T }.of }

Tactic:
simp [← T.η.naturality g]

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

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

Premises used: CategoryTheory.Kleisli.Hom.of, CategoryTheory.Monad.assoc, CategoryTheory.Monad.μ, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
h :
  Eq (α := ((toKleisli T).obj X).of ⟶ T.obj Z.of)
    (Hom.of
      (({ toFun := fun (f : (toKleisli T).obj X ⟶ Z) ↦ f.of,
              invFun := fun (f : X ⟶ (fromKleisli T).obj Z) ↦ { of := f : ((toKleisli T).obj X).Hom Z }, left_inv := ⋯,
              right_inv := ⋯ : ((toKleisli T).obj X ⟶ Z) ≃ (X ⟶ (fromKleisli T).obj Z) }.symm :
          (a : X ⟶ (fromKleisli T).obj Z) → (toKleisli T).obj X ⟶ Z)
        (f ≫ g)))
    (Hom.of
      ((toKleisli T).map f ≫
        ({ toFun := fun (f : (toKleisli T).obj Y ⟶ Z) ↦ f.of,
                invFun := fun (f : Y ⟶ (fromKleisli T).obj Z) ↦ { of := f : ((toKleisli T).obj Y).Hom Z },
                left_inv := ⋯, right_inv := ⋯ : ((toKleisli T).obj Y ⟶ Z) ≃ (Y ⟶ (fromKleisli T).obj Z) }.symm :
            (a : Y ⟶ (fromKleisli T).obj Z) → (toKleisli T).obj Y ⟶ Z)
          g))
⊢ Eq (α := (toKleisli T).obj X ⟶ Z)
    (({ toFun := fun (f : (toKleisli T).obj X ⟶ Z) ↦ f.of,
              invFun := fun (f : X ⟶ (fromKleisli T).obj Z) ↦ { of := f : ((toKleisli T).obj X).Hom Z }, left_inv := ⋯,
              right_inv := ⋯ : ((toKleisli T).obj X ⟶ Z) ≃ (X ⟶ (fromKleisli T).obj Z) }.symm :
          (a : X ⟶ (fromKleisli T).obj Z) → (toKleisli T).obj X ⟶ Z)
        (f ≫ g) :
      (toKleisli T).obj X ⟶ Z)
    ((toKleisli T).map f ≫
        ({ toFun := fun (f : (toKleisli T).obj Y ⟶ Z) ↦ f.of,
                invFun := fun (f : Y ⟶ (fromKleisli T).obj Z) ↦ { of := f : ((toKleisli T).obj Y).Hom Z },
                left_inv := ⋯, right_inv := ⋯ : ((toKleisli T).obj Y ⟶ Z) ≃ (Y ⟶ (fromKleisli T).obj Z) }.symm :
            (a : Y ⟶ (fromKleisli T).obj Z) → (toKleisli T).obj Y ⟶ Z)
          g :
      (toKleisli T).obj X ⟶ Z)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ Eq (α := ((toKleisli T).obj X).of ⟶ T.obj Z.of)
    (Hom.of
      (({ toFun := fun (f : (toKleisli T).obj X ⟶ Z) ↦ f.of,
              invFun := fun (f : X ⟶ (fromKleisli T).obj Z) ↦ { of := f : ((toKleisli T).obj X).Hom Z }, left_inv := ⋯,
              right_inv := ⋯ : ((toKleisli T).obj X ⟶ Z) ≃ (X ⟶ (fromKleisli T).obj Z) }.symm :
          (a : X ⟶ (fromKleisli T).obj Z) → (toKleisli T).obj X ⟶ Z)
        (f ≫ g)))
    (Hom.of
      ((toKleisli T).map f ≫
        ({ toFun := fun (f : (toKleisli T).obj Y ⟶ Z) ↦ f.of,
                invFun := fun (f : Y ⟶ (fromKleisli T).obj Z) ↦ { of := f : ((toKleisli T).obj Y).Hom Z },
                left_inv := ⋯, right_inv := ⋯ : ((toKleisli T).obj Y ⟶ Z) ≃ (Y ⟶ (fromKleisli T).obj Z) }.symm :
            (a : Y ⟶ (fromKleisli T).obj Z) → (toKleisli T).obj Y ⟶ Z)
          g))

Tactic:
simp [← T.η.naturality_assoc g]

Premises used: CategoryTheory.Monad.η, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
U : Comonad.{v, u} C
c : Cokleisli U
⊢ { of := c.of : Cokleisli U } = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
U : Comonad.{v, u} C
c : C
⊢ { of := c : Cokleisli U }.of = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Kleisli
Goal:
C : Type u
inst : Category.{v, u} C
U : Comonad.{v, u} C
x y : Cokleisli U
f g : x ⟶ y
h : f.of = g.of
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.Cokleisli.Hom.ext
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
rw : c.π.app j ≫ 𝟙 (D.obj j).A = 𝟙 c.pt ≫ c.π.app j
⊢ (T.η.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
rw [Category.assoc, t.fac, newCone_π_app, ← T.η.naturality_assoc, Functor.id_map,
        (D.obj j).unit]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app, CategoryTheory.Functor.id_map, CategoryTheory.Monad.η, CategoryTheory.Monad.Algebra.unit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ c.π.app j ≫ 𝟙 (D.obj j).A = 𝟙 c.pt ≫ c.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
rw :
  (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    T.map (T.map (c.π.app j)) ≫ T.map (D.obj j).a ≫ (D.obj j).a
⊢ Eq (α := (T.toFunctor ⋙ T.toFunctor).obj c.pt ⟶ (D ⋙ T.forget).obj j)
    ((T.μ.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j)
    (CategoryStruct.comp (Y := T.obj c.pt) (T.map (t.lift (newCone D c)) : T.obj (T.obj c.pt) ⟶ T.obj c.pt)
        (t.lift (newCone D c) : (newCone D c).pt ⟶ c.pt) ≫
      c.π.app j)

Tactic:
rw [Category.assoc, Category.assoc, t.fac (newCone D c), newCone_π_app, ←
        Functor.map_comp_assoc, t.fac (newCone D c), newCone_π_app, ← T.μ.naturality_assoc,
        (D.obj j).assoc, Functor.map_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app, CategoryTheory.Monad.Algebra.assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Monad.μ, CategoryTheory.Monad.ForgetCreatesLimits.newCone, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (c.π.app j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    T.map (T.map (c.π.app j)) ≫ T.map (D.obj j).a ≫ (D.obj j).a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
X Y : J
f : X ⟶ Y
h :
  Eq (α := (obj (obj (const J) (conePoint D c t)) X).A ⟶ (D.obj Y).A)
    (Algebra.Hom.f (map (obj (const J) (conePoint D c t)) f ≫ { f := c.π.app Y, h := ⋯ }))
    (Algebra.Hom.f ({ f := c.π.app X, h := ⋯ } ≫ D.map f))
⊢ Eq (α := obj (obj (const J) (conePoint D c t)) X ⟶ D.obj Y)
    (map (obj (const J) (conePoint D c t)) f ≫ { f := c.π.app Y, h := ⋯ }) ({ f := c.π.app X, h := ⋯ } ≫ D.map f)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
X Y : J
f : X ⟶ Y
⊢ Eq (α := (obj (obj (const J) (conePoint D c t)) X).A ⟶ (D.obj Y).A)
    (Algebra.Hom.f (map (obj (const J) (conePoint D c t)) f ≫ { f := c.π.app Y, h := ⋯ }))
    (Algebra.Hom.f ({ f := c.π.app X, h := ⋯ } ≫ D.map f))

Tactic:
simpa using (c.w f).symm

Premises used: CategoryTheory.Limits.Cone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
dsimp :
  CategoryStruct.comp (Y := T.obj c.pt) (T.map (t.lift (T.forget.mapCone s)) : T.obj s.pt.A ⟶ T.obj c.pt)
        (t.lift (newCone D c) : (newCone D c).pt ⟶ c.pt) ≫
      c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j
⊢ (T.map (t.lift (T.forget.mapCone s)) ≫ (liftedCone D c t).pt.a) ≫ c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
rw : T.map (T.forget.map (s.π.app j)) ≫ (D.obj j).a = s.pt.a ≫ T.forget.map (s.π.app j)
⊢ CategoryStruct.comp (Y := T.obj c.pt) (T.map (t.lift (T.forget.mapCone s)) : T.obj s.pt.A ⟶ T.obj c.pt)
        (t.lift (newCone D c) : (newCone D c).pt ⟶ c.pt) ≫
      c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j

Tactic:
rw [Category.assoc, Category.assoc, t.fac, newCone_π_app, ← Functor.map_comp_assoc,
            t.fac, Functor.mapCone_π_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.Limits.IsLimit.fac