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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
rw :
  IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)
⊢ IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))

Tactic:
rw [comparisonAdjunction_unit_f]

Premises used: CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f
-- 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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
this :
  IsIso (Y := (unitCofork X).pt)
    (Iso.hom ((beckCoequalizer X).coconePointUniqueUpToIso (unitColimitOfPreservesCoequalizer X)))
⊢ IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)

Tactic:
change
          IsIso
            (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
                (unitColimitOfPreservesCoequalizer X)).hom

Premises used: CategoryTheory.Monad.beckCoequalizer, CategoryTheory.IsIso, CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer, 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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := (unitCofork X).pt)
    (Iso.hom ((beckCoequalizer X).coconePointUniqueUpToIso (unitColimitOfPreservesCoequalizer X)))

Tactic:
(IsColimit.coconePointUniqueUpToIso _ _).isIso_hom

Premises used: CategoryTheory.Iso.isIso_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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
X : adj.toMonad.Algebra
⊢ IsIso (Y := (unitCofork X).pt)
    (Iso.hom ((beckCoequalizer X).coconePointUniqueUpToIso (unitColimitOfPreservesCoequalizer X)))

Tactic:
exact (IsColimit.coconePointUniqueUpToIso _ _).isIso_hom

Premises used: CategoryTheory.Iso.isIso_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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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]
        change
          IsIso
            (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
                (unitColimitOfPreservesCoequalizer X)).hom
        exact (IsColimit.coconePointUniqueUpToIso _ _).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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair G
this :
  ∀ (X : adj.toMonad.Algebra),
    IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)
Y : D
h : G.IsSplitPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))) := ⋯
⊢ ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) G

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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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 _ _ _ _ _ _ _ _ ?_
      letI _ :
        G.IsSplitPair (F.map (G.map (adj.counit.app Y)))
          (adj.counit.app (F.obj (G.obj Y))) :=
        MonadicityInternal.main_pair_G_split _ ((comparison adj).obj Y)
      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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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 : HasCoequalizerOfIsSplitPair G
inst_3 : PreservesColimitOfIsSplitPair G
inst_4 : ReflectsColimitOfIsSplitPair 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.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 : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
rw :
  HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
⊢ HasColimit (parallelPair f g ⋙ G)

Tactic:
rw [hasColimit_iff_of_iso (diagramIsoParallelPair.{v₁} _)]
-- 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 : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))

Tactic:
inferInstanceAs <| HasCoequalizer (G.map f) (G.map g)

Premises used: CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers._proof_1
-- 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 : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))

Tactic:
exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g)
-- 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 : CreatesColimitOfIsSplitPair G
⊢ ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)

Tactic:
have I {A B} (f g : A ⟶ B) [G.IsSplitPair f g] : HasColimit (parallelPair f g ⋙ G) := by
    rw [hasColimit_iff_of_iso (diagramIsoParallelPair.{v₁} _)]
    exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g)
-- 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 : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
⊢ HasCoequalizerOfIsSplitPair G

Tactic:
have : HasCoequalizerOfIsSplitPair G := ⟨fun _ _ => hasColimit_of_created (parallelPair _ _) G⟩
-- 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 : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this : HasCoequalizerOfIsSplitPair G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ PreservesColimit (parallelPair f g) G

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 : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this : HasCoequalizerOfIsSplitPair G
⊢ PreservesColimitOfIsSplitPair G

Tactic:
have : PreservesColimitOfIsSplitPair G := ⟨by intros; 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 : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this_1 : HasCoequalizerOfIsSplitPair G
this : PreservesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst_3 : G.IsSplitPair f g
⊢ ReflectsColimit (parallelPair f g) G

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 : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this_1 : HasCoequalizerOfIsSplitPair G
this : PreservesColimitOfIsSplitPair G
⊢ ReflectsColimitOfIsSplitPair G

Tactic:
have : ReflectsColimitOfIsSplitPair G := ⟨by intros; 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 : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this_1 : HasCoequalizerOfIsSplitPair G
this_2 : PreservesColimitOfIsSplitPair G
this : ReflectsColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G

Tactic:
exact monadicOfHasPreservesReflectsGSplitCoequalizers adj

Premises used: CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers
-- 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 : G.ReflectsIsomorphisms
inst_3 : HasCoequalizerOfIsSplitPair G
inst_4 : PreservesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
h : G.IsSplitPair f g
⊢ HasCoequalizer f g

Tactic:
have := HasCoequalizerOfIsSplitPair.out G f g
-- 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 : G.ReflectsIsomorphisms
inst_3 : HasCoequalizerOfIsSplitPair G
inst_4 : PreservesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
h : G.IsSplitPair f g
this : HasCoequalizer f g
⊢ ReflectsColimit (parallelPair f g) 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 : G.ReflectsIsomorphisms
inst_3 : HasCoequalizerOfIsSplitPair G
inst_4 : PreservesColimitOfIsSplitPair G
⊢ ReflectsColimitOfIsSplitPair G

Tactic:
have : ReflectsColimitOfIsSplitPair G := ⟨fun f g _ => by
    have := HasCoequalizerOfIsSplitPair.out G f g
    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 : G.ReflectsIsomorphisms
inst_3 : HasCoequalizerOfIsSplitPair G
inst_4 : PreservesColimitOfIsSplitPair G
this : ReflectsColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G

Tactic:
apply monadicOfHasPreservesReflectsGSplitCoequalizers adj

Premises used: CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers
-- 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
A B : D
f g : A ⟶ B
inst_4 : IsReflexivePair f g
inst_5 : PreservesColimitOfIsReflexivePair G
⊢ PreservesColimit (parallelPair f g) G

Tactic:
PreservesColimitOfIsReflexivePair.out f g

Premises used: CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out
-- 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), PreservesColimit (parallelPair (F.map X.a) (adj.counit.app (F.obj X.A))) G

Tactic:
fun _ => PreservesColimitOfIsReflexivePair.out _ _

Premises used: CategoryTheory.Monad.Algebra.a, CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out, CategoryTheory.Monad.Algebra.A, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.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
X : adj.toMonad.Algebra
_ :
  IsIso (Y := adj.toMonad.forget.obj ((leftAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toMonad.forget.map (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
⊢ IsIso (Y := (leftAdjointComparison adj ⋙ comparison adj).obj X)
    (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X)

Tactic:
apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _

Premises used: CategoryTheory.Monad.forget, CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Adjunction.toMonad
-- 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
change :
  IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
⊢ IsIso (Y := adj.toMonad.forget.obj ((leftAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toMonad.forget.map (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))

Tactic:
change IsIso ((comparisonAdjunction adj).unit.app X).f

Premises used: CategoryTheory.IsIso, CategoryTheory.Adjunction.unit, CategoryTheory.Monad.Algebra.Hom.f, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction, CategoryTheory.NatTrans.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
X : adj.toMonad.Algebra
rw :
  IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)
⊢ IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))

Tactic:
rw [comparisonAdjunction_unit_f]

Premises used: CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f