awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this_1 :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
this : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))
⊢ IsLimit (unitFork adj Y)
have apply : ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F
Tactic: apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
⊢ (comparison adj).IsEquivalence
have this₁ : ∀ (Y : C),
  IsIso (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y) (NatTrans.app (unit (comparisonAdjunction adj)) Y)
Tactic: have : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y) := by
      intro Y
      rw [comparisonAdjunction_unit_app]
      change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
      · infer_instance
      have : IsCoreflexivePair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) := by
        apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
        · rw [← G.map_comp, ← G.map_id]
          exact congr_arg G.map (adj.left_triangle_components Y)
        · rw [← G.map_id]
          simp
      apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
      apply reflectsLimit_of_reflectsIsomorphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
have apply : T.cofree.obj (T.obj X.A) ⟶ T.cofree.obj X.A
Tactic: apply IsCoreflexivePair.mk' _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
apply : T.cofree.obj (T.obj X.A) ⟶ T.cofree.obj X.A
⊢ IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
have apply₁ : CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
Tactic: apply IsCoreflexivePair.mk' _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
apply : T.cofree.obj (T.obj X.A) ⟶ T.cofree.obj X.A
apply₁ : CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
⊢ IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
have apply₂ : CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
Tactic: apply IsCoreflexivePair.mk' _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
have h : (CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A)).f = Coalgebra.Hom.f (𝟙 (T.cofree.obj X.A))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ (CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A)).f = Coalgebra.Hom.f (𝟙 (T.cofree.obj X.A))
have h : T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)
have h : T.map (X.a ≫ T.ε.app X.A) = 𝟙 (T.obj X.A)
Tactic: rw [← Functor.map_comp, X.counit, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
h : T.map (X.a ≫ T.ε.app X.A) = 𝟙 (T.obj X.A)
⊢ T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)
have h₁ : T.map (𝟙 X.A) = 𝟙 (T.obj X.A)
Tactic: rw [← Functor.map_comp, X.counit, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
h : T.map (X.a ≫ T.ε.app X.A) = 𝟙 (T.obj X.A)
h₁ : T.map (𝟙 X.A) = 𝟙 (T.obj X.A)
⊢ T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)
have h₂ : Eq.{v₁ + 1} (α := T.obj X.A ⟶ T.obj X.A) (𝟙 (T.obj X.A)) (𝟙 (T.obj X.A))
Tactic: rw [← Functor.map_comp, X.counit, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
have h : (CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A)).f = Coalgebra.Hom.f (𝟙 (T.cofree.obj X.A))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (hypothesis)
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)
⊢ { l : s.pt ⟶ (beckCoalgebraFork X).pt //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }
have h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
Tactic: have h₁ : s.ι.f ≫ (T : C ⥤ C).map X.a = s.ι.f ≫ T.δ.app X.A :=
      congr_arg Comonad.Coalgebra.Hom.f s.condition
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (hypothesis)
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
⊢ { l : s.pt ⟶ (beckCoalgebraFork X).pt //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }
have h₂ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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
⊢ { l : s.pt ⟶ (beckCoalgebraFork X).pt //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }
have refine_1 : s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ (beckCoalgebraFork X).pt.a
Tactic: refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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
⊢ { l : s.pt ⟶ (beckCoalgebraFork X).pt //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }
have refine_2 : { f := s.ι.f ≫ T.ε.app X.A, h := sorry : s.pt.Hom (beckCoalgebraFork X).pt } ≫ (beckCoalgebraFork X).ι = s.ι
Tactic: refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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.ι
⊢ { l : s.pt ⟶ (beckCoalgebraFork X).pt //
    l ≫ (beckCoalgebraFork X).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = l }
have refine_3 : ∀ {m : s.pt ⟶ (beckCoalgebraFork X).pt}, m ≫ (beckCoalgebraFork X).ι = s.ι → m = { f := s.ι.f ≫ T.ε.app X.A, h := sorry }
Tactic: refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ (beckCoalgebraFork X).pt.a
have refine_1 : s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
have refine_1 : s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
Tactic: rw [Functor.map_comp, reassoc_of% h₂, Comonad.right_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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 ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
have refine_1 : s.ι.f = s.ι.f ≫ 𝟙 (T.obj X.A)
Tactic: rw [Category.comp_id, Category.assoc, ← T.counit_naturality,
        reassoc_of% h₁, Comonad.left_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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
⊢ { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ : s.pt.Hom (beckCoalgebraFork X).pt } ≫ (beckCoalgebraFork X).ι = s.ι
have refine_2 : Coalgebra.Hom.f ({ f := s.ι.f ≫ T.ε.app X.A, h := sorry : s.pt.Hom (beckCoalgebraFork X).pt } ≫ (beckCoalgebraFork X).ι) =
  s.ι.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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 := s.ι.f ≫ T.ε.app X.A, h := ⋯ }
have refine_3 : m.f = { f := s.ι.f ≫ T.ε.app X.A, h := sorry }.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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 = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }.f
have refine_3 : m.f = s.ι.f ≫ T.ε.app X.A
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Equalizer (goal)
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 = s.ι.f ≫ T.ε.app X.A
have refine_3 : m.f = (m ≫ (beckCoalgebraFork X).ι).f ≫ T.ε.app X.A
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.EquivMon (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Monad.{v, u} C
⊢ MonoidalCategoryStruct.whiskerRight M.μ M.toFunctor ≫ M.μ =
    Iso.hom (MonoidalCategoryStruct.associator M.toFunctor M.toFunctor M.toFunctor) ≫
      MonoidalCategoryStruct.whiskerLeft M.toFunctor M.μ ≫ M.μ
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Kleisli (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : Kleisli T
f : X.Hom Y
⊢ { of := Hom.of { of := T.η.app X.of : X.Hom X } ≫ T.map f.of ≫ T.μ.app Y.of : X.Hom Y } = f
have 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Kleisli (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : Kleisli T
f : X.Hom Y
⊢ { 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
have of : T.η.app X.of ≫ T.map f.of ≫ T.μ.app Y.of = f.of
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Kleisli (goal)
Goal:
C : Type u
inst : Category.{v, u} C
T : Monad.{v, u} C
X Y : Kleisli T
f : X.Hom Y
⊢ T.η.app X.of ≫ T.map f.of ≫ T.μ.app Y.of = f.of
have of : Functor.map (𝟭 C) f.of ≫ 𝟙 (Functor.obj.{v, v, u, u} (𝟭 C) (T.obj Y.of)) = f.of
Tactic: rw [← T.η.naturality_assoc f.of, T.left_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Kleisli (goal)
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 ⟶ 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)
have 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 := sorry,
            right_inv := sorry : ((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 := sorry,
              right_inv := sorry : ((toKleisli T).obj Y ⟶ Z) ≃ (Y ⟶ (fromKleisli T).obj Z) }.symm :
          (a : Y ⟶ (fromKleisli T).obj Z) → (toKleisli T).obj Y ⟶ Z)
        g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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.η.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j
have rw : c.π.app j ≫ 𝟙 (D.obj j).A = 𝟙 c.pt ≫ c.π.app j
Tactic: rw [Category.assoc, t.fac, newCone_π_app, ← T.η.naturality_assoc, Functor.id_map,
        (D.obj j).unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 ⟶ 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)
have 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 := sorry }))
  (Algebra.Hom.f ({ f := c.π.app X, h := sorry } ≫ D.map f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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
have rw : T.map (T.forget.map (s.π.app j)) ≫ (D.obj j).a = s.pt.a ≫ T.forget.map (s.π.app j)
Tactic: rw [Category.assoc, Category.assoc, t.fac, newCone_π_app, ← Functor.map_comp_assoc,
            t.fac, Functor.mapCone_π_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone D c t).π.app j = s.π.app j
⊢ m = { f := t.lift (T.forget.mapCone s), h := ⋯ }
have h : m.f = Algebra.Hom.f { f := t.lift (T.forget.mapCone s), h := sorry }
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone D c t).π.app j = s.π.app j
⊢ m.f = Algebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ }
have h : ∀ (j : J_1), m.f ≫ c.π.app j = Algebra.Hom.f { f := t.lift (T.forget.mapCone s), h := sorry } ≫ c.π.app j
Tactic: apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
⊢ T.η.app c.pt ≫ lambda c t = 𝟙 c.pt
have apply : ∀ (j : J), c.ι.app j ≫ T.η.app c.pt ≫ lambda c t = c.ι.app j ≫ 𝟙 c.pt
Tactic: apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.ι.app j ≫ T.η.app c.pt ≫ lambda c t = c.ι.app j ≫ 𝟙 c.pt
have rw : c.ι.app j = c.ι.app j ≫ 𝟙 c.pt
Tactic: rw [show c.ι.app j ≫ T.η.app c.pt ≫ _ = T.η.app (D.obj j).A ≫ _ ≫ _ from
        T.η.naturality_assoc _ _,
      commuting, Algebra.unit_assoc (D.obj j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (T.mapCocone (T.mapCocone c)).ι.app j ≫ T.μ.app c.pt ≫ lambda c t =
    (T.mapCocone (T.mapCocone c)).ι.app j ≫ T.map (lambda c t) ≫ lambda c t
have rw : T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map (D.obj j).a ≫ (D.obj j).a ≫ c.ι.app j
Tactic: rw [Functor.mapCocone_ι_app, Functor.mapCocone_ι_app,
      show (T : C ⥤ C).map ((T : C ⥤ C).map _) ≫ _ ≫ _ = _ from T.μ.naturality_assoc _ _, ←
      Functor.map_comp_assoc, commuting, Functor.map_comp, Category.assoc, commuting]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ Eq (α := D.obj A ⟶ obj (obj (const J) (coconePoint c t)) B) (D.map f ≫ { f := c.ι.app B, h := ⋯ })
    ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint c t)) f)
have h : Eq (α := (D.obj A).A ⟶ (obj (obj (const J) (coconePoint c t)) B).A)
  (Algebra.Hom.f (D.map f ≫ { f := c.ι.app B, h := sorry }))
  (Algebra.Hom.f ({ f := c.ι.app A, h := sorry } ≫ map (obj (const J) (coconePoint c t)) f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ Eq (α := (D.obj A).A ⟶ (obj (obj (const J) (coconePoint c t)) B).A)
    (Algebra.Hom.f (D.map f ≫ { f := c.ι.app B, h := ⋯ }))
    (Algebra.Hom.f ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint c t)) f))
have h : (D.map f).f ≫ c.ι.app B = c.ι.app A ≫ 𝟙 c.pt
Tactic: dsimp