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
A B : C
f g : A ⟶ B
inst_2 : F.IsCosplitPair f g
inst_3 : ReflectsLimitOfIsCosplitPair F
⊢ ReflectsLimit (parallelPair f g) F

Tactic:
ReflectsLimitOfIsCosplitPair.out f g

Premises used: CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.out
-- 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 : ReflectsLimitOfIsCosplitPair F
⊢ ∀ (A : adj.toComonad.Coalgebra), ReflectsLimit (parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F

Tactic:
fun _ => ReflectsLimitOfIsCosplitPair.out _ _

Premises used: CategoryTheory.Comonad.Coalgebra.a, CategoryTheory.Adjunction.unit, CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.out, CategoryTheory.Functor.map, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.Functor.obj, 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
apply :
  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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
this :
  IsIso (X := (counitFork X).pt)
    (Iso.inv ((beckEqualizer X).conePointUniqueUpToIso (counitLimitOfPreservesEqualizer X)))
⊢ IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckEqualizer X).lift (counitFork X) : (counitFork X).pt ⟶ (beckFork X).pt)

Tactic:
change
          IsIso
            (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
                (counitLimitOfPreservesEqualizer X)).inv

Premises used: CategoryTheory.IsIso, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer, CategoryTheory.Comonad.beckEqualizer, 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso (X := (counitFork X).pt)
    (Iso.inv ((beckEqualizer X).conePointUniqueUpToIso (counitLimitOfPreservesEqualizer X)))

Tactic:
(IsLimit.conePointUniqueUpToIso _ _).isIso_inv

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso (X := (counitFork X).pt)
    (Iso.inv ((beckEqualizer X).conePointUniqueUpToIso (counitLimitOfPreservesEqualizer X)))

Tactic:
exact (IsLimit.conePointUniqueUpToIso _ _).isIso_inv

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
⊢ ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)

Tactic:
have : ∀ (X : Coalgebra adj.toComonad), 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]
        change
          IsIso
            (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
                (counitLimitOfPreservesEqualizer X)).inv
        exact (IsLimit.conePointUniqueUpToIso _ _).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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
change :
  IsIso (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)))))
        (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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsIso (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)))))
        (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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
h : F.IsCosplitPair (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:
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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair 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
      apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
      letI _ :
        F.IsCosplitPair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) :=
        ComonadicityInternal.main_pair_F_cosplit _ ((comparison adj).obj Y)
      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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair 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 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair 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.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 : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
rw :
  HasLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
⊢ HasLimit (parallelPair f g ⋙ F)

Tactic:
rw [hasLimit_iff_of_iso (diagramIsoParallelPair _)]

Premises used: CategoryTheory.Limits.hasLimit_iff_of_iso, CategoryTheory.Limits.diagramIsoParallelPair
-- 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 : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
⊢ HasLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))

Tactic:
inferInstanceAs <| HasEqualizer (F.map f) (F.map g)

Premises used: CategoryTheory.Comonad.comonadicOfCreatesFSplitEqualizers._proof_1
-- 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 : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
⊢ HasLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))

Tactic:
exact inferInstanceAs <| HasEqualizer (F.map f) (F.map g)
-- 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 : CreatesLimitOfIsCosplitPair F
⊢ ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)

Tactic:
have I {A B} (f g : A ⟶ B) [F.IsCosplitPair f g] : HasLimit (parallelPair f g ⋙ F) := by
    rw [hasLimit_iff_of_iso (diagramIsoParallelPair _)]
    exact inferInstanceAs <| HasEqualizer (F.map f) (F.map g)
-- 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 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
⊢ HasEqualizerOfIsCosplitPair F

Tactic:
have : HasEqualizerOfIsCosplitPair F := ⟨fun _ _ => hasLimit_of_created (parallelPair _ _) 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 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
⊢ PreservesLimit (parallelPair f g) F

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 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
⊢ PreservesLimitOfIsCosplitPair F

Tactic:
have : PreservesLimitOfIsCosplitPair F := ⟨by intros; 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 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this_1 : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
⊢ ReflectsLimit (parallelPair f g) F

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 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this_1 : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
⊢ ReflectsLimitOfIsCosplitPair F

Tactic:
have : ReflectsLimitOfIsCosplitPair F := ⟨by intros; 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 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this_1 : HasEqualizerOfIsCosplitPair F
this_2 : PreservesLimitOfIsCosplitPair F
this : ReflectsLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F

Tactic:
exact comonadicOfHasPreservesReflectsFSplitEqualizers adj

Premises used: CategoryTheory.Comonad.comonadicOfHasPreservesReflectsFSplitEqualizers
-- 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 : F.ReflectsIsomorphisms
inst_3 : HasEqualizerOfIsCosplitPair F
inst_4 : PreservesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
h : F.IsCosplitPair f g
⊢ HasEqualizer f g

Tactic:
have := HasEqualizerOfIsCosplitPair.out F f g
-- 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 : F.ReflectsIsomorphisms
inst_3 : HasEqualizerOfIsCosplitPair F
inst_4 : PreservesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
h : F.IsCosplitPair f g
this : HasEqualizer f g
⊢ ReflectsLimit (parallelPair f g) 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 : F.ReflectsIsomorphisms
inst_3 : HasEqualizerOfIsCosplitPair F
inst_4 : PreservesLimitOfIsCosplitPair F
⊢ ReflectsLimitOfIsCosplitPair F

Tactic:
have : ReflectsLimitOfIsCosplitPair F := ⟨fun f g _ => by
    have := HasEqualizerOfIsCosplitPair.out F f g
    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 : F.ReflectsIsomorphisms
inst_3 : HasEqualizerOfIsCosplitPair F
inst_4 : PreservesLimitOfIsCosplitPair F
this : ReflectsLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F

Tactic:
apply comonadicOfHasPreservesReflectsFSplitEqualizers adj

Premises used: CategoryTheory.Comonad.comonadicOfHasPreservesReflectsFSplitEqualizers
-- 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
A B : C
f g : A ⟶ B
inst_4 : IsCoreflexivePair f g
inst_5 : PreservesLimitOfIsCoreflexivePair F
⊢ PreservesLimit (parallelPair f g) F

Tactic:
PreservesLimitOfIsCoreflexivePair.out f g

Premises used: CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.out
-- 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), PreservesLimit (parallelPair (G.map X.a) (adj.unit.app (G.obj X.A))) F

Tactic:
fun _ => PreservesLimitOfIsCoreflexivePair.out _ _

Premises used: CategoryTheory.Comonad.Coalgebra.a, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.out, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app