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 : adj.toComonad.Coalgebra
B : C
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
h :
  CategoryStruct.comp (Y := equalizer (G.map A.a) (adj.unit.app (G.1 A.A)))
      ((fun (f : (comparison adj).obj B ⟶ A) ↦
          (equalizer.lift ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f) ⋯ :
            B ⟶ equalizer (G.map A.a) (adj.unit.app (G.1 A.A))))
        ((fun (f : B ⟶ comparisonRightAdjointObj adj A) ↦
            ({
                f :=
                  (Equiv.symm (adj.homEquiv B A.A) : (a : B ⟶ G.obj A.A) → F.obj B ⟶ A.A)
                    (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))),
                h := ⋯ } :
              ((comparison adj).obj B).Hom A))
          f))
      (equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))) =
    f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))
⊢ (fun (f : (comparison adj).obj B ⟶ A) ↦
        (equalizer.lift ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f) ⋯ :
          B ⟶ equalizer (G.map A.a) (adj.unit.app (G.1 A.A))))
      ((fun (f : B ⟶ comparisonRightAdjointObj adj A) ↦
          ({
              f :=
                (Equiv.symm (adj.homEquiv B A.A) : (a : B ⟶ G.obj A.A) → F.obj B ⟶ A.A)
                  (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))),
              h := ⋯ } :
            ((comparison adj).obj B).Hom A))
        f) =
    f

Tactic:
apply equalizer.hom_ext

Premises used: CategoryTheory.Limits.equalizer.hom_ext
-- 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 : adj.toComonad.Coalgebra
B : C
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ CategoryStruct.comp (Y := equalizer (G.map A.a) (adj.unit.app (G.1 A.A)))
      ((fun (f : (comparison adj).obj B ⟶ A) ↦
          (equalizer.lift ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f) ⋯ :
            B ⟶ equalizer (G.map A.a) (adj.unit.app (G.1 A.A))))
        ((fun (f : B ⟶ comparisonRightAdjointObj adj A) ↦
            ({
                f :=
                  (Equiv.symm (adj.homEquiv B A.A) : (a : B ⟶ G.obj A.A) → F.obj B ⟶ A.A)
                    (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))),
                h := ⋯ } :
              ((comparison adj).obj B).Hom A))
          f))
      (equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))) =
    f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))

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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
refine_1 :
  (A : C) →
    (B : adj.toComonad.Coalgebra) →
      ((comparison adj).obj A ⟶ B) ≃ (A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B)
