awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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) (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)
have 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)))
Tactic: change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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)))
⊢ 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)
have change₁ : IsColimit (counitCofork adj Y)
Tactic: change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
⊢ IsColimit (counitCofork adj Y)
have apply : ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) G
Tactic: apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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)
⊢ (comparison adj).IsEquivalence
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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 f g ⋙ G)
have rw : HasColimit
  (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
    ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
Tactic: rw [hasColimit_iff_of_iso (diagramIsoParallelPair.{v₁} _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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
⊢ MonadicRightAdjoint G
have I : ∀ {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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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)
⊢ MonadicRightAdjoint G
have this : HasCoequalizerOfIsSplitPair G
Tactic: have : HasCoequalizerOfIsSplitPair G := ⟨fun _ _ => hasColimit_of_created (parallelPair _ _) G⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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
⊢ MonadicRightAdjoint G
have this₁ : PreservesColimitOfIsSplitPair G
Tactic: have : PreservesColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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
⊢ MonadicRightAdjoint G
have this₁ : ReflectsColimitOfIsSplitPair G
Tactic: have : ReflectsColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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
⊢ ReflectsColimit (parallelPair f g) G
have this : HasCoequalizer f g
Tactic: have := HasCoequalizerOfIsSplitPair.out G f g
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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
⊢ MonadicRightAdjoint G
have this : ReflectsColimitOfIsSplitPair G
Tactic: have : ReflectsColimitOfIsSplitPair G := ⟨fun f g _ => by
    have := HasCoequalizerOfIsSplitPair.out G f g
    apply reflectsColimit_of_reflectsIsomorphisms⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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)
have _ : IsIso (Y := adj.toMonad.forget.obj ((leftAdjointComparison adj ⋙ comparison adj).obj X))
  (adj.toMonad.forget.map (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
Tactic: apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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))
have change : IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
  (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
Tactic: change IsIso ((comparisonAdjunction adj).unit.app X).f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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)
    (Algebra.Hom.f (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) X))
have rw : IsIso (Y := ((leftAdjointComparison adj ⋙ comparison adj).obj X).A)
  ((beckCoequalizer X).desc (unitCofork X) : (beckCofork X).pt ⟶ (unitCofork X).pt)
Tactic: rw [comparisonAdjunction_unit_f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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
⊢ (comparison adj).IsEquivalence
have this : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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)
have 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)
Tactic: rw [comparisonAdjunction_counit_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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) (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)
have 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)))
Tactic: change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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)))
⊢ 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)
have change₁ : IsColimit (counitCofork adj Y)
Tactic: change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
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
⊢ IsColimit (counitCofork adj Y)
have apply : ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y)))) G
Tactic: apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (hypothesis)
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)
⊢ (comparison adj).IsEquivalence
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x x_1 : Type u
f : x ⟶ x_1
⊢ 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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x x_1 : Type u
x_2 : x ⟶ x_1
⊢ (__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
have 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
Tactic: ext _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
⊢ 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)
have 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 := sorry :
                NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
              x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := sorry :
              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 := sorry } ((ofTypeFunctor m).obj x))
          (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := sorry } x)))
      x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
⊢ 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))
have 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 := sorry : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) }
            ((ofTypeFunctor m).obj x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := sorry :
              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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Types (goal)
Goal:
m : Type u → Type u
inst : _root_.Monad m
inst_1 : LawfulMonad m
x : Type u
⊢ CategoryStruct.comp (Y := (ofTypeFunctor m).obj ((ofTypeFunctor m).obj x))
      ((ofTypeFunctor m).map (NatTrans.app { app := fun (X : Type u) ↦ ↾pure, naturality := ⋯ } x))
      (NatTrans.app { app := fun (X : Type u) ↦ ↾joinM, naturality := ⋯ } x) =
    𝟙 ((ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x))
have h : ∀ (x_1 : (ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) 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) ↦ ↾pure, naturality := sorry : NatTrans (𝟭 (Type u)) (ofTypeFunctor m) }
              x))
          (NatTrans.app
            { app := fun (X : Type u) ↦ ↾joinM, naturality := sorry :
              NatTrans (ofTypeFunctor m ⋙ ofTypeFunctor m) (ofTypeFunctor m) }
            x)))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((ofTypeFunctor m).obj (Functor.obj (𝟭 (Type u)) x)))).toFun x_1
Tactic: ext