awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)

Tactic:
(IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
          (unitColimitOfPreservesCoequalizer X)).isIso_hom

Premises used: CategoryTheory.Monad.beckCoequalizer, CategoryTheory.Limits.colimit, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj, CategoryTheory.Iso.isIso_hom, CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)

Tactic:
exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
          (unitColimitOfPreservesCoequalizer X)).isIso_hom

Premises used: CategoryTheory.Monad.beckCoequalizer, CategoryTheory.Iso.isIso_hom, CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
⊢ ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)

Tactic:
have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by
      intro X
      apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).unit.app X).f
        rw [comparisonAdjunction_unit_f]
        exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
          (unitColimitOfPreservesCoequalizer X)).isIso_hom
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Y : D
rw :
  IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y) (Y := Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) Y)
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))
        (counitCofork adj Y) :
      colimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) ⟶
        (counitCofork adj Y).pt)
⊢ IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y)
    (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) Y)

Tactic:
rw [comparisonAdjunction_counit_app]

Premises used: CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Y : D
change :
  IsIso (X := (colimit.cocone (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))).pt)
    (Iso.hom
      (IsColimit.coconePointUniqueUpToIso
        (colimit.isColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))))
        (counitCoequalizerOfReflectsCoequalizer adj Y)))
change₁ : IsColimit (counitCofork adj Y)
⊢ IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y) (Y := Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) Y)
    (colimit.desc (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))
        (counitCofork adj Y) :
      colimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) ⟶
        (counitCofork adj Y).pt)

Tactic:
change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom

Premises used: CategoryTheory.IsIso, CategoryTheory.Iso.hom, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Y : D
⊢ IsIso (X := (colimit.cocone (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))).pt)
    (Iso.hom
      (IsColimit.coconePointUniqueUpToIso
        (colimit.isColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))))
        (counitCoequalizerOfReflectsCoequalizer adj Y)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Y : D
apply : ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) G
⊢ IsColimit (counitCofork adj Y)

Tactic:
apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_

Premises used: CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Y : D
⊢ ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) G

Tactic:
apply reflectsColimit_of_reflectsIsomorphisms

Premises used: CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
⊢ ∀ (Y : D),
    IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y)
      (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) Y)

Tactic:
have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) := by
      intro Y
      rw [comparisonAdjunction_counit_app]
      -- Porting note: passing instances through
      change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
      · infer_instance
      -- Porting note: passing instances through
      apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_
      apply reflectsColimit_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this_1 :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
this :
  ∀ (Y : D),
    IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y)
      (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) Y)
⊢ (comparison adj).IsEquivalence

Tactic:
(comparisonAdjunction adj).toEquivalence.isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.Monad.comparison, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction, CategoryTheory.Adjunction.toEquivalence
-- Module: Mathlib.CategoryTheory.Monad.Monadicity
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : HasReflexiveCoequalizers.{v₁, u₂} D
inst_3 : G.ReflectsIsomorphisms
inst_4 : PreservesColimitOfIsReflexivePair G
this_1 :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
this :
  ∀ (Y : D),
    IsIso (X := (comparison adj ⋙ leftAdjointComparison adj).obj Y)
      (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) Y)
⊢ (comparison adj).IsEquivalence

Tactic:
exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction, CategoryTheory.Adjunction.toEquivalence
-- Module: Mathlib.CategoryTheory.Monad.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasBinaryProducts.{v, u} C
X_1 Y : Coalgebra.{v, u} (prodComonad X)
f : X_1 ⟶ Y
⊢ f.f ≫ (Over.mk (Y.a ≫ prod.fst)).hom = (Over.mk (X_1.a ≫ prod.fst)).hom

Tactic:
simp [← dsimp% f.h_assoc]

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.h_assoc
-- Module: Mathlib.CategoryTheory.Monad.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasBinaryProducts.{v, u} C
A : Coalgebra.{v, u} (prodComonad X)
⊢ ((Functor.obj (𝟭 (Coalgebra.{v, u} (prodComonad X))) A).a ≫
        Functor.map (toFunctor (prodComonad X))
          (Iso.hom (Iso.refl (Functor.obj (𝟭 (Coalgebra.{v, u} (prodComonad X))) A).A))) ≫
      prod.fst =
    (Iso.hom (Iso.refl (Functor.obj (𝟭 (Coalgebra.{v, u} (prodComonad X))) A).A) ≫
        Coalgebra.a (Functor.obj (coalgebraToOver X ⋙ overToCoalgebra X) A)) ≫
      prod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasBinaryProducts.{v, u} C