refine_2 :
  ∀ (X' X : C) (Y : adj.toComonad.Coalgebra) (f : X' ⟶ X) (g : (comparison adj).obj X ⟶ Y),
    Eq (α := X' ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) Y)
      (((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
                (comparisonRightAdjointHomEquiv adj B A :
                  ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
              X' Y :
            (a : (comparison adj).obj X' ⟶ Y) →
              X' ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) Y)
          ((comparison adj).map f ≫ g) :
        X' ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) Y)
      (f ≫
          ((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
                  (comparisonRightAdjointHomEquiv adj B A :
                    ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
                X Y :
              (a : (comparison adj).obj X ⟶ Y) →
                X ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) Y)
            g :
        X' ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) Y)
⊢ adj.toComonad.Coalgebra ⥤ C

Tactic:
refine
    Adjunction.rightAdjointOfEquiv (F := comparison adj)
      (G_obj := fun A => comparisonRightAdjointObj adj A) (fun A B => ?_) ?_

Premises used: CategoryTheory.Adjunction.rightAdjointOfEquiv
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A : C
B : adj.toComonad.Coalgebra
⊢ ((comparison adj).obj A ⟶ B) ≃ (A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B)

Tactic:
apply comparisonRightAdjointHomEquiv

Premises used: CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A B : C
B' : adj.toComonad.Coalgebra
g : A ⟶ B
h : (comparison adj).obj B ⟶ B'
refine_2 :
  CategoryStruct.comp (Y := equalizer (G.map B'.a) (adj.unit.app (G.1 B'.A)))
      (((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
              (comparisonRightAdjointHomEquiv adj B A :
                ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
            A B' :
          (a : (comparison adj).obj A ⟶ B') →
            A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
        ((comparison adj).map g ≫ h))
      (equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A))) =
    CategoryStruct.comp (Y := equalizer (G.map B'.a) (adj.unit.app (G.1 B'.A)))
      (g ≫
        ((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
                (comparisonRightAdjointHomEquiv adj B A :
                  ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
              B B' :
            (a : (comparison adj).obj B ⟶ B') →
              B ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
          h)
      (equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A)))
⊢ Eq (α := A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
    (((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
              (comparisonRightAdjointHomEquiv adj B A :
                ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
            A B' :
          (a : (comparison adj).obj A ⟶ B') →
            A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
        ((comparison adj).map g ≫ h) :
      A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
    (g ≫
        ((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
                (comparisonRightAdjointHomEquiv adj B A :
                  ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
              B B' :
            (a : (comparison adj).obj B ⟶ B') →
              B ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
          h :
      A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')

Tactic:
apply equalizer.hom_ext

Premises used: CategoryTheory.Limits.equalizer.hom_ext
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A B : C
B' : adj.toComonad.Coalgebra
g : A ⟶ B
h : (comparison adj).obj B ⟶ B'
⊢ CategoryStruct.comp (Y := equalizer (G.map B'.a) (adj.unit.app (G.1 B'.A)))
      (((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
              (comparisonRightAdjointHomEquiv adj B A :
                ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
            A B' :
          (a : (comparison adj).obj A ⟶ B') →
            A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
        ((comparison adj).map g ≫ h))
      (equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A))) =
    CategoryStruct.comp (Y := equalizer (G.map B'.a) (adj.unit.app (G.1 B'.A)))
      (g ≫
        ((fun (A : C) (B : adj.toComonad.Coalgebra) ↦
                (comparisonRightAdjointHomEquiv adj B A :
                  ((comparison adj).obj A ⟶ B) ≃ (A ⟶ comparisonRightAdjointObj adj B)))
              B B' :
            (a : (comparison adj).obj B ⟶ B') →
              B ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B')
          h)
      (equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A)))

Tactic:
simp [Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A : adj.toComonad.Coalgebra
⊢ Eq (α := ((rightAdjointComparison adj ⋙ comparison adj).obj A).A ⟶ (Functor.obj (𝟭 adj.toComonad.Coalgebra) A).A)
    (Coalgebra.Hom.f (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) A))
    ((Equiv.symm (adj.homEquiv (equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) A.A) :
        (a : equalizer (G.map A.a) (adj.unit.app (G.obj A.A)) ⟶ G.obj A.A) →
          F.obj (equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) ⟶ A.A)
      (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))))

Tactic:
congr_arg (adj.homEquiv _ _).symm (Category.id_comp _)

Premises used: CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj, congr_arg, CategoryTheory.Limits.limit, CategoryTheory.Adjunction.homEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.Category.id_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
A : adj.toComonad.Coalgebra
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
rw :
  Eq (α := F.obj (equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) ⟶ F.obj (G.obj (adj.toComonad.obj A.A)))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)) ≫ G.map A.a))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A)))
rw₁ :
  Eq (α := F.obj (equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) ⟶ F.obj (G.obj (adj.toComonad.obj A.A)))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)) ≫ adj.unit.app (G.obj A.A)))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A)))
rw₂ rw₃ :
  Eq (α := F.obj (equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) ⟶ F.obj (G.obj (adj.toComonad.obj A.A)))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A)))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A)))
⊢ Eq (α := F.obj (equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) ⟶ F.obj (G.obj (adj.toComonad.obj A.A)))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (G.map A.a))
    (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A)))

Tactic:
rw [← F.map_comp, equalizer.condition, F.map_comp]

Premises used: CategoryTheory.Limits.equalizer.condition, 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
A : adj.toComonad.Coalgebra
inst_2 : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ (counitFork A).ι = F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A : adj.toComonad.Coalgebra
⊢ Eq (α := ((rightAdjointComparison adj ⋙ comparison adj).obj A).A ⟶ (Functor.obj (𝟭 adj.toComonad.Coalgebra) A).A)
    (Coalgebra.Hom.f (NatTrans.app (Adjunction.counit (comparisonAdjunction adj)) A))
    ((beckEqualizer A).lift (counitFork A))

Tactic:
simp [Adjunction.homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_counit
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ HasLimit (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))

Tactic:
inferInstanceAs <| HasEqualizer
    (G.map ((comparison adj).obj B).a)
    (adj.unit.app (G.obj ((comparison adj).obj B).A))

Premises used: _private.0.CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA._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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
h :
  CategoryStruct.comp (Y :=
      equalizer (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) B)
      (equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A))) =
    CategoryStruct.comp (Y :=
      equalizer (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))
      (limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B))
      (equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))
⊢ Eq (α := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) B ⟶ (comparison adj ⋙ rightAdjointComparison adj).obj B)
    (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) B)
    (limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B))

Tactic:
apply equalizer.hom_ext

