awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
apply : T.free.obj X.A ⟶ T.free.obj (T.obj X.A)
apply₁ : T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)
apply₂ : T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)

Tactic:
apply IsReflexivePair.mk' _ _ _

Premises used: CategoryTheory.IsReflexivePair.mk'
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ T.free.obj X.A ⟶ T.free.obj (T.obj X.A)

Tactic:
apply (free T).map (T.η.app X.A)

Premises used: CategoryTheory.Monad.Algebra.A, CategoryTheory.Functor.map, CategoryTheory.Monad.η, CategoryTheory.Monad.free, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
h : (T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X).f = Algebra.Hom.f (𝟙 (T.free.obj X.A))
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
h : T.map (T.η.app X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)
⊢ (T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X).f = Algebra.Hom.f (𝟙 (T.free.obj X.A))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
h : T.map (T.η.app X.A ≫ 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 (T.η.app X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)

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

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
h : (T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X).f = Algebra.Hom.f (𝟙 (T.free.obj X.A))
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ (T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X).f = Algebra.Hom.f (𝟙 (T.free.obj X.A))

Tactic:
apply Monad.right_unit

Premises used: CategoryTheory.Monad.right_unit
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
⊢ T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f

Tactic:
have h₁ : (T : C ⥤ C).map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f :=
      congr_arg Monad.Algebra.Hom.f s.condition
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
⊢ T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f

Tactic:
have h₂ : (T : C ⥤ C).map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f := s.π.h
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 :
  T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
refine_2 :
  (beckAlgebraCofork X).π ≫
      { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ : (beckAlgebraCofork X).pt.Hom s.pt } =
    s.π
refine_3 :
  ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt},
    (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }
⊢ { l : (beckAlgebraCofork X).pt ⟶ s.pt //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }

Tactic:
refine ⟨⟨T.η.app _ ≫ s.π.f, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
⊢ T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_1 : (T.map (T.η.app X.1) ≫ T.map s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₁ : T.map (T.η.app X.1) ≫ T.map s.π.f ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₂ : T.map (T.η.app X.1) ≫ T.μ.app X.A ≫ s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₃ : s.π.f = X.a ≫ T.η.app X.1 ≫ s.π.f
refine_1₄ : s.π.f = T.η.app (T.obj X.1) ≫ T.map X.2 ≫ s.π.f
refine_1₅ : s.π.f = T.η.app (T.obj X.1) ≫ T.μ.app X.A ≫ s.π.f
refine_1₆ refine_1₇ : s.π.f = s.π.f
⊢ T.map (T.η.app X.1 ≫ s.π.f) ≫ s.pt.a = X.a ≫ T.η.app X.1 ≫ s.π.f

Tactic:
rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Monad.Algebra.a, CategoryTheory.Monad.η, CategoryTheory.Functor.map_comp, CategoryTheory.Monad.left_unit_assoc, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Monad.right_unit_assoc
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
refine_2 :
  ((beckAlgebraCofork X).π ≫
        { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ : (beckAlgebraCofork X).pt.Hom s.pt }).f =
    s.π.f
⊢ (beckAlgebraCofork X).π ≫
      { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ : (beckAlgebraCofork X).pt.Hom s.pt } =
    s.π

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ ((beckAlgebraCofork X).π ≫
        { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ : (beckAlgebraCofork X).pt.Hom s.pt }).f =
    s.π.f

Tactic:
simpa [← T.η.naturality_assoc, T.left_unit_assoc] using T.η.app ((T : C ⥤ C).obj X.A) ≫= h₁

Premises used: CategoryTheory.Monad.Algebra.A, CategoryTheory.Monad.toFunctor, CategoryTheory.Monad.η, CategoryTheory.Monad.left_unit_assoc, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
refine_3 : m.f = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }.f
⊢ m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
refine_3 : m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f
⊢ m.f = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }.f

Tactic:
dsimp only
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
refine_3 : m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ ((beckAlgebraCofork X).π ≫ m).f
⊢ m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f