A : Coalgebra.{v, u} (prodComonad X)
⊢ ((Functor.obj (𝟭 (Coalgebra.{v, u} (prodComonad X))) A).a ≫
        Functor.map (toFunctor (prodComonad X))
          (Iso.hom (Iso.refl (Functor.obj (𝟭 (Coalgebra.{v, u} (prodComonad X))) A).A))) ≫
      prod.snd =
    (Iso.hom (Iso.refl (Functor.obj (𝟭 (Coalgebra.{v, u} (prodComonad X))) A).A) ≫
        Coalgebra.a (Functor.obj (coalgebraToOver X ⋙ overToCoalgebra X) A)) ≫
      prod.snd

Tactic:
simpa using A.counit

Premises used: CategoryTheory.Comonad.Coalgebra.counit
-- Module: Mathlib.CategoryTheory.Monad.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasBinaryCoproducts.{v, u} C
X_1 Y : Algebra.{v, u} (coprodMonad X)
f : X_1 ⟶ Y
⊢ (Under.mk (coprod.inl ≫ X_1.a)).hom ≫ f.f = (Under.mk (coprod.inl ≫ Y.a)).hom

Tactic:
simp [← dsimp% f.h]

Premises used: CategoryTheory.Monad.Algebra.Hom.h
-- Module: Mathlib.CategoryTheory.Monad.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasBinaryCoproducts.{v, u} C
A : Algebra.{v, u} (coprodMonad X)
⊢ coprod.inl ≫
      Functor.map (toFunctor (coprodMonad X))
          (Iso.hom (Iso.refl (Functor.obj (𝟭 (Algebra.{v, u} (coprodMonad X))) A).A)) ≫
        Algebra.a (Functor.obj (algebraToUnder X ⋙ underToAlgebra X) A) =
    coprod.inl ≫
      (Functor.obj (𝟭 (Algebra.{v, u} (coprodMonad X))) A).a ≫
        Iso.hom (Iso.refl (Functor.obj (𝟭 (Algebra.{v, u} (coprodMonad X))) A).A)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Products
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasBinaryCoproducts.{v, u} C
A : Algebra.{v, u} (coprodMonad X)
⊢ coprod.inr ≫
      Functor.map (toFunctor (coprodMonad X))
          (Iso.hom (Iso.refl (Functor.obj (𝟭 (Algebra.{v, u} (coprodMonad X))) A).A)) ≫
        Algebra.a (Functor.obj (algebraToUnder X ⋙ underToAlgebra X) A) =
    coprod.inr ≫
      (Functor.obj (𝟭 (Algebra.{v, u} (coprodMonad X))) A).a ≫
        Iso.hom (Iso.refl (Functor.obj (𝟭 (Algebra.{v, u} (coprodMonad X))) A).A)

Tactic:
simpa using A.unit.symm

Premises used: Eq.symm, CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x x_1 : Type u
f : x ⟶ x_1
h :
  ∀ (x_2 : Functor.obj (𝟭 (Type u)) x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (𝟭 (Type u)) f ≫
            (fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x_1))
        x_2 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x ≫ __Functor.map f))
        x_2
⊢ Eq (α := Functor.obj (𝟭 (Type u)) x ⟶ __Functor.obj x_1)
    (Functor.map (𝟭 (Type u)) f ≫ (fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x_1)
    ((fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x ≫ __Functor.map f)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x_1 x_2 : Type u
f : x_1 ⟶ x_2
x : Functor.obj (𝟭 (Type u)) x_1
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (𝟭 (Type u)) f ≫ (fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x_2))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x_1 ≫ __Functor.map f))
      x

Tactic:
(LawfulApplicative.map_pure f x).symm