Premises used: CategoryTheory.Limits.equalizer.hom_ext
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
h :
  CategoryStruct.comp (Y :=
      equalizer (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))
      (equalizer.lift ((adj.homEquiv B (F.obj B) : (a : F.obj B ⟶ F.obj B) → B ⟶ G.obj (F.obj B)) (𝟙 (F.obj B))) ⋯)
      (equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A))) =
    CategoryStruct.comp (Y := equalizer (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
      (equalizer.lift (adj.unit.app B) ⋯)
      (equalizer.ι (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
⊢ CategoryStruct.comp (Y :=
      equalizer (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))
      (NatTrans.app (Adjunction.unit (comparisonAdjunction adj)) B)
      (equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A))) =
    CategoryStruct.comp (Y :=
      equalizer (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))
      (limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B))
      (equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))

Tactic:
change
    equalizer.lift ((adj.homEquiv B _) (𝟙 _)) _ ≫ equalizer.ι _ _ =
      equalizer.lift _ _ ≫ equalizer.ι _ _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.equalizer.lift, CategoryTheory.Limits.equalizer.ι, CategoryTheory.Adjunction.homEquiv, DFunLike.coe
-- 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 : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ CategoryStruct.comp (Y :=
      equalizer (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)))
      (equalizer.lift ((adj.homEquiv B (F.obj B) : (a : F.obj B ⟶ F.obj B) → B ⟶ G.obj (F.obj B)) (𝟙 (F.obj B))) ⋯)
      (equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A))) =
    CategoryStruct.comp (Y := equalizer (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
      (equalizer.lift (adj.unit.app B) ⋯)
      (equalizer.ι (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))

Tactic:
simp [Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit
-- Module: Mathlib.CategoryTheory.Monad.Comonadicity
Goal:
C : Type u₁
D : Type u₂
inst_1 : Category.{v₁, u₁} C
inst_2 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst_4 : F.IsCosplitPair f g
inst : PreservesLimit (parallelPair f g ⋙ F) (comonadicRightAdjoint F ⋙ F)
inst₁ : PreservesLimit ((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F) (comonadicRightAdjoint F ⋙ F)
⊢ CreatesLimit (parallelPair f g) F

Tactic:
apply +allowSynthFailures comonadicCreatesLimitOfPreservesLimit

Premises used: CategoryTheory.comonadicCreatesLimitOfPreservesLimit
-- 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 : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
apply :
  PreservesLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
    (comonadicRightAdjoint F ⋙ F)
⊢ PreservesLimit (parallelPair f g ⋙ F) (comonadicRightAdjoint F ⋙ F)

Tactic:
apply @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).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 : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
dsimp : PreservesLimit (parallelPair (F.map f) (F.map g)) (comonadicRightAdjoint F ⋙ F)
⊢ PreservesLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
    (comonadicRightAdjoint F ⋙ F)

Tactic:
dsimp
-- 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 : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
⊢ PreservesLimit (parallelPair (F.map f) (F.map g)) (comonadicRightAdjoint F ⋙ 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 : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
apply :
  PreservesLimit
    (parallelPair (((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F).map WalkingParallelPairHom.left)
      (((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F).map WalkingParallelPairHom.right))
    (comonadicRightAdjoint F ⋙ F)
⊢ PreservesLimit ((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F) (comonadicRightAdjoint F ⋙ F)

Tactic:
apply @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).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 : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
dsimp :
  PreservesLimit
    (parallelPair (F.map ((comonadicRightAdjoint F).map (F.map f))) (F.map ((comonadicRightAdjoint F).map (F.map g))))
    (comonadicRightAdjoint F ⋙ F)
⊢ PreservesLimit
    (parallelPair (((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F).map WalkingParallelPairHom.left)
      (((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F).map WalkingParallelPairHom.right))
    (comonadicRightAdjoint F ⋙ F)

Tactic:
dsimp
-- 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 : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
⊢ PreservesLimit
    (parallelPair (F.map ((comonadicRightAdjoint F).map (F.map f))) (F.map ((comonadicRightAdjoint F).map (F.map g))))
    (comonadicRightAdjoint F ⋙ 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
⊢ ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))

Tactic:
fun _ => HasEqualizerOfIsCosplitPair.out F _ _

Premises used: CategoryTheory.Comonad.Coalgebra.a, CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair.out, CategoryTheory.Adjunction.unit, 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
A B : C
f g : A ⟶ B
inst_2 : F.IsCosplitPair f g
inst_3 : PreservesLimitOfIsCosplitPair F
⊢ PreservesLimit (parallelPair f g) F

Tactic:
PreservesLimitOfIsCosplitPair.out f g

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

Tactic:
fun _ => PreservesLimitOfIsCosplitPair.out _ _

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