-- Mathlib/CategoryTheory/Monad/Monadicity.lean
theorem comparisonAdjunction_counit_app
    [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) :
    (comparisonAdjunction adj).counit.app B = colimit.desc _ (counitCofork adj B)

Proof state:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
B : D
⊢ coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc ((adj.homEquiv (G.obj B) B).symm (𝟙 (G.obj B))) ⋯ =
    coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc (adj.counit.app B) ⋯

Tactic:
simp [Adjunction.homEquiv_counit]

Result:
no goals

Proof state:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
B : D
⊢ coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      (comparisonAdjunction adj).counit.app B =
    coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
        (counitCofork adj B)

Tactic:
change
  coequalizer.π _ _ ≫ coequalizer.desc ((adj.homEquiv _ B).symm (𝟙 _)) _ =
    coequalizer.π _ _ ≫ coequalizer.desc _ _

Result:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
B : D
⊢ coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc ((adj.homEquiv (G.obj B) B).symm (𝟙 (G.obj B))) ⋯ =
    coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc (adj.counit.app B) ⋯

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
B : D
⊢ (comparisonAdjunction adj).counit.app B =
    colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
      (counitCofork adj B)

Tactic:
apply coequalizer.hom_ext

Result:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
B : D
⊢ coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      (comparisonAdjunction adj).counit.app B =
    coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫
      colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
        (counitCofork adj B)