awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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 : (comparison adj).obj B ⟶ A
rw :
  adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
rw₁ :
  adj.unit.app B ≫ G.map (F.map (adj.unit.app B)) ≫ G.map (F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
rw₂ :
  adj.unit.app B ≫ adj.unit.app (G.obj (F.obj B)) ≫ G.map (F.map (G.map f.f)) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
⊢ adj.unit.app B ≫ G.map (F.map (adj.unit.app B) ≫ (G ⋙ F).map f.f) =
    adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
have rw₃ : adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.obj A.A) = adj.unit.app B ≫ G.map f.f ≫ adj.unit.app (G.1 A.A)
Tactic: rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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
⊢ (comparison adj).obj B ⟶ A
have refine : Eq (α := B ⟶ G.obj (adj.toComonad.obj A.A))
  ((adj.homEquiv B (adj.toComonad.obj A.A) : (a : F.obj B ⟶ adj.toComonad.obj A.A) → B ⟶ G.obj (adj.toComonad.obj A.A))
      (((comparison adj).obj B).a ≫
        adj.toComonad.map
          ((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))))) :
    B ⟶ G.obj (adj.toComonad.obj A.A))
  ((adj.homEquiv B (adj.toComonad.obj A.A) : (a : F.obj B ⟶ adj.toComonad.obj A.A) → B ⟶ G.obj (adj.toComonad.obj A.A))
      ((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))) ≫
          A.a :
        ((comparison adj).obj B).A ⟶ adj.toComonad.obj A.A) :
    B ⟶ G.obj (adj.toComonad.obj A.A))
Tactic: refine ⟨(adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)), (adj.homEquiv _ _).injective ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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
⊢ Eq (α := B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B (adj.toComonad.obj A.A) :
          (a : F.obj B ⟶ adj.toComonad.obj A.A) → B ⟶ G.obj (adj.toComonad.obj A.A))
        (((comparison adj).obj B).a ≫
          adj.toComonad.map
            ((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))))) :
      B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B (adj.toComonad.obj A.A) :
          (a : F.obj B ⟶ adj.toComonad.obj A.A) → B ⟶ G.obj (adj.toComonad.obj A.A))
        ((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))) ≫
            A.a :
          ((comparison adj).obj B).A ⟶ adj.toComonad.obj A.A) :
      B ⟶ G.obj (adj.toComonad.obj A.A))
have simp : f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ adj.unit.app (G.obj A.A) =
  f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ G.map A.a
Tactic: simp only [Adjunction.toComonad_coe, Functor.comp_obj, comparison_obj_A, comparison_obj_a,
          Adjunction.homEquiv_counit, Functor.map_comp, Category.assoc,
          Functor.comp_map, Adjunction.homEquiv_unit, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality, Adjunction.right_triangle_components_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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
⊢ f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ adj.unit.app (G.obj A.A) =
    f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ G.map A.a
have e_a : Eq (α := comparisonRightAdjointObj adj A ⟶ G.obj (F.obj (G.obj A.A)))
  (equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ adj.unit.app (G.obj A.A))
  (equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ G.map A.a)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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
⊢ (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
have 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) sorry :
          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 := sorry } :
            ((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: apply equalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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))
⊢ adj.toComonad.Coalgebra ⥤ C
have refine_1 : (A : C) →
  (B : adj.toComonad.Coalgebra) →
    ((comparison adj).obj A ⟶ B) ≃ (A ⟶ (fun (A : adj.toComonad.Coalgebra) ↦ comparisonRightAdjointObj adj A) B)
Tactic: refine
    Adjunction.rightAdjointOfEquiv (F := comparison adj)
      (G_obj := fun A => comparisonRightAdjointObj adj A) (fun A B => ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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)
⊢ adj.toComonad.Coalgebra ⥤ C
have 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)
Tactic: refine
    Adjunction.rightAdjointOfEquiv (F := comparison adj)
      (G_obj := fun A => comparisonRightAdjointObj adj A) (fun A B => ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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'
⊢ 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')
have 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)))
Tactic: apply equalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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))
⊢ 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)))
have 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)))
Tactic: rw [← F.map_comp, equalizer.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [← F.map_comp, equalizer.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [← F.map_comp, equalizer.condition, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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
⊢ 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))
have 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)))
Tactic: apply equalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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)))
      (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)))
have 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))) sorry)
    (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) sorry) (equalizer.ι (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
Tactic: change
    equalizer.lift ((adj.homEquiv B _) (𝟙 _)) _ ≫ equalizer.ι _ _ =
      equalizer.lift _ _ ≫ equalizer.ι _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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
⊢ CreatesLimit (parallelPair f g) F
have inst : PreservesLimit (parallelPair f g ⋙ F) (comonadicRightAdjoint F ⋙ F)
Tactic: apply +allowSynthFailures comonadicCreatesLimitOfPreservesLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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)
⊢ CreatesLimit (parallelPair f g) F
have inst₁ : PreservesLimit ((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F) (comonadicRightAdjoint F ⋙ F)
Tactic: apply +allowSynthFailures comonadicCreatesLimitOfPreservesLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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 g ⋙ F) (comonadicRightAdjoint F ⋙ F)
have apply : PreservesLimit
  (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
    ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
  (comonadicRightAdjoint F ⋙ F)
Tactic: apply @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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 ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
    (comonadicRightAdjoint F ⋙ F)
have dsimp : PreservesLimit (parallelPair (F.map f) (F.map g)) (comonadicRightAdjoint F ⋙ F)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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 g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F) (comonadicRightAdjoint F ⋙ F)
have 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)
Tactic: apply @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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 (((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F).map WalkingParallelPairHom.left)
      (((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F).map WalkingParallelPairHom.right))
    (comonadicRightAdjoint F ⋙ F)
have dsimp : PreservesLimit
  (parallelPair (F.map ((comonadicRightAdjoint F).map (F.map f))) (F.map ((comonadicRightAdjoint F).map (F.map g))))
  (comonadicRightAdjoint F ⋙ F)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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)
have apply : IsIso (X := adj.toComonad.forget.obj ((rightAdjointComparison adj ⋙ comparison adj).obj X))
  (adj.toComonad.forget.map (NatTrans.app (counit (comparisonAdjunction adj)) X))
Tactic: apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
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 := adj.toComonad.forget.obj ((rightAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toComonad.forget.map (NatTrans.app (counit (comparisonAdjunction adj)) X))
have change : IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
  (Coalgebra.Hom.f (NatTrans.app (counit (comparisonAdjunction adj)) X))
Tactic: change IsIso ((comparisonAdjunction adj).counit.app X).f