awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
dsimp :
  R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫ X.a)) =
    𝟙 (R.obj ((reflector R).obj X.A))
⊢ R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫ X.a)) =
    𝟙 (R.obj ((reflector R).obj X.A))

Tactic:
dsimp [X.unit]

Premises used: CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
⊢ R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫ X.a)) =
    𝟙 (R.obj ((reflector R).obj X.A))

Tactic:
simpa using congrArg (fun t ↦ R.map ((reflector R).map t)) X.unit

Premises used: congrArg, CategoryTheory.reflector, CategoryTheory.Functor.map, CategoryTheory.Monad.Algebra.unit
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
⊢ EssSurj (D := (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra)
    (Monad.comparison (reflectorAdjunction R))

Tactic:
⟨fun X => ⟨(reflector R).obj X.A, ⟨?_⟩⟩⟩

Premises used: CategoryTheory.reflector, CategoryTheory.Functor.EssSurj.mk, Nonempty.intro, CategoryTheory.Monad.Algebra.A, Exists.intro, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
symm : X ≅ obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)
⊢ obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A) ≅ X

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
refine_1 :
  X.A ≅
    Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
      (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))
refine_2 :
  Eq (α :=
    (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj X.A ⟶
      Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
        (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (CategoryStruct.comp (Y :=
      (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj
        (Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
          (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
      ((Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A))))
      (Monad.Algebra.a (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
    (X.a ≫ Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)))
⊢ X ≅ obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)

Tactic:
refine Monad.Algebra.isoMk ?_ ?_

Premises used: CategoryTheory.Monad.Algebra.isoMk
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
⊢ X.A ≅
    Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
      (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))

Tactic:
exact asIso ((reflectorAdjunction R).unit.app X.A)

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Monad.Algebra.A, CategoryTheory.reflectorAdjunction, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
refine_2 :
  Eq (α := R.obj ((reflector R).obj X.A) ⟶ R.obj ((reflector R).obj X.A))
    (R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
      R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
⊢ Eq (α :=
    (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj X.A ⟶
      Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
        (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (CategoryStruct.comp (Y :=
      (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj
        (Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
          (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
      ((Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A))))
      (Monad.Algebra.a (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
    (X.a ≫ Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)))

Tactic:
dsimp only [Functor.comp_map, Monad.comparison_obj_a, asIso_hom, Functor.comp_obj,
    Monad.comparison_obj_A, Adjunction.toMonad_coe]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Monad.comparison_obj_a, CategoryTheory.Monad.comparison_obj_A, CategoryTheory.Adjunction.toMonad_coe, CategoryTheory.asIso_hom, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
refine_2 :
  Eq (α := obj.{v₁, v₁, u₁, u₁} (𝟭 C) X.A ⟶ R.obj ((reflector R).obj X.A))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
        R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
⊢ Eq (α := R.obj ((reflector R).obj X.A) ⟶ R.obj ((reflector R).obj X.A))
    (R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
      R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)

Tactic:
rw [← cancel_epi ((reflectorAdjunction R).unit.app X.A)]

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Monad.Algebra.A, CategoryTheory.reflectorAdjunction, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
refine_2 :
  Eq (α := X.A ⟶ R.obj ((reflector R).obj X.A))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
        R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
⊢ Eq (α := obj.{v₁, v₁, u₁, u₁} (𝟭 C) X.A ⟶ R.obj ((reflector R).obj X.A))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
        R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)

Tactic:
dsimp only [Functor.id_obj, Functor.comp_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
refine_2 :
  Eq (α := X.A ⟶ R.obj ((reflector R).obj X.A)) (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
⊢ Eq (α := X.A ⟶ R.obj ((reflector R).obj X.A))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
        R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)

Tactic:
rw [Adjunction.unit_naturality_assoc,
    Adjunction.right_triangle_components, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
⊢ Eq (α := X.A ⟶ R.obj ((reflector R).obj X.A)) (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)

Tactic:
apply (X.unit_assoc _).symm

Premises used: CategoryTheory.Monad.Algebra.unit_assoc, Eq.symm
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
dsimp : NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)
⊢ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.id_obj]

Premises used: CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
rw :
  R.map ((coreflector R).map X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) ((coreflector R ⋙ R).obj X.A) =
    𝟙 ((coreflector R ⋙ R).obj X.A)
⊢ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)

Tactic:
rw [← (coreflectorAdjunction R).counit_naturality]

Premises used: CategoryTheory.Adjunction.counit_naturality, CategoryTheory.coreflectorAdjunction
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
dsimp :
  R.map ((coreflector R).map X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) (R.obj ((coreflector R).obj X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))
⊢ R.map ((coreflector R).map X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) ((coreflector R ⋙ R).obj X.A) =
    𝟙 ((coreflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Adjunction.toMonad_coe
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
rw :
  R.map ((coreflector R).map (X.a ≫ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))
⊢ R.map ((coreflector R).map X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) (R.obj ((coreflector R).obj X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))

Tactic:
rw [counit_obj_eq_map_counit, ← Functor.map_comp, ← Functor.map_comp]

Premises used: CategoryTheory.counit_obj_eq_map_counit, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ R.map ((coreflector R).map (X.a ≫ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))

Tactic:
simpa using congrArg (fun t ↦ R.map ((coreflector R).map t)) X.counit

Premises used: CategoryTheory.coreflector, congrArg, CategoryTheory.Functor.map, CategoryTheory.Comonad.Coalgebra.counit
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
⊢ EssSurj (D := (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra)
    (Comonad.comparison (coreflectorAdjunction R))

Tactic:
⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩

Premises used: CategoryTheory.coreflector, CategoryTheory.Functor.EssSurj.mk, Nonempty.intro, Exists.intro, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
refine :
  (X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra) →
    obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A) ≅ X
⊢ EssSurj (D := (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra)
    (Comonad.comparison (coreflectorAdjunction R))

Tactic:
refine ⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
refine_1 :
  Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
      (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≅
    X.A
refine_2 :
  Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).obj X.A)
    (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
    (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a)
⊢ obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A) ≅ X

Tactic:
refine Comonad.Coalgebra.isoMk ?_ ?_

Premises used: CategoryTheory.Comonad.Coalgebra.isoMk
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
      (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≅
    X.A

Tactic:
exact (asIso ((coreflectorAdjunction R).counit.app X.A))

Premises used: CategoryTheory.Adjunction.counit, CategoryTheory.coreflectorAdjunction, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
refine_2 :
  Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      obj.{v₁, v₁, u₁, u₁} (𝟭 C) X.A)
    (CategoryStruct.comp (Y := (coreflector R ⋙ R).obj X.A)
      (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
        (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
          (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
      (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))
    ((Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
⊢ Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).obj X.A)
    (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
    (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a)

Tactic:
rw [← cancel_mono ((coreflectorAdjunction R).counit.app X.A)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Adjunction.counit, CategoryTheory.coreflectorAdjunction, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
refine_2 :
  Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      X.A)
    (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
          (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))) ≫
        NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
    (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫
      X.a ≫ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
⊢ Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      obj.{v₁, v₁, u₁, u₁} (𝟭 C) X.A)
    (CategoryStruct.comp (Y := (coreflector R ⋙ R).obj X.A)
      (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
        (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
          (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
      (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))
    ((Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)

Tactic:
simp only [Functor.comp_obj, Functor.id_obj,
    assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      X.A)
    (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
          (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))) ≫
        NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
    (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫
      X.a ≫ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)

Tactic:
simpa using (coreflectorAdjunction R).counit.app X.A ≫= X.counit.symm

Premises used: CategoryTheory.Adjunction.counit, CategoryTheory.coreflectorAdjunction, CategoryTheory.Comonad.Coalgebra.A, CategoryTheory.Comonad.Coalgebra.counit, Eq.symm, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X Y : T.Algebra
f g : X ⟶ Y
h : f.f = g.f
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.Monad.Algebra.Hom.ext
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A A' A'' : T.Algebra
f : A ⟶ A'
g : A' ⟶ A''
⊢ Hom.comp f g = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A : T.Algebra
⊢ Hom.id A = 𝟙 A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monad.Algebra
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A : T.Algebra
⊢ Hom.f (𝟙 A) = 𝟙 A.A

Tactic:
rfl

Premises used: rfl