awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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
X : adj.toComonad.Coalgebra
_ :
  IsIso (X := adj.toComonad.forget.obj ((rightAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toComonad.forget.map (NatTrans.app (counit (comparisonAdjunction adj)) X))
⊢ IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X) (NatTrans.app (counit (comparisonAdjunction adj)) X)

Tactic:
apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _

Premises used: CategoryTheory.Comonad.forget, CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Adjunction.toComonad
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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
X : adj.toComonad.Coalgebra
change :
  IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Coalgebra.Hom.f (NatTrans.app (counit (comparisonAdjunction adj)) X))
⊢ IsIso (X := adj.toComonad.forget.obj ((rightAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toComonad.forget.map (NatTrans.app (counit (comparisonAdjunction adj)) X))

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

Premises used: CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction, CategoryTheory.IsIso, CategoryTheory.Comonad.Coalgebra.Hom.f, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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
X : adj.toComonad.Coalgebra
rw :
  IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckEqualizer X).lift (counitFork X) : (counitFork X).pt ⟶ (beckFork X).pt)
⊢ IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Coalgebra.Hom.f (NatTrans.app (counit (comparisonAdjunction adj)) X))

Tactic:
rw [comparisonAdjunction_counit_f]

Premises used: CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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
X : adj.toComonad.Coalgebra
⊢ IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckEqualizer X).lift (counitFork X) : (counitFork X).pt ⟶ (beckFork X).pt)

Tactic:
(IsLimit.conePointUniqueUpToIso (beckEqualizer X)
          (counitLimitOfPreservesEqualizer X)).isIso_inv

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer, CategoryTheory.Comonad.beckEqualizer, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj, CategoryTheory.Iso.isIso_inv, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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
X : adj.toComonad.Coalgebra
⊢ IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckEqualizer X).lift (counitFork X) : (counitFork X).pt ⟶ (beckFork X).pt)

Tactic:
exact (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
          (counitLimitOfPreservesEqualizer X)).isIso_inv

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer, CategoryTheory.Comonad.beckEqualizer, CategoryTheory.Iso.isIso_inv
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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
⊢ ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)

Tactic:
have : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X) := by
      intro X
      apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).counit.app X).f
        rw [comparisonAdjunction_counit_f]
        exact (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
          (counitLimitOfPreservesEqualizer X)).isIso_inv
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
rw :
  IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
    (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
      (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
⊢ IsIso (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y) (NatTrans.app (unit (comparisonAdjunction adj)) Y)

Tactic:
rw [comparisonAdjunction_unit_app]

Premises used: CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
change :
  IsIso (X := (unitFork adj Y).pt) (Y :=
    (limit.cone (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).pt)
    (Iso.inv
      (IsLimit.conePointUniqueUpToIso
        (limit.isLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
        (have this : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) := ⋯;
        unitEqualizerOfCoreflectsEqualizer adj Y)))
change₁ : IsLimit (unitFork adj Y)
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
    (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
      (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))

Tactic:
change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv

Premises used: CategoryTheory.IsIso, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
⊢ IsIso (X := (unitFork adj Y).pt) (Y :=
    (limit.cone (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).pt)
    (Iso.inv
      (IsLimit.conePointUniqueUpToIso
        (limit.isLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
        (have this : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) := ⋯;
        unitEqualizerOfCoreflectsEqualizer adj Y)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
apply :
  G.map (F.map (adj.unit.app Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
apply₁ :
  adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
⊢ IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))

Tactic:
apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _

Premises used: CategoryTheory.IsCoreflexivePair.mk', CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
rw :
  G.map (F.map (adj.unit.app Y) ≫ adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
⊢ G.map (F.map (adj.unit.app Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))

Tactic:
rw [← G.map_comp, ← G.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
⊢ G.map (F.map (adj.unit.app Y) ≫ adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))

Tactic:
congr_arg G.map (adj.left_triangle_components Y)

Premises used: CategoryTheory.Functor.map, congr_arg, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
⊢ G.map (F.map (adj.unit.app Y) ≫ adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))

Tactic:
exact congr_arg G.map (adj.left_triangle_components Y)

Premises used: CategoryTheory.Functor.map, congr_arg, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
rw :
  adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))

Tactic:
rw [← G.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
Y : C
⊢ IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))

Tactic:
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
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)))
apply : ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F
⊢ IsLimit (unitFork adj Y)

Tactic:
apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_

Premises used: CategoryTheory.Comonad.ComonadicityInternal.unitEqualizerOfCoreflectsEqualizer
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)))
⊢ ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F

Tactic:
apply reflectsLimit_of_reflectsIsomorphisms

Premises used: CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
⊢ ∀ (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
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
this :
  ∀ (Y : C),
    IsIso (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y) (NatTrans.app (unit (comparisonAdjunction adj)) Y)
⊢ (comparison adj).IsEquivalence

Tactic:
(comparisonAdjunction adj).toEquivalence.symm.isEquivalence_inverse

Premises used: CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction, CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.Comonad.comparison, CategoryTheory.Adjunction.toEquivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
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)
this :
  ∀ (Y : C),
    IsIso (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y) (NatTrans.app (unit (comparisonAdjunction adj)) Y)
⊢ (comparison adj).IsEquivalence

Tactic:
exact (comparisonAdjunction adj).toEquivalence.symm.isEquivalence_inverse

Premises used: CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction, CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.Adjunction.toEquivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ ι X ≫ topMap X = ι X ≫ bottomMap X

Tactic:
Coalgebra.Hom.ext X.coassoc.symm

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.ext, CategoryTheory.Comonad.Coalgebra.coassoc, Eq.symm
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
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)
apply₂ : CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
⊢ IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)

Tactic:
apply IsCoreflexivePair.mk' _ _ _

Premises used: CategoryTheory.IsCoreflexivePair.mk'
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
⊢ T.cofree.obj (T.obj X.A) ⟶ T.cofree.obj X.A

Tactic:
apply (cofree T).map (T.ε.app X.A)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Comonad.ε, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.Comonad.cofree, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
h : (CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A)).f = Coalgebra.Hom.f (𝟙 (T.cofree.obj X.A))
⊢ CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
h : T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)
⊢ (CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A)).f = Coalgebra.Hom.f (𝟙 (T.cofree.obj X.A))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
h : T.map (X.a ≫ T.ε.app X.A) = 𝟙 (T.obj X.A)
h₁ : T.map (𝟙 X.A) = 𝟙 (T.obj X.A)
h₂ h₃ : Eq.{v₁ + 1} (α := T.obj X.A ⟶ T.obj X.A) (𝟙 (T.obj X.A)) (𝟙 (T.obj X.A))
⊢ T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)

Tactic:
rw [← Functor.map_comp, X.counit, Functor.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Comonad.Coalgebra.counit
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
h : (CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A)).f = Coalgebra.Hom.f (𝟙 (T.cofree.obj X.A))
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
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)).f = Coalgebra.Hom.f (𝟙 (T.cofree.obj X.A))

Tactic:
apply Comonad.right_counit

Premises used: CategoryTheory.Comonad.right_counit
-- Module: Mathlib.CategoryTheory.Monad.Equalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Comonad.{v₁, u₁} C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
⊢ 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