Premises used: CategoryTheory.ConcreteCategory.hom, LawfulApplicative.map_pure, Eq.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x_1 x_2 : Type u
f : x_1 ⟶ x_2
x : Functor.obj (𝟭 (Type u)) x_1
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (𝟭 (Type u)) f ≫ (fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x_2))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Type u) ↦ (↾pure : Functor.obj (𝟭 (Type u)) X ⟶ __Functor.obj X)) x_1 ≫ __Functor.map f))
      x

Tactic:
exact (LawfulApplicative.map_pure f x).symm

Premises used: CategoryTheory.ConcreteCategory.hom, LawfulApplicative.map_pure, Eq.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x x_1 : Type u
x_2 : x ⟶ x_1
h :
  ∀ (x_3 : (__Functor ⋙ __Functor).obj x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((__Functor ⋙ __Functor).map x_2 ≫
            (fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x_1))
        x_3 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x ≫ __Functor.map x_2))
        x_3
⊢ (__Functor ⋙ __Functor).map x_2 ≫
      (fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x_1 =
    (fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x ≫ __Functor.map x_2

Tactic:
ext _
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x x_1 : Type u
x_2 : x ⟶ x_1
x_3 : (__Functor ⋙ __Functor).obj x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((__Functor ⋙ __Functor).map x_2 ≫
          (fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x_1))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x ≫ __Functor.map x_2))
      x_3

Tactic:
joinM_map_map _ _

Premises used: joinM_map_map, joinM
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x x_1 : Type u
x_2 : x ⟶ x_1
x_3 : (__Functor ⋙ __Functor).obj x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((__Functor ⋙ __Functor).map x_2 ≫
          (fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x_1))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Type u) ↦ (↾joinM : (__Functor ⋙ __Functor).obj X ⟶ __Functor.obj X)) x ≫ __Functor.map x_2))
      x_3

Tactic:
exact joinM_map_map _ _

Premises used: joinM_map_map
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
h :
  ∀ (x_1 : (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj x)),
    Eq (α := (ofTypeFunctor m).obj x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
            ((ofTypeFunctor m).map
              (NatTrans.app
                { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
                  NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
                x))
            (NatTrans.app
              { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
                NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
              x)))
        x_1)
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
            (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } ((ofTypeFunctor m).obj x))
            (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x)))
        x_1)
⊢ Eq (α := (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj x) ⟶ (ofTypeFunctor m).obj x)
    (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
        ((ofTypeFunctor m).map (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x))
        (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x) :
      (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj x) ⟶ (ofTypeFunctor m).obj x)
    (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
        (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } ((ofTypeFunctor m).obj x))
        (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x) :
      (ofTypeFunctor m ⋙ ofTypeFunctor m).obj ((ofTypeFunctor m).obj x) ⟶ (ofTypeFunctor m).obj x)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
x_1 : (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj x)
⊢ Eq (α := (ofTypeFunctor m).obj x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          ((ofTypeFunctor m).map
            (NatTrans.app
              { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
                NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
              x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
              NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
            x)))
      x_1)
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } ((ofTypeFunctor m).obj x))
          (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x)))
      x_1)

Tactic:
joinM_map_joinM _

Premises used: joinM_map_joinM, joinM
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
x_1 : (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj x)
⊢ Eq (α := (ofTypeFunctor m).obj x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          ((ofTypeFunctor m).map
            (NatTrans.app
              { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
                NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
              x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
              NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
            x)))
      x_1)
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
          (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } ((ofTypeFunctor m).obj x))
          (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x)))
      x_1)

Tactic:
exact joinM_map_joinM _

Premises used: joinM_map_joinM
-- Module: Mathlib.CategoryTheory.Monad.Types
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
h :
  ∀ (x_1 : Functor.obj (𝟭 (Type u)) ((ofTypeFunctor m).obj x)),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
            (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) }
              ((ofTypeFunctor m).obj x))
            (NatTrans.app
              { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ :
                NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
              x)))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Functor.obj (𝟭 (Type u)) ((ofTypeFunctor m).obj x)))).toFun x_1
⊢ CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
      (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ } ((ofTypeFunctor m).obj x))
      (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x) =
    𝟙 (Functor.obj (𝟭 (Type u)) ((ofTypeFunctor m).obj x))

Tactic:
ext