Tactic:
rw [← hm]
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ ((beckAlgebraCofork X).π ≫ m).f

Tactic:
apply (X.unit_assoc _).symm

Premises used: CategoryTheory.Monad.Algebra.unit_assoc, Eq.symm
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
⊢ (beckCofork X).π = X.a

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Monad.Coequalizer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : T.Algebra
s : Cofork (T.map X.a) (T.μ.app X.A)
⊢ (beckCoequalizer X).desc s = T.η.app X.A ≫ s.π

Tactic:
rfl

Premises used: 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
A : adj.toComonad.Coalgebra
apply : G.map A.a ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
apply₁ : adj.unit.app (G.obj A.A) ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
⊢ IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))

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
A : adj.toComonad.Coalgebra
rw : G.map (A.a ≫ adj.counit.app A.1) = G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
⊢ G.map A.a ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))

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
A : adj.toComonad.Coalgebra
⊢ G.map (A.a ≫ adj.counit.app A.1) = G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))

Tactic:
congr_arg G.map A.counit

Premises used: CategoryTheory.Functor.map, congr_arg, CategoryTheory.Comonad.Coalgebra.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
A : adj.toComonad.Coalgebra
⊢ G.map (A.a ≫ adj.counit.app A.1) = G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))

Tactic:
exact congr_arg G.map A.counit

Premises used: CategoryTheory.Functor.map, congr_arg, CategoryTheory.Comonad.Coalgebra.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
A : adj.toComonad.Coalgebra
rw :
  Eq.{v₁ + 1} (α := G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1) ⟶ G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
    (𝟙 (G.obj A.A)) (𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1)))
⊢ adj.unit.app (G.obj A.A) ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))

Tactic:
rw [adj.right_triangle_components]

Premises used: CategoryTheory.Adjunction.right_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
A : adj.toComonad.Coalgebra
⊢ Eq.{v₁ + 1} (α := G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1) ⟶ G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1))
    (𝟙 (G.obj A.A)) (𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) A.1)))

Tactic:
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
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
refine :
  Eq (α := B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ G.map A.a : B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ adj.unit.app (G.1 A.A) :
      B ⟶ G.obj (adj.toComonad.obj A.A))
⊢ B ⟶ comparisonRightAdjointObj adj A

Tactic:
refine equalizer.lift (adj.homEquiv _ _ f.f) ?_

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.f, CategoryTheory.Limits.equalizer.lift, 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
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
simp :
  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)
⊢ Eq (α := B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ G.map A.a : B ⟶ G.obj (adj.toComonad.obj A.A))
    ((adj.homEquiv B A.A : (a : F.obj B ⟶ A.A) → B ⟶ G.obj A.A) f.f ≫ adj.unit.app (G.1 A.A) :
      B ⟶ G.obj (adj.toComonad.obj A.A))

Tactic:
simp only [Adjunction.toComonad_coe, Functor.comp_obj, Adjunction.homEquiv_unit,
          Category.assoc, ← G.map_comp, ← f.h, comparison_obj_A, comparison_obj_a]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Comonad.comparison_obj_a, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.Comonad.comparison_obj_A, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.toComonad_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
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality]

Premises used: CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.unit_naturality_assoc
-- 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
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))
⊢ (comparison adj).obj B ⟶ A

Tactic:
refine ⟨(adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)), (adj.homEquiv _ _).injective ?_⟩
-- 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
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
⊢ 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:
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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Comonad.comparison_obj_a, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Comonad.comparison_obj_A, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Adjunction.right_triangle_components_assoc, CategoryTheory.Adjunction.toComonad_coe, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.unit_naturality_assoc
-- 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
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)
⊢ 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:
congr 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
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 (α := 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:
(equalizer.condition _ _).symm

Premises used: CategoryTheory.Limits.equalizer.condition, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj, Eq.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
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 (α := 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:
exact (equalizer.condition _ _).symm

Premises used: CategoryTheory.Limits.equalizer.condition, Eq.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
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
⊢ (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))
      ((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))))
        f) =
    f

Tactic:
aesop